rewire-embedder-2.8: A ReWire-to-Isabelle embedder

Safe Haskell	Trustworthy
Language	Haskell2010

Embedder.Builtins

Synopsis

data Builtin
- = Error
- | Extern
- | Cryptol
- | Bind
- | Return
- | Put
- | Get
- | Signal
- | Lift
- | Extrude
- | VecFromList
- | VecReplicate
- | VecReverse
- | VecSlice
- | VecRSlice
- | VecIndex
- | VecIndexProxy
- | VecConcat
- | VecMap
- | VecGenerate
- | Finite
- | FiniteMinBound
- | FiniteMaxBound
- | ToFinite
- | ToFiniteMod
- | FromFinite
- | NatVal
- | Bits
- | Resize
- | BitSlice
- | BitIndex
- | Add
- | Sub
- | Mul
- | Div
- | Mod
- | Pow
- | LAnd
- | LOr
- | And
- | Or
- | XOr
- | XNor
- | LShift
- | RShift
- | RShiftArith
- | Eq
- | Gt
- | GtEq
- | Lt
- | LtEq
- | LNot
- | Not
- | RAnd
- | RNAnd
- | ROr
- | RNor
- | RXOr
- | RXNor
- | MSBit
builtinName :: Builtin -> Text
builtins :: [(Text, Builtin)]
data TyBuiltin
- = TyInteger
- | TyString
- | TyBool
- | TyUnit
- | TyFun
- | TyReacT
- | TyStateT
- | TyIdentity
- | TyState
- | TyRe
- | TyDev
- | TyStateDev
- | TyS
- | TyProd
- | TyList
- | TyVec
- | TyProxy
- | TyFin
- | TyPlus
- | TyNeg
- | TyRef
s2tb :: Text -> Maybe TyBuiltin
tb2s :: TyBuiltin -> Text
tybuiltins :: [(Text, TyBuiltin)]
builtinUserQName :: [(Builtin, Text)]
builtinUserName :: [(Builtin, Text)]
data RWUserOp
- = RWBuiltin Builtin
- | CompDot
- | CompDol
- | BindI
- | BindS
- | BindR
- | BindRInf
- | Seq
- | SeqI
- | SeqS
- | SeqR
- | SeqRInf
- | RBindI
- | RBindS
- | RBindR
- | RBindRInf
- | ReturnI
- | ReturnS
- | ReturnR
- | LiftS
- | LiftR
- | WordIndexProxy
- | WordIndexFin
- | BAnd
- | BOr
- | BXOr
- | FinAdd
- | FinSub
- | FinMul
- | FinDiv
- | FinEq
- | FinLt
- | WordSlice
- | WordIndex
- | NEq
- | Update
- | VecLastIndexProxy
rwu2s :: RWUserOp -> Maybe Text
s2rwu :: Text -> Maybe RWUserOp
rwu2qn :: RWUserOp -> Maybe Text
qn2rwu :: Text -> Maybe RWUserOp

Documentation

Instances

Instances details

Instance details

Defined in ReWire.Builtins

Methods

rnf :: Builtin -> () #

Instance details

Defined in ReWire.Builtins

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Builtin -> c Builtin #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Builtin #

toConstr :: Builtin -> Constr #

dataTypeOf :: Builtin -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Builtin) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Builtin) #

gmapT :: (forall b. Data b => b -> b) -> Builtin -> Builtin #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Builtin -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Builtin -> r #

gmapQ :: (forall d. Data d => d -> u) -> Builtin -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Builtin -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Builtin -> m Builtin #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Builtin -> m Builtin #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Builtin -> m Builtin #

Bounded Builtin

Instance details

Defined in ReWire.Builtins

Methods

minBound :: Builtin #

maxBound :: Builtin #

Instance details

Defined in ReWire.Builtins

Methods

succ :: Builtin -> Builtin #

pred :: Builtin -> Builtin #

toEnum :: Int -> Builtin #

fromEnum :: Builtin -> Int #

enumFrom :: Builtin -> [Builtin] #

enumFromThen :: Builtin -> Builtin -> [Builtin] #

