Skip to content

Commit c3a0ee5

Browse files
ana-pantilieana-pantilie
authored
Add -Wall to Haskell metatheory modules and fix warnings (#7302)
* Add -Wall to Haskell metatheory modules and fix warnings * Regenerate MAlonzo
1 parent c42ff4f commit c3a0ee5

File tree

8 files changed

+76
-83
lines changed

8 files changed

+76
-83
lines changed

‎plutus-metatheory/src/Certifier.hs‎

Lines changed: 19 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
{-# OPTIONS_GHC -Wall #-}
2+
13
module Certifier (
24
runCertifier
35
, mkCertifier
@@ -6,14 +8,13 @@ module Certifier (
68
, CertifierError (..)
79
) where
810

9-
import Control.Monad ((>=>))
1011
import Control.Monad.Except (ExceptT (..), runExceptT, throwError)
1112
import Control.Monad.IO.Class (liftIO)
1213
import Data.Char (toUpper)
1314
import Data.List (find)
1415
import Data.List.NonEmpty (NonEmpty (..))
1516
import Data.List.NonEmpty qualified as NE
16-
import Data.Maybe (fromJust)
17+
import Data.Maybe (fromMaybe)
1718
import Data.Time.Clock.System (getSystemTime, systemNanoseconds)
1819
import System.Directory (createDirectory)
1920
import System.FilePath ((</>))
@@ -35,9 +36,7 @@ data CertifierError
3536
| InvalidCompilerOutput
3637
| ValidationError CertName
3738

38-
newtype CertifierSuccess = CertifierSuccess
39-
{ certDir :: CertDir
40-
}
39+
newtype CertifierSuccess = CertifierSuccess CertDir
4140

4241
prettyCertifierError :: CertifierError -> String
4342
prettyCertifierError (InvalidCertificate certDir) =
@@ -140,10 +139,10 @@ mkCertificate certName rawTrace =
140139
-> [(SimplifierStage, (UTerm, UTerm))]
141140
-> [(SimplifierStage, (TermWithId, TermWithId))]
142141
go _ [] = []
143-
go id ((stage, (before, after)) : rest) =
144-
let beforeWithId = TermWithId id before
145-
afterWithId = TermWithId (id + 1) after
146-
in (stage, (beforeWithId, afterWithId)) : go (id + 2) rest
142+
go id' ((stage, (before, after)) : rest) =
143+
let beforeWithId = TermWithId id' before
144+
afterWithId = TermWithId (id' + 1) after
145+
in (stage, (beforeWithId, afterWithId)) : go (id' + 2) rest
147146

148147
extractTermWithIds
149148
:: [(SimplifierStage, (TermWithId, TermWithId))]
@@ -163,17 +162,24 @@ mkCertificate certName rawTrace =
163162
getRepresentatives :: [NonEmpty Ast] -> [Ast]
164163
getRepresentatives = fmap NE.head
165164

166-
mkAsts :: [TermWithId] -> [Ast]
167-
mkAsts = findEquivClasses >=> NE.toList
165+
errorMessage :: String
166+
errorMessage =
167+
"Internal error: could not find AST.\
168+
\ This is an issue in the certifier, please open a bug report at\
169+
\ https://github.com/IntersectMBO/plutus/issues"
168170

169171
mkAstTrace
170172
:: [Ast]
171173
-> [(SimplifierStage, (TermWithId, TermWithId))]
172174
-> [(SimplifierStage, (Ast, Ast))]
173175
mkAstTrace _ [] = []
174176
mkAstTrace allAsts ((stage, (rawBefore, rawAfter)) : rest) =
175-
let Just processedBefore = find (\ast -> getTermId ast == termId rawBefore) allAsts
176-
Just processedAfter = find (\ast -> getTermId ast == termId rawAfter) allAsts
177+
let processedBefore =
178+
fromMaybe (error errorMessage)
179+
$ find (\ast -> getTermId ast == termId rawBefore) allAsts
180+
processedAfter =
181+
fromMaybe (error errorMessage)
182+
$ find (\ast -> getTermId ast == termId rawAfter) allAsts
177183
in (stage, (processedBefore, processedAfter)) : mkAstTrace allAsts rest
178184

179185
mkAstModuleName :: Ast -> String
@@ -306,8 +312,6 @@ writeCertificateProject
306312
= liftIO $ do
307313
let (mainModulePath, mainModuleContents) = mainModule
308314
(agdalibPath, agdalibContents) = agdalib
309-
astModulePaths = fmap fst astModules
310-
astModuleContents = fmap snd astModules
311315
time <- systemNanoseconds <$> getSystemTime
312316
let actualProjectDir = projectDir <> "-" <> show time
313317
createDirectory actualProjectDir

‎plutus-metatheory/src/FFI/AgdaUnparse.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
{-# LANGUAGE FlexibleInstances #-}
2+
{-# OPTIONS_GHC -Wall #-}
23

34
module FFI.AgdaUnparse where
45

56
import Data.ByteString (ByteString)
6-
import Data.Functor.Identity
77
import Data.Proxy
88
import Data.Text (Text)
99
import Data.Text qualified as T

‎plutus-metatheory/src/FFI/Opts.hs‎

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,15 @@
11
-- editorconfig-checker-disable-file
22
{-# LANGUAGE OverloadedStrings #-}
3+
{-# OPTIONS_GHC -Wall #-}
34

45
module FFI.Opts where
56

6-
import Data.Semigroup ((<>))
7-
import Data.Text qualified as T
8-
import Data.Text.IO qualified as T
9-
107
import Data.Foldable (asum)
118
import Options.Applicative hiding (asum)
129

1310
import PlutusCore.Executable.Common
1411
import PlutusCore.Executable.Parsers
1512

16-
import System.Exit (exitFailure)
17-
import System.IO (stderr)
18-
1913
import PlutusCore.Evaluation.Machine.ExBudgetingDefaults (defaultCekMachineCostsForTesting)
2014
import PlutusCore.Evaluation.Machine.SimpleBuiltinCostModel
2115
import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts (CekMachineCosts)

‎plutus-metatheory/src/FFI/SimplifierTrace.hs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
{-# OPTIONS_GHC -Wall #-}
2+
13
module FFI.SimplifierTrace (
24
mkFfiSimplifierTrace,
35
) where

‎plutus-metatheory/src/FFI/Untyped.hs‎

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,14 @@
11
{-# LANGUAGE GADTs #-}
22
{-# LANGUAGE KindSignatures #-}
3+
{-# OPTIONS_GHC -Wall #-}
34

45
module FFI.Untyped where
56

6-
import PlutusCore.Data hiding (Constr)
77
import PlutusCore.Default
88
import UntypedPlutusCore
99

10-
import Data.ByteString as BS hiding (map)
1110
import Data.Text as T hiding (map)
12-
import Data.Word (Word64)
1311
import GHC.Exts (IsList (..))
14-
import Universe
1512

1613
-- Untyped (Raw) syntax
1714

@@ -45,6 +42,7 @@ conv (Force _ t) = UForce (conv t)
4542
conv (Constr _ i es) = UConstr (toInteger i) (toList (fmap conv es))
4643
conv (Case _ arg cs) = UCase (conv arg) (toList (fmap conv cs))
4744

45+
tmnames :: String
4846
tmnames = ['a' .. 'z']
4947

5048
uconv :: Int -> UTerm -> Term NamedDeBruijn DefaultUni DefaultFun ()
@@ -58,9 +56,9 @@ uconv i (ULambda t) = LamAbs
5856
(NamedDeBruijn (T.pack [tmnames !! i]) deBruijnInitIndex)
5957
(uconv (i+1) t)
6058
uconv i (UApp t u) = Apply () (uconv i t) (uconv i u)
61-
uconv i (UCon c) = Constant () c
62-
uconv i UError = Error ()
63-
uconv i (UBuiltin b) = Builtin () b
59+
uconv _ (UCon c) = Constant () c
60+
uconv _ UError = Error ()
61+
uconv _ (UBuiltin b) = Builtin () b
6462
uconv i (UDelay t) = Delay () (uconv i t)
6563
uconv i (UForce t) = Force () (uconv i t)
6664
uconv i (UConstr j xs) = Constr () (fromInteger j) (fmap (uconv i) xs)

‎plutus-metatheory/src/MAlonzo/Code/Utils/Decidable.hs‎

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,29 @@
1-
{-# LANGUAGE BangPatterns #-}
2-
{-# LANGUAGE EmptyCase #-}
3-
{-# LANGUAGE EmptyDataDecls #-}
1+
{-# LANGUAGE BangPatterns #-}
2+
{-# LANGUAGE EmptyCase #-}
3+
{-# LANGUAGE EmptyDataDecls #-}
44
{-# LANGUAGE ExistentialQuantification #-}
55
{-# LANGUAGE NoMonomorphismRestriction #-}
6-
{-# LANGUAGE OverloadedStrings #-}
7-
{-# LANGUAGE PatternSynonyms #-}
8-
{-# LANGUAGE RankNTypes #-}
9-
{-# LANGUAGE ScopedTypeVariables #-}
6+
{-# LANGUAGE OverloadedStrings #-}
7+
{-# LANGUAGE PatternSynonyms #-}
8+
{-# LANGUAGE RankNTypes #-}
9+
{-# LANGUAGE ScopedTypeVariables #-}
1010

1111
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
1212

1313
module MAlonzo.Code.Utils.Decidable where
1414

15-
import Data.Text qualified
16-
import MAlonzo.Code.Agda.Builtin.Bool qualified
17-
import MAlonzo.Code.Agda.Builtin.Equality qualified
18-
import MAlonzo.Code.Agda.Builtin.Sigma qualified
19-
import MAlonzo.Code.Agda.Primitive qualified
20-
import MAlonzo.Code.Data.Irrelevant qualified
21-
import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
22-
import MAlonzo.Code.Relation.Nullary.Reflects qualified
23-
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
24-
mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
25-
word64ToNat)
26-
import MAlonzo.RTE qualified
15+
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
16+
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
17+
rem64, lt64, eq64, word64FromNat, word64ToNat)
18+
import qualified MAlonzo.RTE
19+
import qualified Data.Text
20+
import qualified MAlonzo.Code.Agda.Builtin.Bool
21+
import qualified MAlonzo.Code.Agda.Builtin.Equality
22+
import qualified MAlonzo.Code.Agda.Builtin.Sigma
23+
import qualified MAlonzo.Code.Agda.Primitive
24+
import qualified MAlonzo.Code.Data.Irrelevant
25+
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
26+
import qualified MAlonzo.Code.Relation.Nullary.Reflects
2727

2828
-- Utils.Decidable.dmap
2929
d_dmap_12 ::

‎plutus-metatheory/src/MAlonzo/Code/Utils/Reflection.hs‎

Lines changed: 23 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -1,32 +1,32 @@
1-
{-# LANGUAGE BangPatterns #-}
2-
{-# LANGUAGE EmptyCase #-}
3-
{-# LANGUAGE EmptyDataDecls #-}
1+
{-# LANGUAGE BangPatterns #-}
2+
{-# LANGUAGE EmptyCase #-}
3+
{-# LANGUAGE EmptyDataDecls #-}
44
{-# LANGUAGE ExistentialQuantification #-}
55
{-# LANGUAGE NoMonomorphismRestriction #-}
6-
{-# LANGUAGE OverloadedStrings #-}
7-
{-# LANGUAGE PatternSynonyms #-}
8-
{-# LANGUAGE RankNTypes #-}
9-
{-# LANGUAGE ScopedTypeVariables #-}
6+
{-# LANGUAGE OverloadedStrings #-}
7+
{-# LANGUAGE PatternSynonyms #-}
8+
{-# LANGUAGE RankNTypes #-}
9+
{-# LANGUAGE ScopedTypeVariables #-}
1010

1111
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
1212

1313
module MAlonzo.Code.Utils.Reflection where
1414

15-
import Data.Text qualified
16-
import MAlonzo.Code.Agda.Builtin.List qualified
17-
import MAlonzo.Code.Agda.Builtin.Maybe qualified
18-
import MAlonzo.Code.Agda.Builtin.Reflection qualified
19-
import MAlonzo.Code.Agda.Builtin.Sigma qualified
20-
import MAlonzo.Code.Agda.Builtin.String qualified
21-
import MAlonzo.Code.Agda.Primitive qualified
22-
import MAlonzo.Code.Data.Char.Base qualified
23-
import MAlonzo.Code.Data.List.Base qualified
24-
import MAlonzo.Code.Data.String.Base qualified
25-
import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
26-
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
27-
mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
28-
word64ToNat)
29-
import MAlonzo.RTE qualified
15+
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
16+
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
17+
rem64, lt64, eq64, word64FromNat, word64ToNat)
18+
import qualified MAlonzo.RTE
19+
import qualified Data.Text
20+
import qualified MAlonzo.Code.Agda.Builtin.List
21+
import qualified MAlonzo.Code.Agda.Builtin.Maybe
22+
import qualified MAlonzo.Code.Agda.Builtin.Reflection
23+
import qualified MAlonzo.Code.Agda.Builtin.Sigma
24+
import qualified MAlonzo.Code.Agda.Builtin.String
25+
import qualified MAlonzo.Code.Agda.Primitive
26+
import qualified MAlonzo.Code.Data.Char.Base
27+
import qualified MAlonzo.Code.Data.List.Base
28+
import qualified MAlonzo.Code.Data.String.Base
29+
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
3030

3131
-- Utils.Reflection.constructors
3232
d_constructors_4 ::
@@ -62,7 +62,7 @@ d_lastName_14 v0 v1
6262
(case coe v2 of
6363
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 v3 -> coe v3
6464
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> coe v0
65-
_ -> MAlonzo.RTE.mazUnreachableError)
65+
_ -> MAlonzo.RTE.mazUnreachableError)
6666
-- Utils.Reflection.getLastName
6767
d_getLastName_34 ::
6868
AgdaAny -> MAlonzo.Code.Agda.Builtin.String.T_String_6

‎plutus-metatheory/src/Raw.hs‎

Lines changed: 6 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -5,18 +5,14 @@
55
{-# LANGUAGE MultiParamTypeClasses #-}
66
{-# LANGUAGE RankNTypes #-}
77
{-# LANGUAGE TypeApplications #-}
8+
{-# OPTIONS_GHC -Wall #-}
9+
810
module Raw where
911

10-
import Data.ByteString as BS hiding (map)
1112
import Data.Text qualified as T
1213
import PlutusCore
13-
import PlutusCore.Data hiding (Constr)
1414
import PlutusCore.DeBruijn
15-
import PlutusCore.Default
16-
import PlutusCore.Parser
17-
import PlutusCore.Pretty
1815

19-
import Data.Either
2016
import PlutusCore.Error (ParserErrorBundle)
2117

2218
data KIND = Star | Sharp | Arrow KIND KIND
@@ -101,8 +97,6 @@ convTyCon (SomeTypeIn DefaultUniProtoList) = RTyCon RTyConList
10197
convTyCon (SomeTypeIn DefaultUniProtoArray) = RTyCon RTyConArray
10298
convTyCon (SomeTypeIn DefaultUniProtoPair) = RTyCon RTyConPair
10399
convTyCon (SomeTypeIn (DefaultUniApply _ _)) = error "unsupported builtin type application"
104-
-- TODO: this should be fixed once the metatheory supports builtin arrays
105-
convTyCon (SomeTypeIn DefaultUniProtoArray) = error "unsupported builtin array"
106100

107101
conv :: Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a -> RTerm
108102
conv (Var _ x) = RVar (unIndex (ndbnIndex x))
@@ -138,7 +132,7 @@ unconvT i (RTyPi k t) =
138132
unconvT i (RTyLambda k t) = TyLam () (NamedTyDeBruijn (varTy i)) (unconvK k) (unconvT (i+1) t)
139133

140134
unconvT i (RTyApp t u) = TyApp () (unconvT i t) (unconvT i u)
141-
unconvT i (RTyCon c) = TyBuiltin () (unconvTyCon c)
135+
unconvT _ (RTyCon c) = TyBuiltin () (unconvTyCon c)
142136
unconvT i (RTyMu t u) = TyIFix () (unconvT i t) (unconvT i u)
143137
unconvT i (RTySOP xss) = TySOP () (map (map (unconvT i)) xss)
144138

@@ -160,6 +154,7 @@ unconvTyCon RTyConArray = SomeTypeIn DefaultUniProtoArray
160154
unconvTyCon RTyConPair = SomeTypeIn DefaultUniProtoPair
161155

162156

157+
tmnames, tynames :: String
163158
tmnames = ['a' .. 'z']
164159
--tynames = ['α','β','γ','δ','ε','ζ','θ','ι','κ','ν','ξ','ο','π','ρ','σ','τ','υ','ϕ','χ','ψ','ω']
165160
tynames = ['A' .. 'Z']
@@ -171,9 +166,9 @@ unconv i (RTLambda k tm) = TyAbs () (NamedTyDeBruijn (varTy i)) (unconvK k) (u
171166
unconv i (RTApp t ty) = TyInst () (unconv i t) (unconvT i ty)
172167
unconv i (RLambda ty tm) = LamAbs () (varTm i) (unconvT (i+1) ty) (unconv (i+1) tm)
173168
unconv i (RApp t u) = Apply () (unconv i t) (unconv i u)
174-
unconv i (RCon c) = Constant () c
169+
unconv _ (RCon c) = Constant () c
175170
unconv i (RError ty) = Error () (unconvT i ty)
176-
unconv i (RBuiltin b) = Builtin () b
171+
unconv _ (RBuiltin b) = Builtin () b
177172
unconv i (RWrap tyA tyB t) = IWrap () (unconvT i tyA) (unconvT i tyB) (unconv i t)
178173
unconv i (RUnWrap t) = Unwrap () (unconv i t)
179174
unconv i (RConstr ty j cs) = Constr () (unconvT i ty) (fromInteger j) (fmap (unconv i) cs)

0 commit comments

Comments
 (0)