GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 01:13:34 +03:00
Code Issues Projects Releases Wiki Activity

clean up 7.8-isms

Browse Source
This commit is contained in:
Adam C. Foltzer 2016-06-07 13:40:15 -07:00
parent 1e3d1f642a
commit 76be770d83
22 changed files with 194 additions and 1460 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1071
cabal.GHC78.config
View File

File diff suppressed because it is too large Load Diff

7
cryptol.cabal
View File

@ -40,15 +40,14 @@ flag server
library
Default-language:
Haskell98
Build-depends: base >= 4.7 && < 5,
Build-depends: base >= 4.8 && < 5,
base-compat >= 0.6,
bytestring >= 0.10,
array >= 0.4,
async >= 2.0,
containers >= 0.5,
deepseq >= 1.3,
deepseq-generics >= 0.1 && < 0.3,
directory >= 1.2,
directory >= 1.2.2.0,
filepath >= 1.3,
gitrev >= 1.0,
GraphSCC >= 1.0.4,
@ -61,7 +60,7 @@ library
process >= 1.2,
QuickCheck >= 2.7,
random >= 1.0.1,
sbv >= 5.7,
sbv >= 5.12,
smtLib >= 1.0.7,
simple-smt >= 0.6.0,
syb >= 0.4,

11
src/Cryptol/Eval/Env.hs
View File

@ -6,10 +6,12 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.Eval.Env where
import Cryptol.Eval.Value
@ -22,7 +24,6 @@ import qualified Data.Map as Map
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Prelude ()
import Prelude.Compat
@ -34,9 +35,7 @@ type ReadEnv = EvalEnv
data EvalEnv = EvalEnv
{ envVars :: Map.Map Name Value
, envTypes :: Map.Map TVar (Either Nat' TValue)
} deriving (Generic)
instance NFData EvalEnv where rnf = genericRnf
} deriving (Generic, NFData)
instance Monoid EvalEnv where
mempty = EvalEnv

21
src/Cryptol/Eval/Value.hs
View File

@ -6,12 +6,14 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternGuards #-}
module Cryptol.Eval.Value where
import qualified Cryptol.Eval.Arch as Arch
@ -30,7 +32,6 @@ import Numeric (showIntAtBase)
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
-- Utilities -------------------------------------------------------------------
@ -69,9 +70,7 @@ finNat' n' =
-- | width, value
-- Invariant: The value must be within the range 0 .. 2^width-1
data BV = BV !Integer !Integer deriving (Generic)
instance NFData BV where rnf = genericRnf
data BV = BV !Integer !Integer deriving (Generic, NFData)
-- | Smart constructor for 'BV's that checks for the width limit
mkBv :: Integer -> Integer -> BV
@ -90,9 +89,7 @@ data GenValue b w
| VFun (GenValue b w -> GenValue b w) -- functions
| VPoly (TValue -> GenValue b w) -- polymorphic values (kind *)
| VNumPoly (Nat' -> GenValue b w) -- polymorphic values (kind #)
deriving (Generic)
instance (NFData b, NFData w) => NFData (GenValue b w) where rnf = genericRnf
deriving (Generic, NFData)
type Value = GenValue Bool BV
@ -105,9 +102,7 @@ data TValue
| TVTuple [TValue]
| TVRec [(Ident, TValue)]
| TVFun TValue TValue
deriving (Generic)
instance NFData TValue where rnf = genericRnf
deriving (Generic, NFData)
tValTy :: TValue -> Type
tValTy tv =

25
src/Cryptol/ModuleSystem/Env.hs
View File

@ -7,10 +7,10 @@
-- Portability : portable
{-# LANGUAGE CPP #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.ModuleSystem.Env where
#ifndef RELOCATABLE
@ -39,7 +39,6 @@ import qualified Data.List as List
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Prelude ()
import Prelude.Compat
@ -57,15 +56,11 @@ data ModuleEnv = ModuleEnv
, meSolverConfig :: T.SolverConfig
, meCoreLint :: CoreLint
, meSupply :: !Supply
} deriving (Generic)
instance NFData ModuleEnv where rnf = genericRnf
} deriving (Generic, NFData)
data CoreLint = NoCoreLint -- ^ Don't run core lint
| CoreLint -- ^ Run core lint
deriving (Generic)
instance NFData CoreLint where rnf = genericRnf
deriving (Generic, NFData)
resetModuleEnv :: ModuleEnv -> ModuleEnv
resetModuleEnv env = env
@ -187,11 +182,9 @@ qualifiedEnv me = fold $
newtype LoadedModules = LoadedModules
{ getLoadedModules :: [LoadedModule]
} deriving (Show, Generic)
} deriving (Show, Generic, NFData)
-- ^ Invariant: All the dependencies of any module `m` must precede `m` in the list.
instance NFData LoadedModules where rnf = genericRnf
instance Monoid LoadedModules where
mempty = LoadedModules []
mappend l r = LoadedModules
@ -202,9 +195,7 @@ data LoadedModule = LoadedModule
, lmFilePath :: FilePath
, lmInterface :: Iface
, lmModule :: T.Module
} deriving (Show, Generic)
instance NFData LoadedModule where rnf = genericRnf
} deriving (Show, Generic, NFData)
isLoaded :: ModName -> LoadedModules -> Bool
isLoaded mn lm = any ((mn ==) . lmName) (getLoadedModules lm)
@ -245,9 +236,7 @@ data DynamicEnv = DEnv
{ deNames :: R.NamingEnv
, deDecls :: [T.DeclGroup]
, deEnv :: EvalEnv
} deriving (Generic)
instance NFData DynamicEnv where rnf = genericRnf
} deriving (Generic, NFData)
instance Monoid DynamicEnv where
mempty = DEnv

