Swap argument order for SAWCore Vec type.

cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs

@@ -1331,7 +1331,7 @@ importExpr sc expr =
                 -- of type `seq (TCNum 2) a`.
                if | Just (n, a) <- asSeqType t ->
                       return (n, a)
-                  | Just (n, a) <- asVectorType t -> do
+                  | Just (a, n) <- asVectorType t -> do
                       n' <- scGlobalApply sc "Cryptol.TCNum" [n]
                       return (n', a)
                   | otherwise -> do

otherTests/saw-core/Tests/Rewriter.hs

@@ -41,7 +41,7 @@ prelude_bveq_sameL_test =
     natType <- scNatType sc
     n <- scFreshVariable sc "n" natType
     boolType <- scBoolType sc
-    bvType <- scVecType sc n boolType
+    bvType <- scVecType sc boolType n
     x <- scFreshVariable sc "x" bvType
     z <- scFreshVariable sc "z" bvType
     let lhs =

saw-central/src/SAWCentral/Crucible/LLVM/FFI.hs

@@ -215,7 +215,7 @@ mkSizeArg tyArgTerm = do
   openToSetupTerm $
     OT.applyGlobal "Cryptol.ecNumber"
       [ OT.term tyArgTerm
-      , OT.vectorType sizeBitSize OT.boolType
+      , OT.vectorType OT.boolType sizeBitSize
       , OT.applyGlobal "Cryptol.PLiteralSeqBool"
           [OT.applyGlobal "Cryptol.TCNum" [sizeBitSize]]
       ]
@@ -491,7 +491,7 @@ arrayTypeInfo tenv lenTypes ffiBasicType = do
   FFITypeInfo {..} <- basicTypeInfo ffiBasicType
   pure FFITypeInfo
     { ffiLLVMType = llvm_array totalLen ffiLLVMType
-    , ffiLLVMCoreType = OT.vectorType totalLenTerm ffiLLVMCoreType
+    , ffiLLVMCoreType = OT.vectorType ffiLLVMCoreType totalLenTerm
     , ffiConv =
         case (lenTerms, ffiConv) of
           -- If the array is flat and there is no need to convert individual
@@ -502,7 +502,7 @@ arrayTypeInfo tenv lenTypes ffiBasicType = do
                 basicToLLVM = maybe (Just id) ffiToLLVM ffiConv
                 cumulLenTerms = map OT.nat $ scanl1 (*) lens
                 arrCryType :| cumulElemTypes =
-                  NE.scanr OT.vectorType basicCryType lenTerms
+                  NE.scanr (flip OT.vectorType) basicCryType lenTerms
 
                 noArrayLengths :: a
                 noArrayLengths =

saw-central/src/SAWCentral/Crucible/LLVM/Override.hs

@@ -1365,7 +1365,7 @@ typeToSC sc t =
     Crucible.Array sz ty ->
       do n <- scNat sc (fromIntegral sz)
          ty' <- typeToSC sc ty
-         scVecType sc n ty'
+         scVecType sc ty' n
     Crucible.Struct fields ->
       do fields' <- V.toList <$> traverse (typeToSC sc . view Crucible.fieldVal) fields
          scTupleType sc fields'

saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs

@@ -2092,7 +2092,7 @@ setupArg sc cc ecRef mty0 tp0 =
               (eltCty, eltScTp) <- typeShapeToSAWTypes eltShp
               arraySzTerm <- scNat sc $ fromIntegral @Int @Natural arraySz
               let cty = Cryptol.tSeq (Cryptol.tNum (toInteger @Int arraySz)) eltCty
-              scTp <- scVecType sc arraySzTerm eltScTp
+              scTp <- scVecType sc eltScTp arraySzTerm
               pure (cty, scTp)
 
             StructShape mty _ ->
@@ -2152,7 +2152,7 @@ setupArg sc cc ecRef mty0 tp0 =
             PrimShape {} ->
               termToRegValue sym (shapeType shp) t
             ArrayShape _ _ eltSz eltShp len -> do
-              (arraySz :*: eltScTp) <-
+              (eltScTp :*: arraySz) <-
                 case asVecType scTp of
                   Just nt -> pure nt
                   Nothing -> do

saw-central/src/SAWCentral/Crucible/MIR/TypeShape.hs

@@ -486,7 +486,7 @@ shapeToTerm' sc = go
     mkVec n ty =
       do
         n' <- SAW.scNat sc (fromIntegral n)
-        SAW.scVecType sc n' ty
+        SAW.scVecType sc ty n'
 
     goAgElem :: CryTermAdaptor Integer -> AgElemShape -> m SAW.Term
     goAgElem ada (AgElemShape _ _ shp) = go ada shp

saw-central/src/SAWCentral/Yosys/State.hs

@@ -198,12 +198,12 @@ composeYosysSequentialHelper sc s n =
      width <- SC.scNat sc $ fromIntegral n
      extendedInputFields <-
        forM (s ^. yosysSequentialInputFields) $ \(ty, cty) ->
-       do exty <- SC.scVecType sc width ty
+       do exty <- SC.scVecType sc ty width
           let excty = C.tSeq (C.tNum n) cty
           pure (exty, excty)
      extendedOutputFields <-
        forM (s ^. yosysSequentialOutputFields) $ \(ty, cty) ->
-       do exty <- SC.scVecType sc width ty
+       do exty <- SC.scVecType sc ty width
           let excty = C.tSeq (C.tNum n) cty
           pure (exty, excty)
      extendedInputType <- fieldsToType sc extendedInputFields

saw-central/src/SAWCentral/Yosys/Utils.hs

@@ -399,7 +399,7 @@ scPreterms sc preterms = snd <$> go preterms
            -- Use `join` to concatenate same-length preterms
            do i' <- SC.scNat sc i
               boolty <- SC.scBoolType sc
-              ety <- SC.scVecType sc i' boolty
+              ety <- SC.scVecType sc boolty i'
               ps1' <- traverse (scPreterm sc) ps1
               v <- SC.scVector sc ety (p' : ps1')
               let len = List.genericLength ps1 + 1 :: Natural

saw-core-what4/src/SAWCoreWhat4/Common.hs

@@ -113,7 +113,7 @@ termOfTValue sc val =
     VVecType n a ->
       do n' <- scNat sc n
          a' <- termOfTValue sc a
-         scVecType sc n' a'
+         scVecType sc a' n'
     VDataType (ModuleIdentifier "Prelude.UnitType") [] []
       -> scUnitType sc
     VDataType (ModuleIdentifier "Prelude.PairType") [TValue a, TValue b] []

saw-core-what4/src/SAWCoreWhat4/ReturnTrip.hs

@@ -640,7 +640,8 @@ evaluateExpr sym st sc cache = f Map.empty
           case B.bvarType bvar of
             BaseBVRepr wrepr -> do
               w <- SC.scNat sc $ natValue wrepr
-              ty <- SC.scVecType sc w =<< SC.scBoolType sc
+              boolty <- SC.scBoolType sc
+              ty <- SC.scVecType sc boolty w
               x <- SC.scFreshVariable sc nm ty
               SAWExpr <$>
                 (SC.scBvForall sc w