mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-22 19:41:22 +03:00
Fix build with GHC 8.4.1
This commit is contained in:
parent
6fdc1ff326
commit
9d344bb452
@ -10,6 +10,7 @@
|
||||
module OptParser where
|
||||
|
||||
import Data.Monoid (Endo(..))
|
||||
import Data.Semigroup
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
@ -18,14 +19,17 @@ data OptParser opt
|
||||
= OptSuccess (Endo opt)
|
||||
| OptFailure [String]
|
||||
|
||||
instance Monoid (OptParser opt) where
|
||||
mempty = OptSuccess mempty
|
||||
l `mappend` r = case (l,r) of
|
||||
instance Semigroup (OptParser opt) where
|
||||
l <> r = case (l,r) of
|
||||
(OptSuccess f,OptSuccess g) -> OptSuccess (f `mappend` g)
|
||||
(OptFailure a,OptFailure b) -> OptFailure (a `mappend` b)
|
||||
(OptFailure _,_) -> l
|
||||
(_,OptFailure _) -> r
|
||||
|
||||
instance Monoid (OptParser opt) where
|
||||
mempty = OptSuccess mempty
|
||||
mappend = (<>)
|
||||
|
||||
runOptParser :: opt -> OptParser opt -> Either [String] opt
|
||||
runOptParser def parse = case parse of
|
||||
OptSuccess update -> Right (appEndo update def)
|
||||
|
@ -37,13 +37,14 @@ import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.PP hiding ((<>))
|
||||
|
||||
import Control.Monad
|
||||
import qualified Data.Sequence as Seq
|
||||
import Data.List
|
||||
import Data.Maybe
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Semigroup
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
@ -457,6 +458,13 @@ data ListEnv b w i = ListEnv
|
||||
, leTypes :: !TypeEnv
|
||||
}
|
||||
|
||||
instance Semigroup (ListEnv b w i) where
|
||||
l <> r = ListEnv
|
||||
{ leVars = Map.union (leVars l) (leVars r)
|
||||
, leStatic = Map.union (leStatic l) (leStatic r)
|
||||
, leTypes = Map.union (leTypes l) (leTypes r)
|
||||
}
|
||||
|
||||
instance Monoid (ListEnv b w i) where
|
||||
mempty = ListEnv
|
||||
{ leVars = Map.empty
|
||||
@ -464,11 +472,7 @@ instance Monoid (ListEnv b w i) where
|
||||
, leTypes = Map.empty
|
||||
}
|
||||
|
||||
mappend l r = ListEnv
|
||||
{ leVars = Map.union (leVars l) (leVars r)
|
||||
, leStatic = Map.union (leStatic l) (leStatic r)
|
||||
, leTypes = Map.union (leTypes l) (leTypes r)
|
||||
}
|
||||
mappend l r = l <> r
|
||||
|
||||
toListEnv :: GenEvalEnv b w i -> ListEnv b w i
|
||||
toListEnv e =
|
||||
|
@ -20,10 +20,11 @@ import Cryptol.Eval.Value
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.TypeCheck.AST
|
||||
import Cryptol.TypeCheck.Solver.InfNat
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.PP hiding ((<>))
|
||||
|
||||
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Semigroup
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
@ -38,16 +39,19 @@ data GenEvalEnv b w i = EvalEnv
|
||||
, envTypes :: !TypeEnv
|
||||
} deriving (Generic, NFData)
|
||||
|
||||
instance Semigroup (GenEvalEnv b w i) where
|
||||
l <> r = EvalEnv
|
||||
{ envVars = Map.union (envVars l) (envVars r)
|
||||
, envTypes = Map.union (envTypes l) (envTypes r)
|
||||
}
|
||||
|
||||
instance Monoid (GenEvalEnv b w i) where
|
||||
mempty = EvalEnv
|
||||
{ envVars = Map.empty
|
||||
, envTypes = Map.empty
|
||||
}
|
||||
|
||||
mappend l r = EvalEnv
|
||||
{ envVars = Map.union (envVars l) (envVars r)
|
||||
, envTypes = Map.union (envTypes l) (envTypes r)
|
||||
}
|
||||
mappend l r = l <> r
|
||||
|
||||
ppEnv :: BitWord b w i => PPOpts -> GenEvalEnv b w i -> Eval Doc
|
||||
ppEnv opts env = brackets . fsep <$> mapM bind (Map.toList (envVars env))
|
||||
|
@ -23,6 +23,7 @@
|
||||
> import Data.Ord (comparing)
|
||||
> import Data.Map (Map)
|
||||
> import qualified Data.Map as Map
|
||||
> import Data.Semigroup
|
||||
> import qualified Data.Text as T (pack)
|
||||
>
|
||||
> import Cryptol.ModuleSystem.Name (asPrim)
|
||||
@ -33,7 +34,7 @@
|
||||
> import Cryptol.Prims.Eval (lg2, divModPoly)
|
||||
> import Cryptol.Utils.Ident (Ident, mkIdent)
|
||||
> import Cryptol.Utils.Panic (panic)
|
||||
> import Cryptol.Utils.PP
|
||||
> import Cryptol.Utils.PP hiding ((<>))
|
||||
>
|
||||
> import qualified Cryptol.ModuleSystem as M
|
||||
> import qualified Cryptol.ModuleSystem.Env as M (loadedModules)
|
||||
@ -250,15 +251,18 @@ and type variables that are in scope at any point.
|
||||
> , envTypes :: !(Map TVar (Either Nat' TValue))
|
||||
> }
|
||||
>
|
||||
> instance Semigroup Env where
|
||||
> l <> r = Env
|
||||
> { envVars = Map.union (envVars l) (envVars r)
|
||||
> , envTypes = Map.union (envTypes l) (envTypes r)
|
||||
> }
|
||||
>
|
||||
> instance Monoid Env where
|
||||
> mempty = Env
|
||||
> { envVars = Map.empty
|
||||
> , envTypes = Map.empty
|
||||
> }
|
||||
> mappend l r = Env
|
||||
> { envVars = Map.union (envVars l) (envVars r)
|
||||
> , envTypes = Map.union (envTypes l) (envTypes r)
|
||||
> }
|
||||
> mappend l r = l <> r
|
||||
>
|
||||
> -- | Bind a variable in the evaluation environment.
|
||||
> bindVar :: (Name, Value) -> Env -> Env
|
||||
|
@ -46,6 +46,7 @@ import Numeric (showIntAtBase)
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
-- Values ----------------------------------------------------------------------
|
||||
|
||||
|
@ -9,7 +9,7 @@ import Data.Set ( Set )
|
||||
import qualified Data.Set as Set
|
||||
import Data.Map ( Map )
|
||||
import qualified Data.Map as Map
|
||||
import Data.Monoid ((<>))
|
||||
import Data.Semigroup
|
||||
|
||||
import Cryptol.TypeCheck.AST
|
||||
|
||||
@ -23,13 +23,16 @@ data Deps = Deps { valDeps :: Set Name
|
||||
-- ^ Undefined type params (e.d. mod params)
|
||||
} deriving Eq
|
||||
|
||||
instance Semigroup Deps where
|
||||
d1 <> d2 = mconcat [d1,d2]
|
||||
|
||||
instance Monoid Deps where
|
||||
mempty = Deps { valDeps = Set.empty
|
||||
, tyDeps = Set.empty
|
||||
, tyParams = Set.empty
|
||||
}
|
||||
|
||||
mappend d1 d2 = mconcat [d1,d2]
|
||||
mappend d1 d2 = d1 <> d2
|
||||
|
||||
mconcat ds = Deps { valDeps = Set.unions (map valDeps ds)
|
||||
, tyDeps = Set.unions (map tyDeps ds)
|
||||
|
@ -30,8 +30,8 @@ import Control.Monad (guard,mplus)
|
||||
import qualified Control.Exception as X
|
||||
import Data.Function (on)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Monoid ((<>))
|
||||
import Data.Maybe(fromMaybe)
|
||||
import Data.Semigroup
|
||||
import System.Directory (getAppUserDataDirectory, getCurrentDirectory)
|
||||
import System.Environment(getExecutablePath)
|
||||
import System.FilePath ((</>), normalise, joinPath, splitPath, takeDirectory)
|
||||
@ -224,14 +224,17 @@ data LoadedModules = LoadedModules
|
||||
getLoadedModules :: LoadedModules -> [LoadedModule]
|
||||
getLoadedModules x = lmLoadedParamModules x ++ lmLoadedModules x
|
||||
|
||||
instance Semigroup LoadedModules where
|
||||
l <> r = LoadedModules
|
||||
{ lmLoadedModules = List.unionBy ((==) `on` lmName)
|
||||
(lmLoadedModules l) (lmLoadedModules r)
|
||||
, lmLoadedParamModules = lmLoadedParamModules l ++ lmLoadedParamModules r }
|
||||
|
||||
instance Monoid LoadedModules where
|
||||
mempty = LoadedModules { lmLoadedModules = []
|
||||
, lmLoadedParamModules = []
|
||||
}
|
||||
mappend l r = LoadedModules
|
||||
{ lmLoadedModules = List.unionBy ((==) `on` lmName)
|
||||
(lmLoadedModules l) (lmLoadedModules r)
|
||||
, lmLoadedParamModules = lmLoadedParamModules l ++ lmLoadedParamModules r }
|
||||
mappend l r = l <> r
|
||||
|
||||
data LoadedModule = LoadedModule
|
||||
{ lmName :: ModName
|
||||
@ -295,17 +298,20 @@ data DynamicEnv = DEnv
|
||||
, deEnv :: EvalEnv
|
||||
} deriving (Generic, NFData)
|
||||
|
||||
instance Semigroup DynamicEnv where
|
||||
de1 <> de2 = DEnv
|
||||
{ deNames = deNames de1 <> deNames de2
|
||||
, deDecls = deDecls de1 <> deDecls de2
|
||||
, deEnv = deEnv de1 <> deEnv de2
|
||||
}
|
||||
|
||||
instance Monoid DynamicEnv where
|
||||
mempty = DEnv
|
||||
{ deNames = mempty
|
||||
, deDecls = mempty
|
||||
, deEnv = mempty
|
||||
}
|
||||
mappend de1 de2 = DEnv
|
||||
{ deNames = deNames de1 <> deNames de2
|
||||
, deDecls = deDecls de1 <> deDecls de2
|
||||
, deEnv = deEnv de1 <> deEnv de2
|
||||
}
|
||||
mappend de1 de2 = de1 <> de2
|
||||
|
||||
-- | Build 'IfaceDecls' that correspond to all of the bindings in the
|
||||
-- dynamic environment.
|
||||
|
@ -4,6 +4,7 @@ module Cryptol.ModuleSystem.Exports where
|
||||
import Data.Set(Set)
|
||||
import qualified Data.Set as Set
|
||||
import Data.Foldable(fold)
|
||||
import Data.Semigroup
|
||||
import Control.DeepSeq(NFData)
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
@ -31,11 +32,14 @@ data ExportSpec name = ExportSpec { eTypes :: Set name
|
||||
|
||||
instance NFData name => NFData (ExportSpec name)
|
||||
|
||||
instance Ord name => Semigroup (ExportSpec name) where
|
||||
l <> r = ExportSpec { eTypes = eTypes l <> eTypes r
|
||||
, eBinds = eBinds l <> eBinds r
|
||||
}
|
||||
|
||||
instance Ord name => Monoid (ExportSpec name) where
|
||||
mempty = ExportSpec { eTypes = mempty, eBinds = mempty }
|
||||
mappend l r = ExportSpec { eTypes = mappend (eTypes l) (eTypes r)
|
||||
, eBinds = mappend (eBinds l) (eBinds r)
|
||||
}
|
||||
mempty = ExportSpec { eTypes = mempty, eBinds = mempty }
|
||||
mappend = (<>)
|
||||
|
||||
-- | Add a binding name to the export list, if it should be exported.
|
||||
exportBind :: Ord name => TopLevel name -> ExportSpec name
|
||||
|
@ -30,6 +30,7 @@ import Cryptol.Utils.Ident (ModName)
|
||||
import Cryptol.Parser.Position(Located)
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import Data.Semigroup
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
@ -65,13 +66,16 @@ data IfaceDecls = IfaceDecls
|
||||
, ifDecls :: Map.Map Name IfaceDecl
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
instance Monoid IfaceDecls where
|
||||
mempty = IfaceDecls Map.empty Map.empty Map.empty
|
||||
mappend l r = IfaceDecls
|
||||
instance Semigroup IfaceDecls where
|
||||
l <> r = IfaceDecls
|
||||
{ ifTySyns = Map.union (ifTySyns l) (ifTySyns r)
|
||||
, ifNewtypes = Map.union (ifNewtypes l) (ifNewtypes r)
|
||||
, ifDecls = Map.union (ifDecls l) (ifDecls r)
|
||||
}
|
||||
|
||||
instance Monoid IfaceDecls where
|
||||
mempty = IfaceDecls Map.empty Map.empty Map.empty
|
||||
mappend l r = l <> r
|
||||
mconcat ds = IfaceDecls
|
||||
{ ifTySyns = Map.unions (map ifTySyns ds)
|
||||
, ifNewtypes = Map.unions (map ifNewtypes ds)
|
||||
|
@ -43,7 +43,7 @@ import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
import Prelude.Compat hiding ((<>))
|
||||
|
||||
-- Errors ----------------------------------------------------------------------
|
||||
|
||||
|
@ -62,7 +62,7 @@ import Data.Ord (comparing)
|
||||
import GHC.Generics (Generic)
|
||||
import MonadLib
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
import Prelude.Compat hiding ((<>))
|
||||
|
||||
|
||||
-- Names -----------------------------------------------------------------------
|
||||
|
@ -22,13 +22,14 @@ import Cryptol.ModuleSystem.Name
|
||||
import Cryptol.Parser.AST
|
||||
import Cryptol.Parser.Position
|
||||
import qualified Cryptol.TypeCheck.AST as T
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.PP hiding ((<>))
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
|
||||
import Data.List (nub)
|
||||
import Data.Maybe (catMaybes,fromMaybe,mapMaybe)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import qualified Data.Set as Set
|
||||
import Data.Semigroup
|
||||
import MonadLib (runId,Id)
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
@ -60,6 +61,12 @@ lookupTypeNames qn ro = Map.findWithDefault [] qn (neTypes ro)
|
||||
|
||||
|
||||
|
||||
instance Semigroup NamingEnv where
|
||||
l <> r =
|
||||
NamingEnv { neExprs = Map.unionWith merge (neExprs l) (neExprs r)
|
||||
, neTypes = Map.unionWith merge (neTypes l) (neTypes r)
|
||||
, neFixity = Map.union (neFixity l) (neFixity r) }
|
||||
|
||||
instance Monoid NamingEnv where
|
||||
mempty =
|
||||
NamingEnv { neExprs = Map.empty
|
||||
@ -68,10 +75,7 @@ instance Monoid NamingEnv where
|
||||
|
||||
-- NOTE: merging the fixity maps is a special case that just prefers the left
|
||||
-- entry, as they're already keyed by a name with a unique
|
||||
mappend l r =
|
||||
NamingEnv { neExprs = Map.unionWith merge (neExprs l) (neExprs r)
|
||||
, neTypes = Map.unionWith merge (neTypes l) (neTypes r)
|
||||
, neFixity = Map.union (neFixity l) (neFixity r) }
|
||||
mappend l r = l <> r
|
||||
|
||||
mconcat envs =
|
||||
NamingEnv { neExprs = Map.unionsWith merge (map neExprs envs)
|
||||
@ -190,14 +194,17 @@ namingEnv' a supply = runId (runSupplyT supply (runBuild (namingEnv a)))
|
||||
|
||||
newtype BuildNamingEnv = BuildNamingEnv { runBuild :: SupplyT Id NamingEnv }
|
||||
|
||||
instance Monoid BuildNamingEnv where
|
||||
mempty = BuildNamingEnv (pure mempty)
|
||||
|
||||
mappend (BuildNamingEnv a) (BuildNamingEnv b) = BuildNamingEnv $
|
||||
instance Semigroup BuildNamingEnv where
|
||||
BuildNamingEnv a <> BuildNamingEnv b = BuildNamingEnv $
|
||||
do x <- a
|
||||
y <- b
|
||||
return (mappend x y)
|
||||
|
||||
instance Monoid BuildNamingEnv where
|
||||
mempty = BuildNamingEnv (pure mempty)
|
||||
|
||||
mappend = (<>)
|
||||
|
||||
mconcat bs = BuildNamingEnv $
|
||||
do ns <- sequence (map runBuild bs)
|
||||
return (mconcat ns)
|
||||
|
@ -41,6 +41,7 @@ import qualified Data.Foldable as F
|
||||
import Data.Map.Strict ( Map )
|
||||
import qualified Data.Map.Strict as Map
|
||||
import qualified Data.Sequence as Seq
|
||||
import qualified Data.Semigroup as S
|
||||
import qualified Data.Set as Set
|
||||
import Data.String (IsString(..))
|
||||
import MonadLib hiding (mapM, mapM_)
|
||||
@ -49,7 +50,7 @@ import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
import Prelude.Compat hiding ((<>))
|
||||
|
||||
-- Errors ----------------------------------------------------------------------
|
||||
|
||||
@ -198,15 +199,19 @@ data RW = RW
|
||||
newtype RenameM a = RenameM
|
||||
{ unRenameM :: ReaderT RO (StateT RW Lift) a }
|
||||
|
||||
instance Monoid a => Monoid (RenameM a) where
|
||||
instance S.Semigroup a => S.Semigroup (RenameM a) where
|
||||
{-# INLINE (<>) #-}
|
||||
a <> b =
|
||||
do x <- a
|
||||
y <- b
|
||||
return (x S.<> y)
|
||||
|
||||
instance (S.Semigroup a, Monoid a) => Monoid (RenameM a) where
|
||||
{-# INLINE mempty #-}
|
||||
mempty = return mempty
|
||||
|
||||
{-# INLINE mappend #-}
|
||||
mappend a b =
|
||||
do x <- a
|
||||
y <- b
|
||||
return (mappend x y)
|
||||
mappend = (S.<>)
|
||||
|
||||
instance Functor RenameM where
|
||||
{-# INLINE fmap #-}
|
||||
|
@ -87,7 +87,7 @@ import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
import Prelude.Compat hiding ((<>))
|
||||
|
||||
-- AST -------------------------------------------------------------------------
|
||||
|
||||
|
@ -16,6 +16,7 @@ import Cryptol.Utils.Panic (panic)
|
||||
|
||||
import Control.DeepSeq
|
||||
import GHC.Generics (Generic)
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
|
||||
-- Names -----------------------------------------------------------------------
|
||||
|
@ -31,6 +31,7 @@ import Cryptol.Parser.LexerUtils (Config(..),defaultConfig)
|
||||
import Cryptol.Parser.ParserUtils
|
||||
import Cryptol.Parser.Unlit (guessPreProc)
|
||||
import Cryptol.Utils.PP
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
removeIncludesModule :: FilePath -> Module PName -> IO (Either [IncludeError] (Module PName))
|
||||
removeIncludesModule modPath m = runNoIncM modPath (noIncludeModule m)
|
||||
|
@ -33,7 +33,7 @@ import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
import Prelude.Compat hiding ((<>))
|
||||
|
||||
class RemovePatterns t where
|
||||
-- | Eliminate all patterns in a program.
|
||||
|
@ -34,7 +34,7 @@ import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
import Prelude.Compat hiding ((<>))
|
||||
|
||||
parseString :: Config -> ParseM a -> String -> Either ParseError a
|
||||
parseString cfg p cs = parse cfg p (T.pack cs)
|
||||
|
@ -20,6 +20,7 @@ import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
|
||||
import Cryptol.Utils.PP
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
data Located a = Located { srcRange :: !Range, thing :: !a }
|
||||
deriving (Eq, Show, Generic, NFData)
|
||||
|
@ -45,6 +45,7 @@ import Cryptol.TypeCheck.Monad(withParamType,withParameterConstraints)
|
||||
import Cryptol.Utils.Ident (exprModName,packIdent)
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
tcModule :: P.Module Name -> InferInput -> IO (InferOutput Module)
|
||||
tcModule m inp = runInferM inp
|
||||
|
@ -46,6 +46,7 @@ import Control.DeepSeq
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.IntMap as IntMap
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
|
||||
-- | A Cryptol module.
|
||||
|
@ -18,6 +18,7 @@ import Cryptol.TypeCheck.InferTypes
|
||||
import Cryptol.TypeCheck.Subst
|
||||
import Cryptol.ModuleSystem.Name(Name)
|
||||
import Cryptol.Utils.Ident(Ident)
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
cleanupErrors :: [(Range,Error)] -> [(Range,Error)]
|
||||
cleanupErrors = dropErrorsFromSameLoc
|
||||
|
@ -33,6 +33,7 @@ import qualified Data.Set as Set
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
data SolverConfig = SolverConfig
|
||||
{ solverPath :: FilePath -- ^ The SMT solver to invoke
|
||||
|
@ -22,6 +22,7 @@ import Cryptol.Utils.Ident (Ident,unpackIdent)
|
||||
import Cryptol.Parser.AST ( Located(..))
|
||||
import Cryptol.ModuleSystem.Name
|
||||
import Text.PrettyPrint
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
-- ShowParseable prints out a cryptol program in a way that it's parseable by Coq (and likely other things)
|
||||
-- Used mainly for reasoning about the semantics of cryptol programs in Coq (https://github.com/GaloisInc/cryptol-semantics)
|
||||
|
@ -20,6 +20,7 @@ import Cryptol.Utils.PP hiding (int)
|
||||
import Data.Map ( Map )
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe (catMaybes)
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
|
||||
-- | Only meaningful for numeric types
|
||||
|
@ -5,6 +5,7 @@ import Data.Map(Map)
|
||||
import Cryptol.TypeCheck.Type
|
||||
import Cryptol.TypeCheck.PP
|
||||
import Cryptol.TypeCheck.Solver.Numeric.Interval
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
type Ctxt = Map TVar Interval
|
||||
|
||||
|
@ -22,6 +22,7 @@ import Cryptol.Utils.Ident (Ident)
|
||||
import Cryptol.TypeCheck.PP
|
||||
import Cryptol.TypeCheck.Solver.InfNat
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Prelude hiding ((<>))
|
||||
|
||||
infix 4 =#=, >==
|
||||
infixr 5 `tFun`
|
||||
|
@ -17,13 +17,14 @@ import Cryptol.Utils.Ident
|
||||
import Control.DeepSeq
|
||||
import Control.Monad (mplus)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import qualified Data.Semigroup as S
|
||||
import Data.String (IsString(..))
|
||||
import qualified Data.Text as T
|
||||
import GHC.Generics (Generic)
|
||||
import qualified Text.PrettyPrint as PJ
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
import Prelude.Compat hiding ((<>))
|
||||
|
||||
-- Name Displaying -------------------------------------------------------------
|
||||
|
||||
@ -38,14 +39,15 @@ data NameDisp = EmptyNameDisp
|
||||
instance Show NameDisp where
|
||||
show _ = "<NameDisp>"
|
||||
|
||||
instance S.Semigroup NameDisp where
|
||||
NameDisp f <> NameDisp g = NameDisp (\m n -> f m n `mplus` g m n)
|
||||
EmptyNameDisp <> EmptyNameDisp = EmptyNameDisp
|
||||
EmptyNameDisp <> x = x
|
||||
x <> _ = x
|
||||
|
||||
instance Monoid NameDisp where
|
||||
mempty = EmptyNameDisp
|
||||
|
||||
mappend (NameDisp f) (NameDisp g) = NameDisp (\m n -> f m n `mplus` g m n)
|
||||
mappend EmptyNameDisp EmptyNameDisp = EmptyNameDisp
|
||||
mappend EmptyNameDisp x = x
|
||||
mappend x _ = x
|
||||
|
||||
mappend = (S.<>)
|
||||
|
||||
data NameFormat = UnQualified
|
||||
| Qualified !ModName
|
||||
@ -93,9 +95,12 @@ fixNameDisp disp (Doc f) = Doc (\ _ -> f disp)
|
||||
|
||||
newtype Doc = Doc (NameDisp -> PJ.Doc) deriving (Generic, NFData)
|
||||
|
||||
instance S.Semigroup Doc where
|
||||
(<>) = liftPJ2 (PJ.<>)
|
||||
|
||||
instance Monoid Doc where
|
||||
mempty = liftPJ PJ.empty
|
||||
mappend = liftPJ2 (PJ.<>)
|
||||
mappend = (S.<>)
|
||||
|
||||
runDoc :: NameDisp -> Doc -> PJ.Doc
|
||||
runDoc names (Doc f) = f names
|
||||
|
Loading…
Reference in New Issue
Block a user