WIP: fix formatting

crucible-llvm/src/Lang/Crucible/LLVM.hs

@@ -60,8 +60,7 @@ import           What4.ProgramLoc (plSourceLoc)
 --   This will immediately build Crucible CFGs for each function
 --   defined in the module.
 registerModule ::
-   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
-   mem ~ Mem =>
+   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym, mem ~ Mem) =>
    (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling traslation warnings -} ->
    ModuleTranslation mem arch ->
    OverrideSim p sym (LLVM mem) rtp l a ()
@@ -72,8 +71,7 @@ registerModule handleWarning mtrans =
 --   module translation. This will immediately build a Crucible CFG for
 --   the named function.
 registerModuleFn ::
-   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
-   mem ~ Mem =>
+   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym, mem ~ Mem) =>
    (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling traslation warnings -} ->
    ModuleTranslation mem arch ->
    L.Symbol ->
@@ -101,8 +99,7 @@ registerModuleFn handleWarning mtrans sym =
 -- | Lazily register all the functions defined in the LLVM module.  See
 --   'registerLazyModuleFn' for a description.
 registerLazyModule ::
-   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
-   mem ~ Mem =>
+   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym, mem ~ Mem) =>
    (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling traslation warnings -} ->
    ModuleTranslation mem arch ->
    OverrideSim p sym (LLVM mem) rtp l a ()
@@ -118,8 +115,7 @@ registerLazyModule handleWarning mtrans =
 --   Note that the callback for printing translation warnings may be called at
 --   a much-later point, when the function in question is actually first invoked.
 registerLazyModuleFn ::
-   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym) =>
-   mem ~ Mem =>
+   (1 <= ArchWidth arch, HasPtrWidth (ArchWidth arch), IsSymInterface sym, mem ~ Mem) =>
    (LLVMTranslationWarning -> IO ()) {- ^ A callback for handling translation warnings -} ->
    ModuleTranslation mem arch ->
    L.Symbol ->
@@ -179,8 +175,7 @@ llvmGlobals
 llvmGlobals memVar mem = emptyGlobals & insertGlobal memVar mem
 
 llvmExtensionImpl ::
-  (HasLLVMAnn sym) =>
-  mem ~ Mem =>
+  (HasLLVMAnn sym, mem ~ Mem) =>
   MemOptions ->
   ExtensionImpl p sym (LLVM mem)
 llvmExtensionImpl mo =

crucible-llvm/src/Lang/Crucible/LLVM/ArraySizeProfile.hs

@@ -199,8 +199,7 @@ updateProfiles llvm cell state
 arraySizeProfile ::
   forall sym ext mem arch p rtp.
   ( C.IsSymInterface sym, C.HasLLVMAnn sym, C.HasPtrWidth (C.ArchWidth arch)
-  , ?memOpts :: C.MemOptions ) =>
-  mem ~ C.Mem =>
+  , ?memOpts :: C.MemOptions , mem ~ C.Mem) =>
   C.LLVMContext mem arch ->
   IORef (Map Text [FunctionProfile]) ->
   IO (C.ExecutionFeature p sym ext rtp)

crucible-llvm/src/Lang/Crucible/LLVM/Ctors.hs

@@ -158,9 +158,8 @@ callAllCtors = callCtors (const True)
 
 -- | Make a 'LLVMGenerator' into a CFG by making it a function with no arguments
 -- that returns unit.
-generatorToCFG :: forall mem arch wptr ret. (HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr)
-  => Mem.Mem mem
-               => Text
+generatorToCFG :: forall mem arch wptr ret. (HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr, Mem.Mem mem)
+  => Text
                -> HandleAllocator
                -> LLVMContext mem arch
                -> (forall s. LLVMGenerator s mem arch ret (Expr (LLVM mem) s ret))
@@ -184,9 +183,8 @@ generatorToCFG name halloc llvmctx gen ret = do
   return $! toSSA g
 
 -- | Create a CFG that calls some of the functions in @llvm.global_ctors@.
-callCtorsCFG :: forall mem arch wptr. (HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr)
-  => Mem.Mem mem
-             => (Ctor -> Bool) -- ^ Filter function
+callCtorsCFG :: forall mem arch wptr. (HasPtrWidth wptr, wptr ~ ArchWidth arch, 16 <= wptr, Mem.Mem mem)
+  => (Ctor -> Bool) -- ^ Filter function
              -> L.Module
              -> HandleAllocator
              -> LLVMContext mem arch

crucible-llvm/src/Lang/Crucible/LLVM/Eval.hs

@@ -64,8 +64,7 @@ assertSideCondition bak callStack (LLVMSideCondition (RV p) ub) =
 
 llvmExtensionEval ::
   forall sym bak p ext mem rtp blocks r ctx.
-  mem ~ Mem =>
-  (HasLLVMAnn sym, IsSymBackend sym bak) =>
+  (mem ~ Mem, HasLLVMAnn sym, IsSymBackend sym bak) =>
   bak ->
   IntrinsicTypes sym ->
   (Int -> String -> IO ()) ->

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs

@@ -68,8 +68,7 @@ llvmIntrinsicTypes =
 -- | Register all declare and define overrides
 register_llvm_overrides ::
   ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
-  , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
-  mem ~ Mem =>
+  , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions , mem ~ Mem) =>
   L.Module ->
   [OverrideTemplate p sym mem arch rtp l a] {- ^ Additional "define" overrides -} ->
   [OverrideTemplate p sym mem arch rtp l a] {- ^ Additional "declare" overrides -} ->
