uc-crux-llvm: Prefer TypeApplications when using Proxy (#938)

GaloisInc · Dec 9, 2021 · 0d01800 · 0d01800
1 parent c07213c
commit 0d01800
Show file tree

Hide file tree

Showing 7 changed files with 24 additions and 14 deletions.
diff --git a/uc-crux-llvm/.hlint.yaml b/uc-crux-llvm/.hlint.yaml
@@ -42,6 +42,11 @@
     lhs: "Prettyprinter.pretty (show x)"
     rhs: 'Prettyprinter.viaShow x'
 
+- error:
+    name: Use TypeApplications
+    lhs: "Proxy :: a"
+    rhs: 'Proxy @Whatever'
+
 # Ignored
 # -------
 

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Context/Module.hs b/uc-crux-llvm/src/UCCrux/LLVM/Context/Module.hs
@@ -11,6 +11,7 @@ Stability    : provisional
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 
 module UCCrux.LLVM.Context.Module
   ( ModuleContext,
@@ -204,7 +205,7 @@ findFun modCtx funcSym =
                        case retTy of
                          Nothing -> panic "findFun" ["Missing return type"]
                          Just (Some retTy') ->
-                           case testCompatibility (Proxy :: Proxy arch) retTy' cRetTy of
+                           case testCompatibility (Proxy @arch) retTy' cRetTy of
                              Just Refl ->
                                CFGWithTypes
                                  { cfgWithTypes = cfg,

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/FullType/Translation.hs b/uc-crux-llvm/src/UCCrux/LLVM/FullType/Translation.hs
@@ -16,6 +16,7 @@ Stability        : provisional
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 
@@ -208,7 +209,7 @@ translateModuleDefines llvmModule trans =
             if isVarArgs
               then removeVarArgsRepr crucibleTypes
               else Some crucibleTypes
-        case testCompatibilityAssign (Proxy :: Proxy arch) fullTypes crucibleTypes' of
+        case testCompatibilityAssign (Proxy @arch) fullTypes crucibleTypes' of
           Just Refl ->
             pure $
               FunctionTypes
@@ -252,7 +253,7 @@ translateModuleDefines llvmModule trans =
             (withExceptT FullTypeTranslation . toFullTypeM)
             (fdRetType liftedDecl)
         SomeAssign' crucibleTypes Refl _ <-
-          pure $ assignmentToCrucibleType (Proxy :: Proxy arch) fullTypes
+          pure $ assignmentToCrucibleType (Proxy @arch) fullTypes
         pure $
           FunctionTypes
             { ftArgTypes = MatchingAssign fullTypes crucibleTypes,

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs b/uc-crux-llvm/src/UCCrux/LLVM/Overrides/Skip.hs
@@ -14,6 +14,7 @@ Stability    : provisional
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 
 module UCCrux.LLVM.Overrides.Skip
   ( SkipOverrideName (..),
@@ -475,7 +476,7 @@ createSkipOverride modCtx sym usedRef annotationRef clobbers postcondition funcS
             "createSkipOverride"
             ["Mismatched return types - CFG was non-void"]
         (_, Just (Some retFullType)) ->
-          case testEquality (toCrucibleType (Proxy :: Proxy arch) retFullType) ret of
+          case testEquality (toCrucibleType (Proxy @arch) retFullType) ret of
             Nothing ->
               panic
                 "createSkipOverride"

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/PP.hs b/uc-crux-llvm/src/UCCrux/LLVM/PP.hs
@@ -8,6 +8,7 @@ Stability    : provisional
 -}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 
 module UCCrux.LLVM.PP
   ( ppRegValue,
@@ -82,13 +83,13 @@ ppRegMap _proxy funCtx sym mem (Crucible.RegMap regmap) =
   toListFC getConst
     <$> Ctx.traverseWithIndex
       ( \index (Const storageType) ->
-          case translateIndex (Proxy :: Proxy arch) (Ctx.size (funCtx ^. argumentStorageTypes)) index of
+          case translateIndex (Proxy @arch) (Ctx.size (funCtx ^. argumentStorageTypes)) index of
             SomeIndex idx Refl ->
               do
                 let regEntry = regmap Ctx.! idx
                 arg <-
                   liftIO $
-                    ppRegValue (Proxy :: Proxy arch) sym mem storageType regEntry
+                    ppRegValue (Proxy @arch) sym mem storageType regEntry
                 pure $
                   Const $
                     PP.hsep

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Setup.hs b/uc-crux-llvm/src/UCCrux/LLVM/Setup.hs
@@ -13,6 +13,7 @@ Stability    : provisional
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 
@@ -107,7 +108,7 @@ constrainHere ::
   Crucible.RegEntry sym (ToCrucibleType arch atTy) ->
   Setup m arch sym argTypes (Crucible.RegEntry sym (ToCrucibleType arch atTy))
 constrainHere sym _selector constraint fullTypeRepr regEntry@(Crucible.RegEntry _typeRepr regValue) =
-  liftIO (constraintToPred (Proxy :: Proxy arch) sym constraint fullTypeRepr regValue) >>=
+  liftIO (constraintToPred (Proxy @arch) sym constraint fullTypeRepr regValue) >>=
     assume constraint >>
     return regEntry
 
@@ -163,7 +164,7 @@ generateM' h1 gen =
     ( \(n :: NatRepr n) ->
         case NatRepr.leqAdd2
                (LeqProof :: LeqProof n h)
-               (NatRepr.leqRefl (Proxy :: Proxy 1) :: LeqProof 1 1) ::
+               (NatRepr.leqRefl (Proxy @1) :: LeqProof 1 1) ::
                LeqProof (n + 1) (h + 1) of
           LeqProof -> gen n
     )
@@ -306,11 +307,11 @@ generate sym modCtx ftRepr selector (ConstrainedShape shape) =
                   (selector & selectorCursor %~ deepenStruct idx)
                   (ConstrainedShape (fields ^. ixF' idx))
           let fieldVals =
-                FTCT.generate (Proxy :: Proxy arch) (Ctx.size fields) $
+                FTCT.generate proxy (Ctx.size fields) $
                   \idx _ Refl -> fields' ^. ixF' idx . Shape.tag . to getSymValue . to Crucible.RV
           pure $ Shape.ShapeStruct (SymValue fieldVals) fields'
   where
-    proxy = Proxy :: Proxy arch
+    proxy = Proxy @arch
     constrain ::
       Compose [] (Constraint m) atTy ->
       Shape m (SymValue sym arch) atTy ->
@@ -360,7 +361,7 @@ generateArgs _appCtx modCtx funCtx sym argSpecs =
       ( shapes,
         Crucible.RegMap $
           FTCT.generate
-            (Proxy :: Proxy arch)
+            (Proxy @arch)
             (Ctx.size (funCtx ^. argumentFullTypes))
             ( \index index' Refl ->
                 Crucible.RegEntry

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Setup/Monad.hs b/uc-crux-llvm/src/UCCrux/LLVM/Setup/Monad.hs
@@ -17,6 +17,7 @@ Stability    : provisional
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeFamilies #-}
 
@@ -347,8 +348,7 @@ store sym mts ptrRepr selector ptr regValue =
     \mem ->
       do
         ptr' <- annotatePointer sym selector ptrRepr ptr
-        let proxy = Proxy :: Proxy arch
-        mem' <- liftIO $ Mem.store' proxy sym mem mts ptrRepr ptr' regValue
+        mem' <- liftIO $ Mem.store' (Proxy @arch) sym mem mts ptrRepr ptr' regValue
         pure (ptr', mem')
 
 storeGlobal ::
@@ -373,5 +373,5 @@ storeGlobal sym ftRepr selector symb regValue =
       \mem' ->
         do
           mem'' <-
-            liftIO $ Mem.store (Proxy :: Proxy arch) sym mem' ftRepr ptr' regValue
+            liftIO $ Mem.store (Proxy @arch) sym mem' ftRepr ptr' regValue
           pure (ptr', mem'')