[ lint ] Add linter to the CI

Author: buzden

.github/workflows/ci-super-linter.yml

@@ -0,0 +1,45 @@
+---
+name: Lint
+
+on:
+  push:
+    branches:
+      - '**'
+    tags:
+      - '**'
+  pull_request:
+    branches:
+      - main
+      - master
+  # Allows you to run this workflow manually from the Actions tab
+  workflow_dispatch:
+
+permissions:
+  statuses: write
+
+concurrency:
+  group: ${{ github.workflow }}@${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    name: Lint Code Base
+    # Disable PR from the same repo
+    if: github.event_name != 'pull_request' ||
+        github.event.pull_request.head.repo.full_name != github.event.pull_request.base.repo.full_name
+    runs-on: ubuntu-latest
+    steps:
+
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          # Full git history is needed to get a proper
+          # list of changed files within `super-linter`
+          fetch-depth: 0
+
+      - name: Lint Code Base
+        uses: super-linter/super-linter/slim@v8
+        env:
+          DEFAULT_BRANCH: master
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          IGNORE_GENERATED_FILES: true

src/Test/Common/UniqueFins.idr

@@ -6,7 +6,7 @@ import Test.DepTyCheck.Gen
 import public Test.Common.Utils
 
 public export
-data UniqueFins : (n : Nat) -> (fs : FinsList n) -> Type where 
+data UniqueFins : (n : Nat) -> (fs : FinsList n) -> Type where
   Nil  : UniqueFins n []
   (::) : (f : Fin n) -> FinNotIn rest f => UniqueFins n rest -> UniqueFins n (f::rest)
 

src/Test/Common/Utils.idr

@@ -31,7 +31,7 @@ namespace FinsList
   data FinNotIn : FinsList srcs -> Fin srcs -> Type where
     FNIEmpty : FinNotIn [] f
     FNICons  : {x, f : Fin srcs} -> (0 _ : So $ x /= f) -> (fni: FinNotIn xs f) -> FinNotIn (x :: xs) f
-  
+
   -- public export
   -- data FinInFL : FinsList l -> Fin l -> Type where
   --   Here  : (n, n' : Fin l) => (0 _ : So $ n == n') => FinInFL (n::ns) n'

src/Test/Verilog/Connections.idr

@@ -211,7 +211,7 @@ isMD (Net Wor'     t) = True
 isMD _                = False
 
 ||| 10.3.2 The continuous assignment statement
-||| Variables can only be driven by one continuous assignment or by one primitive output or module output. 
+||| Variables can only be driven by one continuous assignment or by one primitive output or module output.
 ||| IEEE 1800-2023
 public export
 data SingleDriven : SVObject -> Type where
@@ -220,7 +220,7 @@ data SingleDriven : SVObject -> Type where
 
 public export
 isSD : SVObject -> Bool
-isSD (Var st)        = True 
+isSD (Var st)        = True
 isSD (Net Uwire' st) = True
 isSD _               = False
 
@@ -336,10 +336,10 @@ ultraSuperReplace SSC = superReplaceSC
 
 public export
 typeOfPort : (ms : ModuleSigsList) -> (m : ModuleSig) -> (subMs : FinsList ms.length) -> FillMode ms m subMs n -> Fin n ->  SVObject
-typeOfPort ms m subMs TSK = typeOf (topSnks m)          
+typeOfPort ms m subMs TSK = typeOf (topSnks m)
 typeOfPort ms m subMs SSK = typeOf (subSnks ms m subMs)
-typeOfPort ms m subMs TSC = typeOf (topSrcs m)          
-typeOfPort ms m subMs SSC = typeOf (subSrcs ms m subMs) 
+typeOfPort ms m subMs TSC = typeOf (topSrcs m)
+typeOfPort ms m subMs SSC = typeOf (subSrcs ms m subMs)
 
 public export
 noSource : MultiConnection ms m subMs -> Bool
@@ -362,7 +362,7 @@ data FitAny : {ms : ModuleSigsList} -> {m : ModuleSig} -> {subMs : FinsList ms.l
   ExistingAny : (f : Fin $ length rest) ->
                 (cap : CanAddPort {ms} {m} {subMs} mode $ index rest f) ->
                 (jmc : JustMC (ultraSuperReplace {ms} {m} {subMs} mode i $ index rest f) newMC) ->
-                (cc : CanConnect (valueOf $ typeOf $ index rest f) (valueOf $ typeOfPort ms m subMs mode i)) -> 
+                (cc : CanConnect (valueOf $ typeOf $ index rest f) (valueOf $ typeOfPort ms m subMs mode i)) ->
                 FitAny {ms} {m} {subMs} rest i mode $ replaceAt rest f newMC
 
 public export
@@ -382,7 +382,7 @@ data FillAny : {ms : ModuleSigsList} -> {m : ModuleSig} -> {subMs : FinsList ms.
                (pre : MultiConnectionsList ms m subMs) -> {n : _} -> (i : Nat) ->
                FillMode ms m subMs n -> (aft : MultiConnectionsList ms m subMs) -> Type where
   FANil  : FillAny pre Z mode pre
-  FACons : {jf : JustFin (natToFin' i n) f} -> (fit : FitAny {ms} {m} {subMs} {n} mid f mode aft) -> 
+  FACons : {jf : JustFin (natToFin' i n) f} -> (fit : FitAny {ms} {m} {subMs} {n} mid f mode aft) ->
            (rest : FillAny {ms} {m} {subMs} pre {n} i mode mid) ->
            FillAny {ms} {m} {subMs} pre {n} (S i) mode aft
 
@@ -418,7 +418,7 @@ genJF : Fuel -> {n : _} -> (mf : MFin n) -> Gen MaybeEmpty (f : Fin n ** JustFin
 
 export
 genFillAny : Fuel -> {ms : ModuleSigsList} -> {m : ModuleSig} -> {subMs : FinsList ms.length} ->
-                     (pre : MultiConnectionsList ms m subMs) -> {n : _} -> (i : Nat) -> (mode : FillMode ms m subMs n) -> 
+                     (pre : MultiConnectionsList ms m subMs) -> {n : _} -> (i : Nat) -> (mode : FillMode ms m subMs n) ->
                      Gen MaybeEmpty (aft : MultiConnectionsList ms m subMs ** FillAny {ms} {m} {subMs} {n} pre i mode aft)
 genFillAny x pre Z     mode = pure (pre ** FANil)
 genFillAny x pre (S i) mode = do
@@ -430,6 +430,6 @@ genFillAny x pre (S i) mode = do
 export
 genModules : Fuel -> (ms : ModuleSigsList) ->
   (Fuel -> {ms' : ModuleSigsList} -> {m' : ModuleSig} -> {subMs' : FinsList ms'.length} ->
-  (pre' : MultiConnectionsList ms' m' subMs') -> {n' : _} -> (i' : Nat) -> (mode' : FillMode ms' m' subMs' n') -> 
+  (pre' : MultiConnectionsList ms' m' subMs') -> {n' : _} -> (i' : Nat) -> (mode' : FillMode ms' m' subMs' n') ->
   Gen MaybeEmpty (aft' : MultiConnectionsList ms' m' subMs' ** FillAny {ms=ms'} {m=m'} {subMs=subMs'} {n=n'} pre' i' mode' aft')) =>
   Gen MaybeEmpty $ Modules ms

src/Test/Verilog/Literal.idr

@@ -30,13 +30,13 @@ namespace BinaryList
 namespace TypeLiteralVect
 
   public export
-  data TypeLiteral : SVType -> Type 
+  data TypeLiteral : SVType -> Type
 
   public export
   data TypeLiteralVect : Nat -> SVType-> Type where
     Nil  : TypeLiteralVect 0 t
     (::) : TypeLiteral t -> TypeLiteralVect n t -> TypeLiteralVect (S n) t
-  
+
   export
   toList : TypeLiteralVect l t -> List $ TypeLiteral t
   toList []      = []

src/Test/Verilog/Pretty.idr

@@ -160,7 +160,7 @@ showSVType ua@(UnpackedArr t     s e) name = "\{showPackedSVT $ basic t} \{name}
   basic : SVType -> SVType
   basic (UnpackedArr t _ _) = basic t
   basic t                   = t
-  
+
   unpDimensions : SVType -> String
   unpDimensions (UnpackedArr t s e) = "[\{show s}:\{show e}]" ++ unpDimensions t
   unpDimensions _                   = ""
@@ -264,7 +264,7 @@ iMcsByF mcs func fin = findIndex resolve $ toVect mcs where
     resolve : MultiConnection ms m subMs -> Bool
     resolve sc = isElem fin $ func sc
 
-findMcsNameByF : (extractField : MultiConnection ms m subMs -> List $ Fin iport) -> 
+findMcsNameByF : (extractField : MultiConnection ms m subMs -> List $ Fin iport) ->
                  (mcs : MultiConnectionsList ms m subMs) -> Vect (length mcs) String -> Fin iport -> String
 findMcsNameByF extract mcs mcsNames fin = case iMcsByF mcs extract fin of
   Just mcsFin => index mcsFin mcsNames
@@ -319,8 +319,8 @@ parameters {opts : LayoutOpts} (m : ModuleSig) (ms: ModuleSigsList)  (subMs : Fi
                  (ctxInps : List SVObject) -> (ctxOuts : List SVObject) -> (exInps : List String) -> (exOuts : List String) -> List (Doc opts)
     printSubm' pre siNames soNames exM ctxInps ctxOuts exInps exOuts = do
       let warningsSubOuts = printAllImplicitCasts showSVObj (toList exM.outputs) exOuts ctxOuts soNames
-      let warningsSubInps = printAllImplicitCasts showSVObj ctxInps siNames (toList exM.inputs) exInps  
-      let warnings = if isNil warningsSubOuts || 
+      let warningsSubInps = printAllImplicitCasts showSVObj ctxInps siNames (toList exM.inputs) exInps
+      let warnings = if isNil warningsSubOuts ||
                         isNil warningsSubInps then warningsSubOuts ++ warningsSubInps else warningsSubOuts ++ [ "//" ] ++ warningsSubInps
       case isNil warnings of
         True  => [ pre, line "" ]
@@ -388,8 +388,8 @@ resolveOutputNames mcs mcsNames = map (findTOName mcs mcsNames) $ allFins (m.out
 ||| Net types aren't compatible with unpacked arrays. So connections to unpacked array ports must be declared explicitly.
 unpackedDecls : (mcs : MultiConnectionsList ms m subMs) -> Vect (length mcs) String -> List String
 unpackedDecls []          _             = []
-unpackedDecls (mc@(MkMC Nothing ssk Nothing ssc) :: mcs) (name::names) = if (isUnpacked $ typeOf mc) 
-  then (showSVObj (typeOf mc) name) :: unpackedDecls mcs names 
+unpackedDecls (mc@(MkMC Nothing ssk Nothing ssc) :: mcs) (name::names) = if (isUnpacked $ typeOf mc)
+  then (showSVObj (typeOf mc) name) :: unpackedDecls mcs names
   else unpackedDecls mcs names
 unpackedDecls (mc :: mcs) (name::names) = unpackedDecls mcs names
 

src/Test/Verilog/TMPExpression.idr

@@ -20,5 +20,5 @@ data TMPExList : (mcs : MultiConnectionsList ms m subMs) -> FinsList (length mcs
   (::) : TMPExpression mcs (valueOf $ typeOf $ index mcs f) -> TMPExList mcs fs -> TMPExList mcs (f::fs)
 
 export
-genTMPExList : Fuel -> {ms : _} -> {m : _} -> {subMs : _} -> 
+genTMPExList : Fuel -> {ms : _} -> {m : _} -> {subMs : _} ->
                (mcs : MultiConnectionsList ms m subMs) -> (fs : FinsList $ length mcs) -> Gen MaybeEmpty $ TMPExList mcs fs

src/Test/Verilog/Warnings.idr

@@ -8,7 +8,7 @@ import Test.Verilog.SVType
 -- |||
 -- ||| module a(output logic [1:0] a1);
 -- ||| endmodule: a
--- ||| 
+-- |||
 -- ||| module b(input bit b1);
 -- ||| endmodule: b
 -- |||