@@ -126,8 +125,7 @@ register_llvm_overrides_ llvmctx acts decls =
          runMaybeT (flip runReaderT (decl,declnm,llvmctx) $ asum (map overrideTemplateAction acts'))
 
 register_llvm_define_overrides ::
-  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch) =>
-  mem ~ Mem =>
+  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch, mem ~ Mem) =>
   L.Module ->
   [OverrideTemplate p sym mem arch rtp l a] ->
   LLVMContext mem arch ->
@@ -139,8 +137,7 @@ register_llvm_define_overrides llvmModule addlOvrs llvmctx =
 
 register_llvm_declare_overrides ::
   ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
-  , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
-  mem ~ Mem =>
+  , ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions , mem ~ Mem) =>
   L.Module ->
   [OverrideTemplate p sym mem arch rtp l a] ->
   LLVMContext mem arch ->
@@ -153,8 +150,7 @@ register_llvm_declare_overrides llvmModule addlOvrs llvmctx =
 -- | Register overrides for declared-but-not-defined functions
 declare_overrides ::
   ( IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch
-  , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions ) =>
-  mem ~ Mem =>
+  , ?lc :: TypeContext, ?intrinsicsOpts :: IntrinsicsOptions, ?memOpts :: MemOptions , mem ~ Mem) =>
   [OverrideTemplate p sym mem arch rtp l a]
 declare_overrides =
   concat
@@ -170,8 +166,7 @@ declare_overrides =
 -- | Register those overrides that should apply even when the corresponding
 -- function has a definition
 define_overrides ::
-  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch, ?lc :: TypeContext) =>
-  mem ~ Mem =>
+  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr, wptr ~ ArchWidth arch, ?lc :: TypeContext, mem ~ Mem) =>
   [OverrideTemplate p sym mem arch rtp l a]
 define_overrides =
   [ Libcxx.register_cpp_override Libcxx.putToOverride12

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Common.hs

@@ -258,8 +258,7 @@ register_1arg_polymorphic_override prefix overrideFn =
        _ -> empty
 
 basic_llvm_override :: forall p args ret sym mem arch wptr l a rtp.
-  mem ~ Mem =>
-  (IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
+  (mem ~ Mem, IsSymInterface sym, HasLLVMAnn sym, HasPtrWidth wptr) =>
   LLVMOverride p sym (LLVM mem) mem args ret ->
   OverrideTemplate p sym mem arch rtp l a
 basic_llvm_override ovr = OverrideTemplate matcher regOvr
@@ -313,8 +312,7 @@ isMatchingDeclaration requested provided = and
  matchingArgList (x:xs) (y:ys) = x `L.eqTypeModuloOpaquePtrs` y && matchingArgList xs ys
 
 register_llvm_override :: forall p args ret sym mem arch wptr l a rtp.
-  (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
-  mem ~ Mem =>
+  (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, mem ~ Mem) =>
   LLVMOverride p sym (LLVM mem) mem args ret ->
   RegOverrideM p sym mem arch rtp l a ()
 register_llvm_override llvmOverride = do
@@ -335,8 +333,7 @@ register_llvm_override llvmOverride = do
 -- | Bind a function handle, and also bind the function to the global function
 -- allocation in the LLVM memory.
 bind_llvm_handle ::
-  (IsSymInterface sym, HasPtrWidth wptr) =>
-  mem ~ Mem =>
+  (IsSymInterface sym, HasPtrWidth wptr, mem ~ Mem) =>
   GlobalVar mem ->
   L.Symbol ->
   FnHandle args ret ->
@@ -353,8 +350,7 @@ bind_llvm_handle mvar nm hdl impl = do
 -- Creates and binds a function handle, and also binds the function to the
 -- global function allocation in the LLVM memory.
 bind_llvm_func ::
-  (IsSymInterface sym, HasPtrWidth wptr) =>
-  mem ~ Mem =>
+  (IsSymInterface sym, HasPtrWidth wptr, mem ~ Mem) =>
   GlobalVar mem ->
   L.Symbol ->
   Ctx.Assignment TypeRepr args ->
@@ -380,8 +376,7 @@ bind_llvm_func mvar nm args ret impl = do
 -- Crucible CFGs written in crucible-syntax. For more usual cases, use
 -- 'Lang.Crucible.LLVM.Intrinsics.register_llvm_overrides'.
 do_register_llvm_override :: forall p args ret sym ext mem arch wptr l a rtp.
-  (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym) =>
-  mem ~ Mem =>
+  (IsSymInterface sym, HasPtrWidth wptr, HasLLVMAnn sym, mem ~ Mem) =>
   LLVMContext mem arch ->
   LLVMOverride p sym ext mem args ret ->
   OverrideSim p sym ext rtp l a ()
@@ -410,8 +405,7 @@ do_register_llvm_override llvmctx llvmOverride = do
 --
 -- c.f. 'Lang.Crucible.LLVM.Globals.allocLLVMFunPtr'
 alloc_and_register_override ::
-  (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions) =>
-  mem ~ Mem =>
+  (IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym, ?memOpts :: MemOptions, mem ~ Mem) =>
   bak ->
   LLVMContext mem arch ->
   LLVMOverride p sym (LLVM mem) mem args ret ->