18
src/Cryptol/ModuleSystem/Interface.hs
View File

@ -6,9 +6,10 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.ModuleSystem.Interface (
Iface(..)
@ -29,7 +30,6 @@ import qualified Data.Map as Map
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Prelude ()
import Prelude.Compat
@ -40,17 +40,13 @@ data Iface = Iface
{ ifModName :: !ModName
, ifPublic :: IfaceDecls
, ifPrivate :: IfaceDecls
} deriving (Show, Generic)
instance NFData Iface where rnf = genericRnf
} deriving (Show, Generic, NFData)
data IfaceDecls = IfaceDecls
{ ifTySyns :: Map.Map Name IfaceTySyn
, ifNewtypes :: Map.Map Name IfaceNewtype
, ifDecls :: Map.Map Name IfaceDecl
} deriving (Show, Generic)
instance NFData IfaceDecls where rnf = genericRnf
} deriving (Show, Generic, NFData)
instance Monoid IfaceDecls where
mempty = IfaceDecls Map.empty Map.empty Map.empty
@ -79,9 +75,7 @@ data IfaceDecl = IfaceDecl
, ifDeclInfix :: Bool
, ifDeclFixity :: Maybe Fixity
, ifDeclDoc :: Maybe String
} deriving (Show, Generic)
instance NFData IfaceDecl where rnf = genericRnf
} deriving (Show, Generic, NFData)
mkIfaceDecl :: Decl -> IfaceDecl
mkIfaceDecl d = IfaceDecl

10
src/Cryptol/ModuleSystem/Monad.hs
View File

@ -7,6 +7,7 @@
-- Portability : portable
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.ModuleSystem.Monad where
@ -35,7 +36,6 @@ import MonadLib
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Prelude ()
import Prelude.Compat
@ -45,9 +45,7 @@ import Prelude.Compat
data ImportSource
= FromModule P.ModName
| FromImport (Located P.Import)
deriving (Show,Generic)
instance NFData ImportSource where rnf = genericRnf
deriving (Show, Generic, NFData)
instance Eq ImportSource where
(==) = (==) `on` importedModule
@ -209,9 +207,7 @@ duplicateModuleName name path1 path2 =
data ModuleWarning
= TypeCheckWarnings [(Range,T.Warning)]
| RenamerWarnings [RenamerWarning]
deriving (Show,Generic)
instance NFData ModuleWarning where rnf = genericRnf
deriving (Show, Generic, NFData)
instance PP ModuleWarning where
ppPrec _ w = case w of

22
src/Cryptol/ModuleSystem/Name.hs
View File

