diff --git a/uc-crux-llvm/.hlint.yaml b/uc-crux-llvm/.hlint.yaml index c554c8522..15e5784ec 100644 --- 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 index 266fb5128..27c29649f 100644 --- 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 index f77546387..3e25c7737 100644 --- 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 index f98d1e7fc..093ff7e57 100644 --- 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 index d814326b8..a9ef7df0e 100644 --- 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 index 19a22e32b..d20b0853d 100644 --- 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 index aaa873af5..8e351a8e0 100644 --- 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'')