Whitespace only

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

@@ -849,7 +849,7 @@ emptyMemoTable = IntMap.empty
 data MonadifyROState = MonadifyROState {
   -- | The monadification environment
   monStEnv :: MonadifyEnv,
-  -- | The monadification context 
+  -- | The monadification context
   monStCtx :: MonadifyCtx,
   -- | The current @SpecM@ function stack
   monStStack :: OpenTerm,

heapster-saw/src/Verifier/SAW/Heapster/IRTTranslation.hs

@@ -209,7 +209,7 @@ irtTMbCombine x =
 -- | Create an @args :++: ext@ binding
 irtNus :: (RAssign Name args -> RAssign Name ext -> b) ->
           IRTTyVarsTransM args ext (Mb (args :++: ext) b)
-irtNus f = 
+irtNus f =
   do args <- irtTArgsCtx <$> ask
      ext  <- irtTExtCtx  <$> ask
      return $ mbCombine ext (nus (RL.map (\_->Proxy) args) (nus ext . f))
@@ -560,7 +560,7 @@ irtCtor c all_args =
 -- recursive permission/shape body given here, and an 'IRTVarIdxs' which is
 -- the second result of the same call to 'translateCompletePermIRTTyVars',
 -- translate the given recursive permission body to an IRT type description
-translateCompleteIRTDesc :: IRTDescs a => SharedContext -> PermEnv -> 
+translateCompleteIRTDesc :: IRTDescs a => SharedContext -> PermEnv ->
                             Ident -> CruCtx args ->
                             Mb args a -> IRTVarIdxs -> IO TypedTerm
 translateCompleteIRTDesc sc env tyVarsIdent args p ixs =
@@ -738,7 +738,7 @@ instance IRTDescs (RAssign ValuePerm ps) where
 -- of corresponding calls to 'translateCompleteIRTDesc' and
 -- 'translateCompletePermIRTTyVars' or 'translateCompleteShapeIRTTyVars',
 -- return a term which is @IRT@ applied to these identifiers
-translateCompleteIRTDef :: SharedContext -> PermEnv -> 
+translateCompleteIRTDef :: SharedContext -> PermEnv ->
                            Ident -> Ident -> CruCtx args ->
                            IO TypedTerm
 translateCompleteIRTDef sc env tyVarsIdent descIdent args =
@@ -751,7 +751,7 @@ translateCompleteIRTDef sc env tyVarsIdent descIdent args =
 -- 'translateCompleteIRTDesc', and 'translateCompletePermIRTTyVars' or
 -- 'translateCompleteShapeIRTTyVars', return a term which is @foldIRT@ applied
 -- to these identifiers
-translateCompleteIRTFoldFun :: SharedContext -> PermEnv -> 
+translateCompleteIRTFoldFun :: SharedContext -> PermEnv ->
                                Ident -> Ident -> Ident -> CruCtx args ->
                                IO Term
 translateCompleteIRTFoldFun sc env tyVarsIdent descIdent _ args =
@@ -764,7 +764,7 @@ translateCompleteIRTFoldFun sc env tyVarsIdent descIdent _ args =
 -- 'translateCompleteIRTDesc', and 'translateCompletePermIRTTyVars' or
 -- 'translateCompleteShapeIRTTyVars', return a term which is @unfoldIRT@
 -- applied to these identifiers
-translateCompleteIRTUnfoldFun :: SharedContext -> PermEnv -> 
+translateCompleteIRTUnfoldFun :: SharedContext -> PermEnv ->
                                  Ident -> Ident -> Ident -> CruCtx args ->
                                  IO Term
 translateCompleteIRTUnfoldFun sc env tyVarsIdent descIdent _ args =
@@ -775,26 +775,26 @@ translateCompleteIRTUnfoldFun sc env tyVarsIdent descIdent _ args =
 -- | Get the terms for the arguments to @IRT@, @foldIRT@, and @unfoldIRT@
 -- given the appropriate identifiers
 irtDefArgs :: Ident -> Ident -> TypeTransM args (OpenTerm, OpenTerm, OpenTerm)
-irtDefArgs tyVarsIdent descIdent = 
+irtDefArgs tyVarsIdent descIdent =
   do args <- askExprCtxTerms
      let tyVars = applyOpenTermMulti (globalOpenTerm tyVarsIdent) args
          substs = ctorOpenTerm "Prelude.IRTs_Nil" [tyVars]
          desc   = applyOpenTermMulti (globalOpenTerm descIdent) args
      return (tyVars, substs, desc)
 
 irtDefinition :: Ident -> Ident -> TypeTransM args OpenTerm
-irtDefinition tyVarsIdent descIdent = 
+irtDefinition tyVarsIdent descIdent =
   do (tyVars, substs, desc) <- irtDefArgs tyVarsIdent descIdent
      return $ dataTypeOpenTerm "Prelude.IRT" [tyVars, substs, desc]
 
 irtFoldFun :: Ident -> Ident -> TypeTransM args OpenTerm
-irtFoldFun tyVarsIdent descIdent = 
+irtFoldFun tyVarsIdent descIdent =
   do (tyVars, substs, desc) <- irtDefArgs tyVarsIdent descIdent
      return $ applyOpenTermMulti (globalOpenTerm "Prelude.foldIRT")
                                  [tyVars, substs, desc]
 
 irtUnfoldFun :: Ident -> Ident -> TypeTransM args OpenTerm
-irtUnfoldFun tyVarsIdent descIdent = 
+irtUnfoldFun tyVarsIdent descIdent =
   do (tyVars, substs, desc) <- irtDefArgs tyVarsIdent descIdent
      return $ applyOpenTermMulti (globalOpenTerm "Prelude.unfoldIRT")
                                  [tyVars, substs, desc]

heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs

@@ -1551,7 +1551,7 @@ parseFunPermFromRust :: (Fail.MonadFail m, 1 <= w, KnownNat w) =>
 parseFunPermFromRust env w args ret str =
   do get3SomeFunPerm <- parseSome3FunPermFromRust env w str
      un3SomeFunPerm args ret get3SomeFunPerm
-  
+
 
 -- | Just like `parseFunPermFromRust`, but returns a `Some3FunPerm`
 parseSome3FunPermFromRust :: (Fail.MonadFail m, 1 <= w, KnownNat w) =>

saw-core-what4/src/Verifier/SAW/Simulator/What4/PosNat.hs

@@ -6,7 +6,7 @@
 -- Maintainer  : sweirich@galois.com
 -- Stability   : experimental
 -- Portability : non-portable (language extensions)
--- 
+--
 -- A runtime representation of positive nats
 ------------------------------------------------------------------------
 
@@ -36,7 +36,7 @@
 -- to allow implicitly provided nats
 {-# LANGUAGE AllowAmbiguousTypes #-}
 
--- to allow 'WithKnownNat' 
+-- to allow 'WithKnownNat'
 {-# OPTIONS_GHC -Wno-warnings-deprecations #-}
 
 module Verifier.SAW.Simulator.What4.PosNat where
@@ -58,7 +58,7 @@ data PosNat (n :: Nat) where
 
 -- | Check whether an integer is a positive nat
 somePosNat :: Integral a => a -> Maybe (Some PosNat)
-somePosNat n 
+somePosNat n
   | Just (Some nr) <- someNat n,
     Just LeqProof  <- testLeq (knownNat @1) nr
   = withKnownNat nr $ Just (Some (PosNat nr))
@@ -79,7 +79,7 @@ addPosNat =
   let w1  = knownNat @w1
       w2  = knownNat @w2
       sm  = addNat w1 w2 in
-  case leqAddPos w1 w2 of 
+  case leqAddPos w1 w2 of
     LeqProof -> withKnownNat sm $ PosNat sm
 
 -- I would hope that the 'leqAddPos' call can be compiled away...

saw-core/src/Verifier/SAW/Simulator/RME.hs

@@ -315,14 +315,14 @@ vSignedShiftR xs i
 
 toIntModOp :: RPrim
 toIntModOp =
-  Prims.natFun $ \n -> 
+  Prims.natFun $ \n ->
   Prims.intFun $ \x ->
     Prims.PrimValue (VIntMod n (x `mod` toInteger n))
 
 fromIntModOp :: RPrim
 fromIntModOp =
   Prims.constFun $
-  Prims.intModFun $ \x -> 
+  Prims.intModFun $ \x ->
     Prims.PrimValue (VInt x)
 
 intModEqOp :: RPrim

saw-core/src/Verifier/SAW/Term/Pretty.hs

@@ -311,9 +311,9 @@ withMemoVar global_p idx f =
       -- "pretend" we memoized by calling `updateMemoVar`, so that non-inlined
       -- memoization identifiers are kept constant between two
       -- otherwise-identical terms with differing inline strategies.
-      (skip:skips) 
+      (skip:skips)
         | skip == memoVar -> local (updateMemoVar . addIdxSkip . setMemoSkips skips) (f Nothing)
-      _ 
+      _
         | idx `Set.member` idxSkips -> f Nothing
         | otherwise -> local (updateMemoVar . bind memoVar) (f (Just memoVar))
   where
@@ -693,7 +693,7 @@ ppLets global_p ((idx, (t_rhs,_)):idxs) bindings baseDoc =
      if isBound then ppLets global_p idxs bindings baseDoc else
        do doc_rhs <- ppTerm' PrecTerm t_rhs
           withMemoVar global_p idx $ \memoVarM ->
-            let bindings' = case memoVarM of 
+            let bindings' = case memoVarM of
                   Just memoVar -> (memoVar, doc_rhs):bindings
                   Nothing -> bindings
             in  ppLets global_p idxs bindings' baseDoc

src/SAWScript/Builtins.hs

@@ -471,7 +471,7 @@ print_goal_inline noInline =
   execTactic $ tacticId $ \goal ->
     do
       opts <- getTopLevelPPOpts
-      let opts' = opts { ppNoInlineMemo = sort noInline } 
+      let opts' = opts { ppNoInlineMemo = sort noInline }
       sc <- getSharedContext
       nenv <- io (scGetNamingEnv sc)
       let output = prettySequent opts' nenv (goalSequent goal)

src/SAWScript/HeapsterBuiltins.hs

@@ -645,7 +645,7 @@ heapster_define_reachability_perm _bic _opts henv
               _ -> Fail.fail "Incorrect type for last argument of reachability perm"
        let args_ctx = appendParsedCtx pre_args_ctx last_args_ctx
        let args = parsedCtxCtx args_ctx
-       trans_tp <- liftIO $ 
+       trans_tp <- liftIO $
          translateCompleteTypeInCtx sc env args $
          nus (cruCtxProxies args) $ const $ ValuePermRepr tp
        trans_tp_ident <- parseAndInsDef henv nm trans_tp trans_tp_str
@@ -1054,7 +1054,7 @@ heapster_translate_rust_type _bic _opts henv perms_string =
         Some3FunPerm fun_perm <-
           parseSome3FunPermFromRust env w64 perms_string
         liftIO $ putStrLn $ permPrettyString emptyPPInfo fun_perm
-        
+
 -- | Create a new SAW core primitive named @nm@ with type @tp@ in the module
 -- associated with the supplied Heapster environment, and return its identifier
 insPrimitive :: HeapsterEnv -> String -> Term -> TopLevel Ident

src/SAWScript/Prover/MRSolver/Monad.hs

@@ -451,7 +451,7 @@ runMRM sc env timeout askSMT rs m =
 
 -- | Run an 'MRM' computation and return a result or an error, discarding the
 -- final state
-evalMRM :: 
+evalMRM ::
   SharedContext ->
   MREnv {- ^ The Mr Solver environment -} ->
   Maybe Integer {- ^ Timeout in milliseconds for each SMT call -} ->
@@ -465,7 +465,7 @@ evalMRM sc env timeout askSMT rs =
 
 -- | Run an 'MRM' computation and return a final state or an error, discarding
 -- the result
-execMRM :: 
+execMRM ::
   SharedContext ->
   MREnv {- ^ The Mr Solver environment -} ->
   Maybe Integer {- ^ Timeout in milliseconds for each SMT call -} ->

src/SAWScript/Prover/MRSolver/SMT.hs

@@ -319,7 +319,7 @@ smtNormPrims sc = Map.fromList
                          Just n -> scNat sc n >>= \n' -> scBvNat sc n' ix'
                tm <- scApplyBeta sc f ix''
                tm' <- smtNorm sc tm
-               return $ VExtra $ VExtraTerm a tm') 
+               return $ VExtra $ VExtraTerm a tm')
     ),
     -- Don't normalize applications of @SpecM@ and its arguments
     ("Prelude.SpecM",
@@ -613,7 +613,7 @@ mrConvOfTerm _ = NoConv
 -- as large as possible, using information from the given terms (i.e. using
 -- 'mrConvOfTerm') where possible. In pictorial form, this function finds
 -- a @tp@, @c1@, and @c2@ which satisfy the following diagram:
--- 
+--
 -- >  tp1      tp2
 -- >   ^        ^
 -- > c1 \      / c2
@@ -655,10 +655,10 @@ findInjConvs tp1 t1 (asNatType -> Just ())
 -- add a 'BVToNat' conversion we have a BV on the other side, using the
 -- bit-width from the other side
 findInjConvs (asNatType -> Just ()) _ (asBitvectorType -> Just n) _ =
-  do bv_tp <- liftSC1 scBitvector n 
+  do bv_tp <- liftSC1 scBitvector n
      return $ Just (bv_tp, BVToNat n, NoConv)
 findInjConvs (asBitvectorType -> Just n) _ (asNatType -> Just ()) _ =
-  do bv_tp <- liftSC1 scBitvector n 
+  do bv_tp <- liftSC1 scBitvector n
      return $ Just (bv_tp, NoConv, BVToNat n)
 -- add a 'BVVecToVec' conversion if the (optional) given term has a
 -- 'BVVecToVec' conversion
@@ -882,7 +882,7 @@ mrProveRelH' _ _ _ _ (asNum -> Just (Left t1)) (asNum -> Just (Left t2)) =
   mrProveEqSimple (liftSC2 scEqualNat) t1 t2
 mrProveRelH' _ _ (asNatType -> Just _) (asNatType -> Just _) t1 t2 =
   mrProveEqSimple (liftSC2 scEqualNat) t1 t2
-mrProveRelH' _ _ tp1@(asVectorType -> Just (n1, asBoolType -> Just ())) 
+mrProveRelH' _ _ tp1@(asVectorType -> Just (n1, asBoolType -> Just ()))
                 tp2@(asVectorType -> Just (n2, asBoolType -> Just ())) t1 t2 =
   do ns_are_eq <- mrConvertible n1 n2
      if ns_are_eq then return () else

src/SAWScript/Prover/MRSolver/Solver.hs

@@ -35,7 +35,7 @@ defined in the SAW core prelude:
 > (if b then m1 else m2) >>= k  = if b then m1 >>= k else m2 >>= k
 > (either f1 f2 e) >>= k        = either (\x -> f1 x >>= k) (\x -> f2 x >>= k) e
 > (multiFixS funs body) >>= k   = multiFixS funs (\F1 ... Fn -> body F1 ... Fn >>= k)
-> 
+>
 > liftStackS (retS x)                = retS x
 > liftStackS (errorS str)            = errorS str
 > liftStackS (m >>= k)               = liftStackS m >>= \x -> liftStackS (k x)
@@ -74,65 +74,65 @@ The goal of the solver at any point is of the form @C |- m1 |= m2@, meaning that
 we are trying to prove @m1@ refines @m2@ in context @C@. This proceeds by cases:
 
 > C |- retS e1 |= retS e2: prove C |- e1 = e2
-> 
+>
 > C |- errorS str1 |= errorS str2: vacuously true
-> 
+>
 > C |- if b then m1' else m1'' |= m2: prove C,b=true |- m1' |= m2 and
 > C,b=false |- m1'' |= m2, skipping either case where C,b=X is unsatisfiable;
-> 
+>
 > C |- m1 |= if b then m2' else m2'': similar to the above
-> 
+>
 > C |- either T U (SpecM V) f1 f2 e |= m: prove C,x:T,e=inl x |- f1 x |= m and
 > C,y:U,e=inl y |- f2 y |= m, again skippping any case with unsatisfiable context;
-> 
+>
 > C |- m |= either T U (SpecM V) f1 f2 e: similar to previous
-> 
+>
 > C |- m |= forallS f: make a new universal variable x and recurse
-> 
+>
 > C |- existsS f |= m: make a new universal variable x and recurse (existential
 > elimination uses universal variables and vice-versa)
-> 
+>
 > C |- m |= existsS f: make a new existential variable x and recurse
-> 
+>
 > C |- forallS f |= m: make a new existential variable x and recurse
-> 
+>
 > C |- m |= orS m1 m2: try to prove C |- m |= m1, and if that fails, backtrack and
 > prove C |- m |= m2
-> 
+>
 > C |- orS m1 m2 |= m: prove both C |- m1 |= m and C |- m2 |= m
-> 
+>
 > C |- multiFixS (\F1 ... Fn -> (f1, ..., fn)) (\F1 ... Fn -> body) |= m: create
 > multiFixS-bound variables F1 through Fn in the context bound to their unfoldings
 > f1 through fn, respectively, and recurse on body |= m
-> 
+>
 > C |- m |= multiFixS (\F1 ... Fn -> (f1, ..., fn)) (\F1 ... Fn -> body): similar to
 > previous case
-> 
+>
 > C |- F e1 ... en >>= k |= F e1' ... en' >>= k': prove C |- ei = ei' for each i
 > and then prove k x |= k' x for new universal variable x
-> 
+>
 > C |- F e1 ... en >>= k |= F' e1' ... em' >>= k':
-> 
+>
 > * If we have an assumption that forall x1 ... xj, F a1 ... an |= F' a1' .. am',
 >   prove ei = ai and ei' = ai' and then that C |- k x |= k' x for fresh uvar x
-> 
+>
 > * If we have an assumption that forall x1, ..., xn, F e1'' ... en'' |= m' for
 >   some ei'' and m', match the ei'' against the ei by instantiating the xj with
 >   fresh evars, and if this succeeds then recursively prove C |- m' >>= k |= RHS
-> 
+>
 > (We don't do this one right now)
 > * If we have an assumption that forall x1', ..., xn', m |= F e1'' ... en'' for
 >   some ei'' and m', match the ei'' against the ei by instantiating the xj with
 >   fresh evars, and if this succeeds then recursively prove C |- LHS |= m' >>= k'
-> 
+>
 > * If either side is a definition whose unfolding does not contain multiFixS, or
 >   any related operations, unfold it
-> 
+>
 > * If F and F' have the same return type, add an assumption forall uvars in scope
 >   that F e1 ... en |= F' e1' ... em' and unfold both sides, recursively proving
 >   that F_body e1 ... en |= F_body' e1' ... em'. Then also prove k x |= k' x for
 >   fresh uvar x.
-> 
+>
 > * Otherwise we don't know to "split" one of the sides into a bind whose
 >   components relate to the two components on the other side, so just fail