@ -7,11 +7,13 @@
-- Portability : portable
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RecordWildCards #-}
-- for the instances of RunM and BaseM
{-# LANGUAGE UndecidableInstances #-}
@ -50,7 +52,6 @@ import Cryptol.Utils.Panic
import Cryptol.Utils.PP
import Control.DeepSeq
import Control.DeepSeq.Generics
import Control.Monad.Fix (MonadFix(mfix))
import qualified Data.Map as Map
import qualified Data.Monoid as M
@ -67,7 +68,7 @@ data NameInfo = Declared !ModName
-- ^ This name refers to a declaration from this module
| Parameter
-- ^ This name is a parameter (function or type)
deriving (Eq,Show,Generic)
deriving (Eq, Show, Generic, NFData)
data Name = Name { nUnique :: {-# UNPACK #-} !Int
-- ^ INVARIANT: this field uniquely identifies a name for one
@ -87,7 +88,7 @@ data Name = Name { nUnique :: {-# UNPACK #-} !Int
, nLoc :: !Range
-- ^ Where this name was defined
} deriving (Show,Generic)
} deriving (Show, Generic, NFData)
instance Eq Name where
a == b = compare a b == EQ
@ -96,9 +97,6 @@ instance Eq Name where
instance Ord Name where
compare a b = compare (nUnique a) (nUnique b)
instance NFData NameInfo where rnf = genericRnf
instance NFData Name where rnf = genericRnf
-- | Compare two names lexically.
cmpNameLexical :: Name -> Name -> Ordering
cmpNameLexical l r =
@ -264,9 +262,7 @@ nextUniqueM = liftSupply nextUnique
data Supply = Supply !Int
deriving (Show,Generic)
instance NFData Supply where rnf = genericRnf
deriving (Show, Generic, NFData)
-- | This should only be used once at library initialization, and threaded
-- through the rest of the session. The supply is started at 0x1000 to leave us
@ -303,9 +299,7 @@ mkParameter nIdent nLoc s =
-- | A mapping from an identifier defined in some module to its real name.
data PrimMap = PrimMap { primDecls :: Map.Map Ident Name
, primTypes :: Map.Map Ident Name
} deriving (Show, Generic)
instance NFData PrimMap where rnf = genericRnf
} deriving (Show, Generic, NFData)
lookupPrimDecl, lookupPrimType :: Ident -> PrimMap -> Name

17
src/Cryptol/ModuleSystem/NamingEnv.hs
View File

@ -6,15 +6,15 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.ModuleSystem.NamingEnv where
import Cryptol.ModuleSystem.Interface
@ -32,7 +32,6 @@ import MonadLib (runId,Id)
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Prelude ()
import Prelude.Compat
@ -48,9 +47,7 @@ data NamingEnv = NamingEnv { neExprs :: !(Map.Map PName [Name])
-- ^ Type renaming environment
, neFixity:: !(Map.Map Name Fixity)
-- ^ Expression-level fixity environment
} deriving (Show, Generic)
instance NFData NamingEnv where rnf = genericRnf
} deriving (Show, Generic, NFData)
instance Monoid NamingEnv where
mempty =

22
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -6,14 +6,13 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.ModuleSystem.Renamer (
NamingEnv(), shadowing
, BindsNames(..), InModule(..), namingEnv'
@ -43,7 +42,6 @@ import MonadLib hiding (mapM, mapM_)
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Prelude ()
import Prelude.Compat
@ -82,9 +80,7 @@ data RenamerError
| BoundReservedType PName (Maybe Range) Doc NameDisp
-- ^ When a builtin type is named in a binder.
deriving (Show,Generic)
instance NFData RenamerError where rnf = genericRnf
deriving (Show, Generic, NFData)
instance PP RenamerError where
ppPrec _ e = case e of
@ -142,9 +138,7 @@ instance PP RenamerError where
data RenamerWarning
= SymbolShadowed Name [Name] NameDisp
deriving (Show,Generic)
instance NFData RenamerWarning where rnf = genericRnf
deriving (Show, Generic, NFData)
instance PP RenamerWarning where
ppPrec _ (SymbolShadowed new originals disp) = fixNameDisp disp $

146
src/Cryptol/Parser/AST.hs
View File

@ -7,12 +7,14 @@
-- Portability : portable
{-# LANGUAGE Safe #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.Parser.AST
( -- * Names
Ident, mkIdent, mkInfix, isInfixIdent, nullIdent, identText
@ -83,7 +85,6 @@ import Numeric(showIntAtBase)
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Prelude ()
import Prelude.Compat
@ -106,9 +107,8 @@ newtype Program name = Program [TopDecl name]
data Module name = Module { mName :: Located ModName
, mImports :: [Located Import]
, mDecls :: [TopDecl name]
} deriving (Show, Generic)
} deriving (Show, Generic, NFData)
instance NFData name => NFData (Module name) where rnf = genericRnf
modRange :: Module name -> Range
modRange m = rCombs $ catMaybes
@ -122,9 +122,7 @@ modRange m = rCombs $ catMaybes
data TopDecl name = Decl (TopLevel (Decl name))
| TDNewtype (TopLevel (Newtype name))
| Include (Located FilePath)
deriving (Show,Generic)
instance NFData name => NFData (TopDecl name) where rnf = genericRnf
deriving (Show, Generic, NFData)
data Decl name = DSignature [Located name] (Schema name)
| DFixity !Fixity [Located name]
@ -133,17 +131,13 @@ data Decl name = DSignature [Located name] (Schema name)
| DPatBind (Pattern name) (Expr name)
| DType (TySyn name)
| DLocated (Decl name) Range
deriving (Eq,Show,Generic)
instance NFData name => NFData (Decl name) where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
-- | An import declaration.
data Import = Import { iModule :: !ModName
, iAs :: Maybe ModName
, iSpec :: Maybe ImportSpec
} deriving (Eq,Show,Generic)
instance NFData Import where rnf = genericRnf
} deriving (Eq, Show, Generic, NFData)
-- | The list of names following an import.
--
@ -152,14 +146,10 @@ instance NFData Import where rnf = genericRnf
-- present.
data ImportSpec = Hiding [Ident]
| Only [Ident]
deriving (Eq,Show,Generic)
instance NFData ImportSpec where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data TySyn n = TySyn (Located n) [TParam n] (Type n)
deriving (Eq,Show,Generic)
instance NFData name => NFData (TySyn name) where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
{- | Bindings. Notes:
@ -182,23 +172,17 @@ data Bind name = Bind { bName :: Located name -- ^ Defined thing
, bPragmas :: [Pragma] -- ^ Optional pragmas
, bMono :: Bool -- ^ Is this a monomorphic binding
, bDoc :: Maybe String -- ^ Optional doc string
} deriving (Eq,Show,Generic)
instance NFData name => NFData (Bind name) where rnf = genericRnf
} deriving (Eq, Show, Generic, NFData)
type LBindDef = Located (BindDef PName)
data BindDef name = DPrim
| DExpr (Expr name)
deriving (Eq,Show,Generic)
instance NFData name => NFData (BindDef name) where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data Fixity = Fixity { fAssoc :: !Assoc
, fLevel :: !Int
} deriving (Eq,Show,Generic)
instance NFData Fixity where rnf = genericRnf
} deriving (Eq, Show, Generic, NFData)
data FixityCmp = FCError
| FCLeft
@ -221,16 +205,12 @@ defaultFixity = Fixity LeftAssoc 100
data Pragma = PragmaNote String
| PragmaProperty
deriving (Eq,Show,Generic)
instance NFData Pragma where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data Newtype name = Newtype { nName :: Located name -- ^ Type name
, nParams :: [TParam name] -- ^ Type params
, nBody :: [Named (Type name)] -- ^ Constructor
} deriving (Eq,Show,Generic)
instance NFData name => NFData (Newtype name) where rnf = genericRnf
} deriving (Eq, Show, Generic, NFData)
-- | Input at the REPL, which can either be an expression or a @let@
-- statement.
@ -241,22 +221,17 @@ data ReplInput name = ExprInput (Expr name)
-- | Export information for a declaration.
data ExportType = Public
| Private
deriving (Eq,Show,Ord,Generic)
instance NFData ExportType where rnf = genericRnf
deriving (Eq, Show, Ord, Generic, NFData)
data TopLevel a = TopLevel { tlExport :: ExportType
, tlDoc :: Maybe (Located String)
, tlValue :: a
} deriving (Show,Generic,Functor,Foldable,Traversable)
instance NFData a => NFData (TopLevel a) where rnf = genericRnf
}
deriving (Show, Generic, NFData, Functor, Foldable, Traversable)
data ExportSpec name = ExportSpec { eTypes :: Set.Set name
, eBinds :: Set.Set name
} deriving (Show,Generic)
instance NFData name => NFData (ExportSpec name) where rnf = genericRnf
} deriving (Show, Generic, NFData)
instance Ord name => Monoid (ExportSpec name) where
mempty = ExportSpec { eTypes = mempty, eBinds = mempty }
@ -291,16 +266,12 @@ data NumInfo = BinLit Int -- ^ n-digit binary literal
| HexLit Int -- ^ n-digit hex literal
| CharLit -- ^ character literal
| PolyLit Int -- ^ polynomial literal
deriving (Eq,Show,Generic)
instance NFData NumInfo where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
-- | Literals.
data Literal = ECNum Integer NumInfo -- ^ @0x10@ (HexLit 2)
| ECString String -- ^ @\"hello\"@
deriving (Eq,Show,Generic)
instance NFData Literal where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data Expr n = EVar n -- ^ @ x @
| ELit Literal -- ^ @ 0x10 @
@ -322,15 +293,11 @@ data Expr n = EVar n -- ^ @ x @
| EParens (Expr n) -- ^ @ (e) @ (Removed by Fixity)
| EInfix (Expr n) (Located n) Fixity (Expr n)-- ^ @ a + b @ (Removed by Fixity)
deriving (Eq,Show,Generic)
instance NFData name => NFData (Expr name) where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data TypeInst name = NamedInst (Named (Type name))
| PosInst (Type name)
deriving (Eq,Show,Generic)
instance NFData name => NFData (TypeInst name) where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
{- | Selectors are used for projecting from various components.
Each selector has an option spec to specify the shape of the thing
@ -349,15 +316,11 @@ data Selector = TupleSel Int (Maybe Int)
| ListSel Int (Maybe Int)
-- ^ List selection.
-- Optionally specifies the length of the list.
deriving (Eq,Show,Ord,Generic)
instance NFData Selector where rnf = genericRnf
deriving (Eq, Show, Ord, Generic, NFData)
data Match name = Match (Pattern name) (Expr name) -- ^ p <- e
| MatchLet (Bind name)
deriving (Eq,Show,Generic)
instance NFData name => NFData (Match name) where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data Pattern n = PVar (Located n) -- ^ @ x @
| PWild -- ^ @ _ @
@ -367,48 +330,38 @@ data Pattern n = PVar (Located n) -- ^ @ x @
| PTyped (Pattern n) (Type n) -- ^ @ x : [8] @
| PSplit (Pattern n) (Pattern n)-- ^ @ (x # y) @
| PLocated (Pattern n) Range -- ^ Location information
deriving (Eq,Show,Generic)
instance NFData name => NFData (Pattern name) where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data Named a = Named { name :: Located Ident, value :: a }
deriving (Eq,Show,Foldable,Traversable,Generic,Functor)
instance NFData a => NFData (Named a) where rnf = genericRnf
deriving (Eq, Show, Foldable, Traversable, Generic, NFData, Functor)
data Schema n = Forall [TParam n] [Prop n] (Type n) (Maybe Range)
deriving (Eq,Show,Generic)
deriving (Eq, Show, Generic, NFData)
instance NFData name => NFData (Schema name) where rnf = genericRnf
data Kind = KNum | KType
deriving (Eq,Show,Generic)
instance NFData Kind where rnf = genericRnf
data Kind = KNum | KType
deriving (Eq, Show, Generic, NFData)
data TParam n = TParam { tpName :: n
, tpKind :: Maybe Kind
, tpRange :: Maybe Range
}
deriving (Eq,Show,Generic)
deriving (Eq, Show, Generic, NFData)
instance NFData name => NFData (TParam name) where rnf = genericRnf
data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@
| TSeq (Type n) (Type n) -- ^ @[8] a@
| TBit -- ^ @Bit@
| TNum Integer -- ^ @10@
| TChar Char -- ^ @'a'@
| TInf -- ^ @inf@
| TUser n [Type n] -- ^ A type variable or synonym
| TApp TFun [Type n] -- ^ @2 + x@
| TRecord [Named (Type n)]-- ^ @{ x : [8], y : [32] }@
| TTuple [Type n] -- ^ @([8], [32])@
| TWild -- ^ @_@, just some type.
| TLocated (Type n) Range -- ^ Location information
| TParens (Type n) -- ^ @ (ty) @
| TInfix (Type n) (Located n) Fixity (Type n) -- ^ @ ty + ty @
deriving (Eq,Show,Generic)
data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@
| TSeq (Type n) (Type n) -- ^ @[8] a@
| TBit -- ^ @Bit@
| TNum Integer -- ^ @10@
| TChar Char -- ^ @'a'@
| TInf -- ^ @inf@
| TUser n [Type n] -- ^ A type variable or synonym
| TApp TFun [Type n] -- ^ @2 + x@
| TRecord [Named (Type n)]-- ^ @{ x : [8], y : [32] }@
| TTuple [Type n] -- ^ @([8], [32])@
| TWild -- ^ @_@, just some type.
| TLocated (Type n) Range -- ^ Location information
| TParens (Type n) -- ^ @ (ty) @
| TInfix (Type n) (Located n) Fixity (Type n) -- ^ @ ty + ty @
deriving (Eq, Show, Generic, NFData)
tconNames :: Map.Map PName (Type PName)
tconNames = Map.fromList
@ -416,19 +369,14 @@ tconNames = Map.fromList
, (mkUnqual (packIdent "inf"), TInf)
]
instance NFData name => NFData (Type name) where rnf = genericRnf
data Prop n = CFin (Type n) -- ^ @ fin x @
| CEqual (Type n) (Type n) -- ^ @ x == 10 @
| CGeq (Type n) (Type n) -- ^ @ x >= 10 @
| CArith (Type n) -- ^ @ Arith a @
| CCmp (Type n) -- ^ @ Cmp a @
| CLocated (Prop n) Range -- ^ Location information
| CType (Type n) -- ^ After parsing
deriving (Eq,Show,Generic)
instance NFData name => NFData (Prop name) where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
--------------------------------------------------------------------------------
-- Note: When an explicit location is missing, we could use the sub-components

37
src/Cryptol/Parser/LexerUtils.hs
View File

@ -6,9 +6,10 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.Parser.LexerUtils where
import Cryptol.Parser.Position
@ -24,7 +25,6 @@ import Data.Word(Word8)
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
data Config = Config
{ cfgSource :: !FilePath -- ^ File that we are working on
@ -355,20 +355,14 @@ virt cfg pos x = Located { srcRange = Range
--------------------------------------------------------------------------------
data Token = Token { tokenType :: TokenT, tokenText :: Text }
deriving (Show, Generic)
instance NFData Token where rnf = genericRnf
deriving (Show, Generic, NFData)
-- | Virtual tokens, inserted by layout processing.
data TokenV = VCurlyL| VCurlyR | VSemi
deriving (Eq,Show,Generic)
instance NFData TokenV where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data TokenW = BlockComment | LineComment | Space | DocStr
deriving (Eq,Show,Generic)
instance NFData TokenW where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data TokenKW = KW_Arith
| KW_Bit
@ -402,9 +396,7 @@ data TokenKW = KW_Arith
| KW_infixr
| KW_infix
| KW_primitive
deriving (Eq,Show,Generic)
instance NFData TokenKW where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
-- | The named operators are a special case for parsing types, and 'Other' is
-- used for all other cases that lexed as an operator.
@ -412,9 +404,7 @@ data TokenOp = Plus | Minus | Mul | Div | Exp | Mod
| Equal | LEQ | GEQ
| Complement | Hash
| Other [T.Text] T.Text
deriving (Eq,Show,Generic)
instance NFData TokenOp where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data TokenSym = Bar
| ArrL | ArrR | FatArrR
@ -432,9 +422,7 @@ data TokenSym = Bar
| CurlyL | CurlyR
| TriL | TriR
| Underscore
deriving (Eq,Show,Generic)
instance NFData TokenSym where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data TokenErr = UnterminatedComment
| UnterminatedString
@ -442,9 +430,7 @@ data TokenErr = UnterminatedComment
| InvalidString
| InvalidChar
| LexicalError
deriving (Eq,Show,Generic)
instance NFData TokenErr where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data TokenT = Num Integer Int Int -- ^ value, base, number of digits
| ChrLit Char -- ^ character literal
@ -457,14 +443,11 @@ data TokenT = Num Integer Int Int -- ^ value, base, number of digits
| White TokenW -- ^ white space token
| Err TokenErr -- ^ error token
| EOF
deriving (Eq,Show,Generic)
instance NFData TokenT where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
instance PP Token where
ppPrec _ (Token _ s) = text (T.unpack s)
-- | Collapse characters into a single Word8, identifying ASCII, and classes of
-- unicode. This came from:
--

50
src/Cryptol/Parser/NoInclude.hs
View File

@ -6,60 +6,40 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE CPP #-}
#ifndef MIN_VERSION_directory
#define MIN_VERSION_directory(a,b,c) 0
#endif
{-# LANGUAGE RecordWildCards #-}
module Cryptol.Parser.NoInclude
( removeIncludesModule
, IncludeError(..), ppIncludeError
) where
import qualified Control.Applicative as A
import Control.DeepSeq
import qualified Control.Exception as X
import Data.Either (partitionEithers)
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy.IO as T
import GHC.Generics (Generic)
import MonadLib
import System.Directory (makeAbsolute)
import System.FilePath (takeDirectory,(</>),isAbsolute)
import Cryptol.Parser (parseProgramWith)
import Cryptol.Parser.AST
import Cryptol.Parser.LexerUtils (Config(..),defaultConfig)
import Cryptol.Parser.ParserUtils
import Cryptol.Utils.PP
import Cryptol.Parser.Unlit (guessPreProc)
import qualified Control.Applicative as A
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy.IO as T
import Data.Either (partitionEithers)
import MonadLib
import qualified Control.Exception as X
import System.FilePath (takeDirectory,(</>),isAbsolute)
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import System.Directory (getCurrentDirectory)
import System.FilePath (isRelative, normalise)
-- from the source of directory-1.2.2.1; included to maintain
-- backwards compatibility
makeAbsolute :: FilePath -> IO FilePath
makeAbsolute = fmap normalise . absolutize
where absolutize path
| isRelative path = fmap (</> path) getCurrentDirectory
| otherwise = return path
import Cryptol.Utils.PP
removeIncludesModule :: FilePath -> Module PName -> IO (Either [IncludeError] (Module PName))
removeIncludesModule modPath m = runNoIncM modPath (noIncludeModule m)
data IncludeError
= IncludeFailed (Located FilePath)
| IncludeParseError ParseError
| IncludeCycle [Located FilePath]
deriving (Show,Generic)
instance NFData IncludeError where rnf = genericRnf
deriving (Show, Generic, NFData)
ppIncludeError :: IncludeError -> Doc
ppIncludeError ie = case ie of

15
src/Cryptol/Parser/NoPat.hs
View File

@ -10,12 +10,13 @@
-- patterns. It also eliminates pattern bindings by de-sugaring them
-- into `Bind`. Furthermore, here we associate signatures and pragmas
-- with the names to which they belong.
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.Parser.NoPat (RemovePatterns(..),Error(..)) where
import Cryptol.Parser.AST
@ -31,7 +32,6 @@ import qualified Data.Map as Map
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Prelude ()
import Prelude.Compat
@ -446,9 +446,7 @@ data Error = MultipleSignatures PName [Located (Schema PName)]
| MultipleFixities PName [Range]
| FixityNoBind (Located PName)
| MultipleDocs PName [Range]
deriving (Show,Generic)
instance NFData Error where rnf = genericRnf
deriving (Show,Generic, NFData)
instance Functor NoPatM where fmap = liftM
instance Applicative NoPatM where pure = return; (<*>) = ap
@ -514,4 +512,3 @@ instance PP Error where
MultipleDocs n locs ->
text "Multiple documentation blocks given for:" <+> pp n
$$ nest 2 (vcat (map pp locs))

12
src/Cryptol/Parser/ParserUtils.hs
View File

@ -6,9 +6,12 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE Safe, PatternGuards #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternGuards #-}
module Cryptol.Parser.ParserUtils where
import Cryptol.Parser.AST
@ -28,7 +31,6 @@ import qualified Data.Text.Lazy as T
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Prelude ()
import Prelude.Compat
@ -66,9 +68,7 @@ lexerP k = P $ \cfg p (S ts) ->
data ParseError = HappyError FilePath Position (Maybe Token)
| HappyErrorMsg Range String
deriving (Show, Generic)
instance NFData ParseError where rnf = genericRnf
deriving (Show, Generic, NFData)
newtype S = S [Located Token]

16
src/Cryptol/Parser/Position.hs
View File

@ -7,9 +7,10 @@
-- Portability : portable
{-# LANGUAGE Safe #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.Parser.Position where
import Data.Text.Lazy (Text)
@ -17,26 +18,19 @@ import qualified Data.Text.Lazy as T
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Cryptol.Utils.PP
data Located a = Located { srcRange :: !Range, thing :: a }
deriving (Eq,Show,Generic)
instance NFData a => NFData (Located a) where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
data Position = Position { line :: !Int, col :: !Int }
deriving (Eq,Ord,Show,Generic)
instance NFData Position where rnf = genericRnf
deriving (Eq, Ord, Show, Generic, NFData)
data Range = Range { from :: !Position
, to :: !Position
, source :: FilePath }
deriving (Eq,Show,Generic)
instance NFData Range where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
-- | An empty range.
--

7
src/Cryptol/Prims/Syntax.hs
View File

@ -6,8 +6,8 @@
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.Prims.Syntax
( TFun(..), tBinOpPrec, tfunNames
) where
@ -19,7 +19,6 @@ import qualified Data.Map as Map
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
-- | Built-in types.
data TFun
@ -41,9 +40,7 @@ data TFun
| TCLenFromThenTo -- ^ @ : Num -> Num -> Num -> Num@
-- Example: @[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]@
deriving (Show, Eq, Ord, Bounded, Enum, Generic)
instance NFData TFun where rnf = genericRnf
deriving (Show, Eq, Ord, Bounded, Enum, Generic, NFData)
tBinOpPrec :: Map.Map TFun (Assoc,Int)
tBinOpPrec = mkMap t_table

72
src/Cryptol/TypeCheck/AST.hs
View File

@ -7,10 +7,11 @@
-- Portability : portable
{-# LANGUAGE Safe #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-}
module Cryptol.TypeCheck.AST
( module Cryptol.TypeCheck.AST
, Name()
@ -38,7 +39,6 @@ import Cryptol.TypeCheck.Solver.InfNat
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Data.Map (Map)
import qualified Data.Map as Map
@ -53,26 +53,20 @@ data Module = Module { mName :: !ModName
, mTySyns :: Map Name TySyn
, mNewtypes :: Map Name Newtype
, mDecls :: [DeclGroup]
} deriving (Show, Generic)
instance NFData Module where rnf = genericRnf
} deriving (Show, Generic, NFData)
-- | Kinds, classify types.
data Kind = KType
| KNum
| KProp
| Kind :-> Kind
deriving (Eq, Show, Generic)
deriving (Eq, Show, Generic, NFData)
infixr 5 :->
instance NFData Kind where rnf = genericRnf
-- | The types of polymorphic values.
data Schema = Forall { sVars :: [TParam], sProps :: [Prop], sType :: Type }
deriving (Eq, Show, Generic)
instance NFData Schema where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
-- | Type synonym.
data TySyn = TySyn { tsName :: Name -- ^ Name
@ -80,27 +74,21 @@ data TySyn = TySyn { tsName :: Name -- ^ Name
, tsConstraints :: [Prop] -- ^ Ensure body is OK
, tsDef :: Type -- ^ Definition
}
deriving (Eq, Show, Generic)
instance NFData TySyn where rnf = genericRnf
deriving (Eq, Show, Generic, NFData)
-- | Named records
data Newtype = Newtype { ntName :: Name
, ntParams :: [TParam]
, ntConstraints :: [Prop]
, ntFields :: [(Ident,Type)]
} deriving (Show, Generic)
instance NFData Newtype where rnf = genericRnf
} deriving (Show, Generic, NFData)
-- | Type parameters.
data TParam = TParam { tpUnique :: !Int -- ^ Parameter identifier
, tpKind :: Kind -- ^ Kind of parameter
, tpName :: Maybe Name -- ^ Name from source, if any.
}
deriving (Show, Generic)
instance NFData TParam where rnf = genericRnf
deriving (Show, Generic, NFData)
instance Eq TParam where
x == y = tpUnique x == tpUnique y
@ -129,9 +117,7 @@ data Type = TCon TCon [Type]
| TRec [(Ident,Type)]
-- ^ Record type
deriving (Show,Eq,Ord,Generic)
instance NFData Type where rnf = genericRnf
deriving (Show, Eq, Ord, Generic, NFData)
-- | The type is supposed to be of kind `KProp`
type Prop = Type
@ -147,15 +133,11 @@ data TVar = TVFree !Int Kind (Set TVar) Doc
| TVBound !Int Kind
deriving (Show,Generic)
instance NFData TVar where rnf = genericRnf
deriving (Show, Generic, NFData)
-- | Type constants.
data TCon = TC TC | PC PC | TF TFun
deriving (Show,Eq,Ord,Generic)
instance NFData TCon where rnf = genericRnf
deriving (Show, Eq, Ord, Generic, NFData)
-- | Built-in type constants.
@ -169,9 +151,7 @@ data PC = PEqual -- ^ @_ == _@
| PHas Selector -- ^ @Has sel type field@ does not appear in schemas
| PArith -- ^ @Arith _@
| PCmp -- ^ @Cmp _@
deriving (Show,Eq,Ord,Generic)
instance NFData PC where rnf = genericRnf
deriving (Show, Eq, Ord, Generic, NFData)
-- | 1-1 constants.
data TC = TCNum Integer -- ^ Numbers
@ -181,14 +161,10 @@ data TC = TCNum Integer -- ^ Numbers
| TCFun -- ^ @_ -> _@
| TCTuple Int -- ^ @(_, _, _)@
| TCNewtype UserTC -- ^ user-defined, @T@
deriving (Show,Eq,Ord,Generic)
instance NFData TC where rnf = genericRnf
deriving (Show, Eq, Ord, Generic, NFData)
data UserTC = UserTC Name Kind
deriving (Show,Generic)
instance NFData UserTC where rnf = genericRnf
deriving (Show, Generic, NFData)
instance Eq UserTC where
UserTC x _ == UserTC y _ = x == y
@ -265,23 +241,17 @@ data Expr = EList [Expr] Type -- ^ List value (with type of elements)
| EWhere Expr [DeclGroup]
deriving (Show, Generic)
instance NFData Expr where rnf = genericRnf
deriving (Show, Generic, NFData)
data Match = From Name Type Expr -- ^ do we need this type? it seems like it
-- can be computed from the expr
| Let Decl
deriving (Show, Generic)
instance NFData Match where rnf = genericRnf
deriving (Show, Generic, NFData)
data DeclGroup = Recursive [Decl] -- ^ Mutually recursive declarations
| NonRecursive Decl -- ^ Non-recursive declaration
deriving (Show,Generic)
instance NFData DeclGroup where rnf = genericRnf
deriving (Show, Generic, NFData)
groupDecls :: DeclGroup -> [Decl]
groupDecls dg = case dg of
@ -295,15 +265,11 @@ data Decl = Decl { dName :: !Name
, dInfix :: !Bool
, dFixity :: Maybe Fixity
, dDoc :: Maybe String
} deriving (Show,Generic)
instance NFData Decl where rnf = genericRnf
} deriving (Show, Generic, NFData)
data DeclDef = DPrim
| DExpr Expr
deriving (Show,Generic)
instance NFData DeclDef where rnf = genericRnf
deriving (Show, Generic, NFData)
--------------------------------------------------------------------------------

36
src/Cryptol/TypeCheck/InferTypes.hs
View File

@ -9,10 +9,13 @@
-- This module contains types used during type inference.
{-# LANGUAGE Safe #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.TypeCheck.InferTypes where
import Cryptol.TypeCheck.AST
@ -32,15 +35,12 @@ import qualified Data.IntMap as IntMap
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
data SolverConfig = SolverConfig
{ solverPath :: FilePath -- ^ The SMT solver to invoke
, solverArgs :: [String] -- ^ Additional arguments to pass to the solver
, solverVerbose :: Int -- ^ How verbose to be when type-checking
} deriving (Show, Generic)
instance NFData SolverConfig where rnf = genericRnf
} deriving (Show, Generic, NFData)
-- | The types of variables in the environment.
data VarType = ExtVar Schema -- ^ Known type
@ -66,9 +66,7 @@ data Goal = Goal
{ goalSource :: ConstraintSource -- ^ What it is about
, goalRange :: Range -- ^ Part of source code that caused goal
, goal :: Prop -- ^ What needs to be proved
} deriving (Show,Generic)
instance NFData Goal where rnf = genericRnf
} deriving (Show, Generic, NFData)
data HasGoal = HasGoal
{ hasName :: !Int
@ -81,9 +79,7 @@ data DelayedCt = DelayedCt
, dctForall :: [TParam]
, dctAsmps :: [Prop]
, dctGoals :: [Goal]
} deriving (Show,Generic)
instance NFData DelayedCt where rnf = genericRnf
} deriving (Show, Generic, NFData)
data Solved = Solved (Maybe Subst) [Goal] -- ^ Solved, assuming the sub-goals.
| Unsolved -- ^ We could not solve the goal.
@ -93,9 +89,7 @@ data Solved = Solved (Maybe Subst) [Goal] -- ^ Solved, assuming the sub-goals.
data Warning = DefaultingKind (P.TParam Name) P.Kind
| DefaultingWildType P.Kind
| DefaultingTo Doc Type
deriving (Show,Generic)
instance NFData Warning where rnf = genericRnf
deriving (Show, Generic, NFData)
-- | Various errors that might happen during type checking/inference
data Error = ErrorMsg Doc
@ -174,9 +168,7 @@ data Error = ErrorMsg Doc
| AmbiguousType [Name]
deriving (Show,Generic)
instance NFData Error where rnf = genericRnf
deriving (Show, Generic, NFData)
-- | Information about how a constraint came to be, used in error reporting.
data ConstraintSource
@ -191,14 +183,10 @@ data ConstraintSource
| CtPartialTypeFun TyFunName -- ^ Use of a partial type function.
| CtImprovement
| CtPattern Doc -- ^ Constraints arising from type-checking patterns
deriving (Show,Generic)
instance NFData ConstraintSource where rnf = genericRnf
deriving (Show, Generic, NFData)
data TyFunName = UserTyFun Name | BuiltInTyFun TFun
deriving (Show,Generic)
instance NFData TyFunName where rnf = genericRnf
deriving (Show, Generic, NFData)
instance PP TyFunName where
ppPrec c (UserTyFun x) = ppPrec c x

12
src/Cryptol/TypeCheck/Monad.hs
View File

@ -5,9 +5,12 @@
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE RecordWildCards, Safe #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE RecursiveDo #-}
module Cryptol.TypeCheck.Monad
( module Cryptol.TypeCheck.Monad
, module Cryptol.TypeCheck.InferTypes
@ -37,7 +40,6 @@ import MonadLib hiding (mapM)
import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
import Prelude ()
import Prelude.Compat
@ -67,9 +69,7 @@ data InferInput = InferInput
data NameSeeds = NameSeeds
{ seedTVar :: !Int
, seedGoal :: !Int
} deriving (Show, Generic)
instance NFData NameSeeds where rnf = genericRnf
} deriving (Show, Generic, NFData)
-- | The initial seeds, used when checking a fresh program.
nameSeeds :: NameSeeds

10
src/Cryptol/TypeCheck/Solver/InfNat.hs
View File

@ -10,20 +10,20 @@
-- element, and various arithmetic operators on them.
{-# LANGUAGE Safe #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.TypeCheck.Solver.InfNat where
import Data.Bits
import Cryptol.Utils.Panic
import GHC.Generics(Generic)
import Control.DeepSeq.Generics
import GHC.Generics (Generic)
import Control.DeepSeq
-- | Natural numbers with an infinity element
data Nat' = Nat Integer | Inf
deriving (Show,Eq,Ord,Generic)
instance NFData Nat' where rnf = genericRnf
deriving (Show, Eq, Ord, Generic, NFData)
fromNat :: Nat' -> Maybe Integer
fromNat n' =

17
src/Cryptol/Utils/PP.hs
View File

@ -7,13 +7,14 @@
-- Portability : portable
{-# LANGUAGE Safe #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternGuards #-}
module Cryptol.Utils.PP where
import Cryptol.Utils.Ident
import Control.DeepSeq
import Control.DeepSeq.Generics
import Control.Monad (mplus)
import Data.Maybe (fromMaybe)
import Data.String (IsString(..))
@ -31,9 +32,7 @@ import Prelude.Compat
-- in scope.
data NameDisp = EmptyNameDisp
| NameDisp (ModName -> Ident -> Maybe NameFormat)
deriving (Generic)
instance NFData NameDisp where rnf = genericRnf
deriving (Generic, NFData)
instance Show NameDisp where
show _ = "<NameDisp>"
@ -91,14 +90,12 @@ fixNameDisp disp (Doc f) = Doc (\ _ -> f disp)
-- Documents -------------------------------------------------------------------
newtype Doc = Doc (NameDisp -> PJ.Doc) deriving (Generic)
newtype Doc = Doc (NameDisp -> PJ.Doc) deriving (Generic, NFData)
instance Monoid Doc where
mempty = liftPJ PJ.empty
mappend = liftPJ2 (PJ.<>)
instance NFData Doc where rnf = genericRnf
runDoc :: NameDisp -> Doc -> PJ.Doc
runDoc names (Doc f) = f names
@ -137,9 +134,7 @@ optParens b body | b = parens body
-- | Information about associativity.
data Assoc = LeftAssoc | RightAssoc | NonAssoc
deriving (Show,Eq,Generic)
instance NFData Assoc where rnf = genericRnf
deriving (Show, Eq, Generic, NFData)
-- | Information about an infix expression of some sort.
data Infix op thing = Infix