enumFromTo :: Builtin -> Builtin -> [Builtin] #

enumFromThenTo :: Builtin -> Builtin -> Builtin -> [Builtin] #

Generic Builtin

Instance details

Defined in ReWire.Builtins

Associated Types

type Rep Builtin

Instance details

Defined in ReWire.Builtins

type Rep Builtin = D1 ('MetaData "Builtin" "ReWire.Builtins" "rewire-frontend-2.8-6fn13RghMuk7zNqk4evZ4E" 'False) (((((C1 ('MetaCons "Error" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Extern" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cryptol" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Bind" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Return" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Put" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Get" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Signal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Extrude" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecFromList" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "VecReplicate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecReverse" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "VecSlice" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecRSlice" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "VecIndex" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "VecIndexProxy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecConcat" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "VecMap" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecGenerate" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Finite" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FiniteMinBound" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "FiniteMaxBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ToFinite" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ToFiniteMod" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FromFinite" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "NatVal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Bits" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Resize" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BitSlice" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "BitIndex" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Add" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Sub" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Mul" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Div" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Mod" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Pow" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "LAnd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LOr" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "And" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Or" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "XOr" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "XNor" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LShift" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RShift" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "RShiftArith" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Eq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Gt" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "GtEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Lt" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LtEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LNot" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Not" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RAnd" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RNAnd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ROr" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RNor" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RXOr" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RXNor" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MSBit" 'PrefixI 'False) (U1 :: Type -> Type)))))))

Methods

from :: Builtin -> Rep Builtin x #

to :: Rep Builtin x -> Builtin #

Instance details

Defined in ReWire.Builtins

Methods

showsPrec :: Int -> Builtin -> ShowS #

show :: Builtin -> String #

showList :: [Builtin] -> ShowS #

Instance details

Defined in ReWire.Builtins

Methods

(==) :: Builtin -> Builtin -> Bool #

(/=) :: Builtin -> Builtin -> Bool #

Instance details

Defined in ReWire.Builtins

Methods

compare :: Builtin -> Builtin -> Ordering #

(<) :: Builtin -> Builtin -> Bool #

(<=) :: Builtin -> Builtin -> Bool #

(>) :: Builtin -> Builtin -> Bool #

(>=) :: Builtin -> Builtin -> Bool #

max :: Builtin -> Builtin -> Builtin #

min :: Builtin -> Builtin -> Builtin #

Hashable Builtin

Instance details

Defined in ReWire.Builtins

Methods

hashWithSalt :: Int -> Builtin -> Int

hash :: Builtin -> Int

Instance details

Defined in ReWire.Builtins

Methods

pretty :: Builtin -> Doc ann #

prettyList :: [Builtin] -> Doc ann

TextShow Builtin

Instance details

Defined in ReWire.Builtins

Methods

showbPrec :: Int -> Builtin -> Builder #

showb :: Builtin -> Builder #

showbList :: [Builtin] -> Builder

showtPrec :: Int -> Builtin -> Text

showt :: Builtin -> Text #

showtList :: [Builtin] -> Text

showtlPrec :: Int -> Builtin -> Text

showtl :: Builtin -> Text

showtlList :: [Builtin] -> Text

type Rep Builtin

Instance details

Defined in ReWire.Builtins

type Rep Builtin = D1 ('MetaData "Builtin" "ReWire.Builtins" "rewire-frontend-2.8-6fn13RghMuk7zNqk4evZ4E" 'False) (((((C1 ('MetaCons "Error" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Extern" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Cryptol" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Bind" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Return" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Put" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Get" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Signal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Extrude" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecFromList" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "VecReplicate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecReverse" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "VecSlice" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecRSlice" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "VecIndex" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "VecIndexProxy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecConcat" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "VecMap" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecGenerate" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Finite" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FiniteMinBound" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "FiniteMaxBound" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ToFinite" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ToFiniteMod" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FromFinite" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "NatVal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Bits" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Resize" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BitSlice" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "BitIndex" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Add" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Sub" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Mul" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Div" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Mod" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Pow" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "LAnd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LOr" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "And" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Or" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "XOr" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "XNor" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LShift" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RShift" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "RShiftArith" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Eq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Gt" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "GtEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Lt" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LtEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LNot" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "Not" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RAnd" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RNAnd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ROr" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RNor" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RXOr" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RXNor" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MSBit" 'PrefixI 'False) (U1 :: Type -> Type)))))))

builtinName :: Builtin -> Text #

builtins :: [(Text, Builtin)] #

data TyBuiltin Source #

Type builtins type (+), type GHC.Monad, type GHC.MonadTrans, KnownNat Identity, ReacT, StateT, Vec, Finite, Ref (..), Proxy (..) Maybe, Either, Bool Products?

Primitives Defined Types/Data structs: Monad, MonadTrans, Ref a=Ref String, Proxy (n::Nat)=Proxy Imported Types/Data structs: type(+),type(Nat),Identity, ReacT, StateT, Integer, String, Bool, Vec=Vector, KnownNat, Finite

Constructors

TyInteger
TyString
TyBool
TyUnit
TyFun
TyReacT
TyStateT
TyIdentity
TyState
TyRe
TyDev
TyStateDev
TyS
TyProd
TyList
TyVec
TyProxy
TyFin
TyPlus
TyNeg
TyRef

Instances

Instances details

NFData TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

Methods

rnf :: TyBuiltin -> () #

Data TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TyBuiltin -> c TyBuiltin #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TyBuiltin #

toConstr :: TyBuiltin -> Constr #

dataTypeOf :: TyBuiltin -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TyBuiltin) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TyBuiltin) #

gmapT :: (forall b. Data b => b -> b) -> TyBuiltin -> TyBuiltin #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TyBuiltin -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TyBuiltin -> r #

gmapQ :: (forall d. Data d => d -> u) -> TyBuiltin -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TyBuiltin -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TyBuiltin -> m TyBuiltin #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TyBuiltin -> m TyBuiltin #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TyBuiltin -> m TyBuiltin #

Bounded TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

Methods

minBound :: TyBuiltin #

maxBound :: TyBuiltin #

Enum TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

Methods

succ :: TyBuiltin -> TyBuiltin #

pred :: TyBuiltin -> TyBuiltin #

toEnum :: Int -> TyBuiltin #

fromEnum :: TyBuiltin -> Int #

enumFrom :: TyBuiltin -> [TyBuiltin] #

enumFromThen :: TyBuiltin -> TyBuiltin -> [TyBuiltin] #

enumFromTo :: TyBuiltin -> TyBuiltin -> [TyBuiltin] #

enumFromThenTo :: TyBuiltin -> TyBuiltin -> TyBuiltin -> [TyBuiltin] #

Generic TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

Associated Types

type Rep TyBuiltin

Instance details

Defined in Embedder.Builtins

type Rep TyBuiltin = D1 ('MetaData "TyBuiltin" "Embedder.Builtins" "rewire-embedder-2.8-G94ytt72LAgDf9UAeQPb84" 'False) ((((C1 ('MetaCons "TyInteger" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyString" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TyBool" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TyUnit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyFun" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TyReacT" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyStateT" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TyIdentity" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TyState" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyRe" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "TyDev" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyStateDev" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TyS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TyProd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyList" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TyVec" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TyProxy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyFin" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TyPlus" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TyNeg" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyRef" 'PrefixI 'False) (U1 :: Type -> Type))))))

Methods

from :: TyBuiltin -> Rep TyBuiltin x #

to :: Rep TyBuiltin x -> TyBuiltin #

Show TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

Methods

showsPrec :: Int -> TyBuiltin -> ShowS #

show :: TyBuiltin -> String #

showList :: [TyBuiltin] -> ShowS #

Eq TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

Methods

(==) :: TyBuiltin -> TyBuiltin -> Bool #

(/=) :: TyBuiltin -> TyBuiltin -> Bool #

Ord TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

Methods

compare :: TyBuiltin -> TyBuiltin -> Ordering #

(<) :: TyBuiltin -> TyBuiltin -> Bool #

(<=) :: TyBuiltin -> TyBuiltin -> Bool #

(>) :: TyBuiltin -> TyBuiltin -> Bool #

(>=) :: TyBuiltin -> TyBuiltin -> Bool #

max :: TyBuiltin -> TyBuiltin -> TyBuiltin #

min :: TyBuiltin -> TyBuiltin -> TyBuiltin #

Hashable TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

Methods

hashWithSalt :: Int -> TyBuiltin -> Int

hash :: TyBuiltin -> Int

Pretty TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

Methods

pretty :: TyBuiltin -> Doc ann #

prettyList :: [TyBuiltin] -> Doc ann

TextShow TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

Methods

showbPrec :: Int -> TyBuiltin -> Builder #

showb :: TyBuiltin -> Builder #

showbList :: [TyBuiltin] -> Builder

showtPrec :: Int -> TyBuiltin -> Text

showt :: TyBuiltin -> Text #

showtList :: [TyBuiltin] -> Text

showtlPrec :: Int -> TyBuiltin -> Text

showtl :: TyBuiltin -> Text

showtlList :: [TyBuiltin] -> Text

type Rep TyBuiltin Source #

Instance details

Defined in Embedder.Builtins

type Rep TyBuiltin = D1 ('MetaData "TyBuiltin" "Embedder.Builtins" "rewire-embedder-2.8-G94ytt72LAgDf9UAeQPb84" 'False) ((((C1 ('MetaCons "TyInteger" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyString" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TyBool" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TyUnit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyFun" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TyReacT" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyStateT" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TyIdentity" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TyState" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyRe" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "TyDev" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyStateDev" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TyS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TyProd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyList" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TyVec" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TyProxy" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyFin" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TyPlus" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TyNeg" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TyRef" 'PrefixI 'False) (U1 :: Type -> Type))))))

s2tb :: Text -> Maybe TyBuiltin Source #

tb2s :: TyBuiltin -> Text Source #

tybuiltins :: [(Text, TyBuiltin)] Source #

builtinUserQName :: [(Builtin, Text)] Source #

Note: this is not injective (e.g., VecConcat has two notations)

Note: there are Builtins that don't have direct corresponding notations (e.g. Bits is used in lit, but not directly)

builtinUserName :: [(Builtin, Text)] Source #

data RWUserOp Source #

Cases where we need to include specific handling for rewire-user definitions:

We need to print punctuation and infix notations carefully
We may need to differentiate based on type information in some circumstances: a. We can't define a single operator over different monads (or can we?) b. We need to differentiate between vector and word operations
We include Builtins because we handle them at the same junctures

We can handle other cases by writing a function or synonym in the Isabelle ReWire session (rewire-embedder/targets/isabelle/thys)

Instances

Instances details

NFData RWUserOp Source #

Instance details

Defined in Embedder.Builtins

Methods

rnf :: RWUserOp -> () #

Data RWUserOp Source #

Instance details

Defined in Embedder.Builtins

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RWUserOp -> c RWUserOp #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RWUserOp #

toConstr :: RWUserOp -> Constr #

dataTypeOf :: RWUserOp -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c RWUserOp) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RWUserOp) #

gmapT :: (forall b. Data b => b -> b) -> RWUserOp -> RWUserOp #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RWUserOp -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RWUserOp -> r #

gmapQ :: (forall d. Data d => d -> u) -> RWUserOp -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> RWUserOp -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RWUserOp -> m RWUserOp #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RWUserOp -> m RWUserOp #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RWUserOp -> m RWUserOp #

Generic RWUserOp Source #

Instance details

Defined in Embedder.Builtins

Associated Types

type Rep RWUserOp

Instance details

Defined in Embedder.Builtins

type Rep RWUserOp = D1 ('MetaData "RWUserOp" "Embedder.Builtins" "rewire-embedder-2.8-G94ytt72LAgDf9UAeQPb84" 'False) (((((C1 ('MetaCons "RWBuiltin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Builtin)) :+: C1 ('MetaCons "CompDot" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CompDol" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BindI" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BindS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BindR" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BindRInf" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Seq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SeqI" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "SeqS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SeqR" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SeqRInf" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RBindI" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RBindS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RBindR" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RBindRInf" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ReturnI" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ReturnS" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "ReturnR" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LiftS" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LiftR" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WordIndexProxy" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "WordIndexFin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BAnd" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BOr" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BXOr" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FinAdd" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "FinSub" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FinMul" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FinDiv" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FinEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FinLt" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "WordSlice" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WordIndex" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Update" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecLastIndexProxy" 'PrefixI 'False) (U1 :: Type -> Type)))))))

Methods

from :: RWUserOp -> Rep RWUserOp x #

to :: Rep RWUserOp x -> RWUserOp #

Show RWUserOp Source #

Instance details

Defined in Embedder.Builtins

Methods

showsPrec :: Int -> RWUserOp -> ShowS #

show :: RWUserOp -> String #

showList :: [RWUserOp] -> ShowS #

Eq RWUserOp Source #

VecEmpty | VecSingleton | VecCons | VecSnoc | VecHead | VecLastIndex | VecLastIndexProxy | VecTake | VecDrop | VecInit | VecTail | VecZipWith | VecZipWith3 | VecPackLo | VecPackHi | VecUnpackLo | VecUnpackHi Additional notation: FiniteComp: even, odd Bits: zero, one, bit, lit, rotR, rotL, even, odd, Lit=W128

Instance details

Defined in Embedder.Builtins

Methods

(==) :: RWUserOp -> RWUserOp -> Bool #

(/=) :: RWUserOp -> RWUserOp -> Bool #

Ord RWUserOp Source #

Instance details

Defined in Embedder.Builtins

Methods

compare :: RWUserOp -> RWUserOp -> Ordering #

(<) :: RWUserOp -> RWUserOp -> Bool #

(<=) :: RWUserOp -> RWUserOp -> Bool #

(>) :: RWUserOp -> RWUserOp -> Bool #

(>=) :: RWUserOp -> RWUserOp -> Bool #

max :: RWUserOp -> RWUserOp -> RWUserOp #

min :: RWUserOp -> RWUserOp -> RWUserOp #

Hashable RWUserOp Source #

Instance details

Defined in Embedder.Builtins

Methods

hashWithSalt :: Int -> RWUserOp -> Int

hash :: RWUserOp -> Int

TextShow RWUserOp Source #

Instance details

Defined in Embedder.Builtins

Methods

showbPrec :: Int -> RWUserOp -> Builder #

showb :: RWUserOp -> Builder #

showbList :: [RWUserOp] -> Builder

showtPrec :: Int -> RWUserOp -> Text

showt :: RWUserOp -> Text #

showtList :: [RWUserOp] -> Text

showtlPrec :: Int -> RWUserOp -> Text

showtl :: RWUserOp -> Text

showtlList :: [RWUserOp] -> Text

type Rep RWUserOp Source #

Instance details

Defined in Embedder.Builtins

type Rep RWUserOp = D1 ('MetaData "RWUserOp" "Embedder.Builtins" "rewire-embedder-2.8-G94ytt72LAgDf9UAeQPb84" 'False) (((((C1 ('MetaCons "RWBuiltin" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Builtin)) :+: C1 ('MetaCons "CompDot" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CompDol" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BindI" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BindS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BindR" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BindRInf" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Seq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SeqI" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "SeqS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "SeqR" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "SeqRInf" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RBindI" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "RBindS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RBindR" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RBindRInf" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ReturnI" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ReturnS" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "ReturnR" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LiftS" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "LiftR" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WordIndexProxy" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "WordIndexFin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BAnd" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BOr" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BXOr" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FinAdd" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "FinSub" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FinMul" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "FinDiv" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FinEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FinLt" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "WordSlice" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "WordIndex" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NEq" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Update" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "VecLastIndexProxy" 'PrefixI 'False) (U1 :: Type -> Type)))))))

rwu2s :: RWUserOp -> Maybe Text Source #

s2rwu :: Text -> Maybe RWUserOp Source #

rwu2qn :: RWUserOp -> Maybe Text Source #

qn2rwu :: Text -> Maybe RWUserOp Source #