{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings#-}

-- | Atoms used by the Crucible CFG concrete syntax.
module Lang.Crucible.Syntax.Atoms
  (
    -- * The atom datatype
    Atomic(..)
  , atom
    -- * Individual atoms
  , AtomName(..)
  , LabelName(..)
  , RegName(..)
  , FunName(..)
  , GlobalName(..)
  , Keyword(..)
  ) where

import Control.Applicative

import Data.Char
import Data.Functor
import Data.Ratio
import Data.Text (Text)
import qualified Data.Text as T

import Lang.Crucible.Syntax.SExpr
import Numeric
import qualified Prettyprinter as PP

import Text.Megaparsec as MP hiding (many, some)
import Text.Megaparsec.Char

-- | The name of an atom (non-keyword identifier)
newtype AtomName = AtomName Text deriving (AtomName -> AtomName -> Bool
(AtomName -> AtomName -> Bool)
-> (AtomName -> AtomName -> Bool) -> Eq AtomName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AtomName -> AtomName -> Bool
== :: AtomName -> AtomName -> Bool
$c/= :: AtomName -> AtomName -> Bool
/= :: AtomName -> AtomName -> Bool
Eq, Eq AtomName
Eq AtomName =>
(AtomName -> AtomName -> Ordering)
-> (AtomName -> AtomName -> Bool)
-> (AtomName -> AtomName -> Bool)
-> (AtomName -> AtomName -> Bool)
-> (AtomName -> AtomName -> Bool)
-> (AtomName -> AtomName -> AtomName)
-> (AtomName -> AtomName -> AtomName)
-> Ord AtomName
AtomName -> AtomName -> Bool
AtomName -> AtomName -> Ordering
AtomName -> AtomName -> AtomName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: AtomName -> AtomName -> Ordering
compare :: AtomName -> AtomName -> Ordering
$c< :: AtomName -> AtomName -> Bool
< :: AtomName -> AtomName -> Bool
$c<= :: AtomName -> AtomName -> Bool
<= :: AtomName -> AtomName -> Bool
$c> :: AtomName -> AtomName -> Bool
> :: AtomName -> AtomName -> Bool
$c>= :: AtomName -> AtomName -> Bool
>= :: AtomName -> AtomName -> Bool
$cmax :: AtomName -> AtomName -> AtomName
max :: AtomName -> AtomName -> AtomName
$cmin :: AtomName -> AtomName -> AtomName
min :: AtomName -> AtomName -> AtomName
Ord, (forall ann. AtomName -> Doc ann)
-> (forall ann. [AtomName] -> Doc ann) -> Pretty AtomName
forall ann. [AtomName] -> Doc ann
forall ann. AtomName -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
$cpretty :: forall ann. AtomName -> Doc ann
pretty :: forall ann. AtomName -> Doc ann
$cprettyList :: forall ann. [AtomName] -> Doc ann
prettyList :: forall ann. [AtomName] -> Doc ann
PP.Pretty, Int -> AtomName -> ShowS
[AtomName] -> ShowS
AtomName -> String
(Int -> AtomName -> ShowS)
-> (AtomName -> String) -> ([AtomName] -> ShowS) -> Show AtomName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AtomName -> ShowS
showsPrec :: Int -> AtomName -> ShowS
$cshow :: AtomName -> String
show :: AtomName -> String
$cshowList :: [AtomName] -> ShowS
showList :: [AtomName] -> ShowS
Show)
-- | The name of a label (identifier followed by colon)
newtype LabelName = LabelName Text deriving (LabelName -> LabelName -> Bool
(LabelName -> LabelName -> Bool)
-> (LabelName -> LabelName -> Bool) -> Eq LabelName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LabelName -> LabelName -> Bool
== :: LabelName -> LabelName -> Bool
$c/= :: LabelName -> LabelName -> Bool
/= :: LabelName -> LabelName -> Bool
Eq, Eq LabelName
Eq LabelName =>
(LabelName -> LabelName -> Ordering)
-> (LabelName -> LabelName -> Bool)
-> (LabelName -> LabelName -> Bool)
-> (LabelName -> LabelName -> Bool)
-> (LabelName -> LabelName -> Bool)
-> (LabelName -> LabelName -> LabelName)
-> (LabelName -> LabelName -> LabelName)
-> Ord LabelName
LabelName -> LabelName -> Bool
LabelName -> LabelName -> Ordering
LabelName -> LabelName -> LabelName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LabelName -> LabelName -> Ordering
compare :: LabelName -> LabelName -> Ordering
$c< :: LabelName -> LabelName -> Bool
< :: LabelName -> LabelName -> Bool
$c<= :: LabelName -> LabelName -> Bool
<= :: LabelName -> LabelName -> Bool
$c> :: LabelName -> LabelName -> Bool
> :: LabelName -> LabelName -> Bool
$c>= :: LabelName -> LabelName -> Bool
>= :: LabelName -> LabelName -> Bool
$cmax :: LabelName -> LabelName -> LabelName
max :: LabelName -> LabelName -> LabelName
$cmin :: LabelName -> LabelName -> LabelName
min :: LabelName -> LabelName -> LabelName
Ord, (forall ann. LabelName -> Doc ann)
-> (forall ann. [LabelName] -> Doc ann) -> Pretty LabelName
forall ann. [LabelName] -> Doc ann
forall ann. LabelName -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
$cpretty :: forall ann. LabelName -> Doc ann
pretty :: forall ann. LabelName -> Doc ann
$cprettyList :: forall ann. [LabelName] -> Doc ann
prettyList :: forall ann. [LabelName] -> Doc ann
PP.Pretty, Int -> LabelName -> ShowS
[LabelName] -> ShowS
LabelName -> String
(Int -> LabelName -> ShowS)
-> (LabelName -> String)
-> ([LabelName] -> ShowS)
-> Show LabelName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LabelName -> ShowS
showsPrec :: Int -> LabelName -> ShowS
$cshow :: LabelName -> String
show :: LabelName -> String
$cshowList :: [LabelName] -> ShowS
showList :: [LabelName] -> ShowS
Show)
-- | The name of a register (dollar sign followed by identifier)
newtype RegName = RegName Text deriving (RegName -> RegName -> Bool
(RegName -> RegName -> Bool)
-> (RegName -> RegName -> Bool) -> Eq RegName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RegName -> RegName -> Bool
== :: RegName -> RegName -> Bool
$c/= :: RegName -> RegName -> Bool
/= :: RegName -> RegName -> Bool
Eq, Eq RegName
Eq RegName =>
(RegName -> RegName -> Ordering)
-> (RegName -> RegName -> Bool)
-> (RegName -> RegName -> Bool)
-> (RegName -> RegName -> Bool)
-> (RegName -> RegName -> Bool)
-> (RegName -> RegName -> RegName)
-> (RegName -> RegName -> RegName)
-> Ord RegName
RegName -> RegName -> Bool
RegName -> RegName -> Ordering
RegName -> RegName -> RegName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: RegName -> RegName -> Ordering
compare :: RegName -> RegName -> Ordering
$c< :: RegName -> RegName -> Bool
< :: RegName -> RegName -> Bool
$c<= :: RegName -> RegName -> Bool
<= :: RegName -> RegName -> Bool
$c> :: RegName -> RegName -> Bool
> :: RegName -> RegName -> Bool
$c>= :: RegName -> RegName -> Bool
>= :: RegName -> RegName -> Bool
$cmax :: RegName -> RegName -> RegName
max :: RegName -> RegName -> RegName
$cmin :: RegName -> RegName -> RegName
min :: RegName -> RegName -> RegName
Ord, (forall ann. RegName -> Doc ann)
-> (forall ann. [RegName] -> Doc ann) -> Pretty RegName
forall ann. [RegName] -> Doc ann
forall ann. RegName -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
$cpretty :: forall ann. RegName -> Doc ann
pretty :: forall ann. RegName -> Doc ann
$cprettyList :: forall ann. [RegName] -> Doc ann
prettyList :: forall ann. [RegName] -> Doc ann
PP.Pretty, Int -> RegName -> ShowS
[RegName] -> ShowS
RegName -> String
(Int -> RegName -> ShowS)
-> (RegName -> String) -> ([RegName] -> ShowS) -> Show RegName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RegName -> ShowS
showsPrec :: Int -> RegName -> ShowS
$cshow :: RegName -> String
show :: RegName -> String
$cshowList :: [RegName] -> ShowS
showList :: [RegName] -> ShowS
Show)
-- | The name of a function (at-sign followed by identifier)
newtype FunName = FunName Text deriving (FunName -> FunName -> Bool
(FunName -> FunName -> Bool)
-> (FunName -> FunName -> Bool) -> Eq FunName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FunName -> FunName -> Bool
== :: FunName -> FunName -> Bool
$c/= :: FunName -> FunName -> Bool
/= :: FunName -> FunName -> Bool
Eq, Eq FunName
Eq FunName =>
(FunName -> FunName -> Ordering)
-> (FunName -> FunName -> Bool)
-> (FunName -> FunName -> Bool)
-> (FunName -> FunName -> Bool)
-> (FunName -> FunName -> Bool)
-> (FunName -> FunName -> FunName)
-> (FunName -> FunName -> FunName)
-> Ord FunName
FunName -> FunName -> Bool
FunName -> FunName -> Ordering
FunName -> FunName -> FunName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FunName -> FunName -> Ordering
compare :: FunName -> FunName -> Ordering
$c< :: FunName -> FunName -> Bool
< :: FunName -> FunName -> Bool
$c<= :: FunName -> FunName -> Bool
<= :: FunName -> FunName -> Bool
$c> :: FunName -> FunName -> Bool
> :: FunName -> FunName -> Bool
$c>= :: FunName -> FunName -> Bool
>= :: FunName -> FunName -> Bool
$cmax :: FunName -> FunName -> FunName
max :: FunName -> FunName -> FunName
$cmin :: FunName -> FunName -> FunName
min :: FunName -> FunName -> FunName
Ord, (forall ann. FunName -> Doc ann)
-> (forall ann. [FunName] -> Doc ann) -> Pretty FunName
forall ann. [FunName] -> Doc ann
forall ann. FunName -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
$cpretty :: forall ann. FunName -> Doc ann
pretty :: forall ann. FunName -> Doc ann
$cprettyList :: forall ann. [FunName] -> Doc ann
prettyList :: forall ann. [FunName] -> Doc ann
PP.Pretty, Int -> FunName -> ShowS
[FunName] -> ShowS
FunName -> String
(Int -> FunName -> ShowS)
-> (FunName -> String) -> ([FunName] -> ShowS) -> Show FunName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FunName -> ShowS
showsPrec :: Int -> FunName -> ShowS
$cshow :: FunName -> String
show :: FunName -> String
$cshowList :: [FunName] -> ShowS
showList :: [FunName] -> ShowS
Show)
-- | The name of a global variable (two dollar signs followed by identifier)
newtype GlobalName = GlobalName Text deriving (GlobalName -> GlobalName -> Bool
(GlobalName -> GlobalName -> Bool)
-> (GlobalName -> GlobalName -> Bool) -> Eq GlobalName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GlobalName -> GlobalName -> Bool
== :: GlobalName -> GlobalName -> Bool
$c/= :: GlobalName -> GlobalName -> Bool
/= :: GlobalName -> GlobalName -> Bool
Eq, Eq GlobalName
Eq GlobalName =>
(GlobalName -> GlobalName -> Ordering)
-> (GlobalName -> GlobalName -> Bool)
-> (GlobalName -> GlobalName -> Bool)
-> (GlobalName -> GlobalName -> Bool)
-> (GlobalName -> GlobalName -> Bool)
-> (GlobalName -> GlobalName -> GlobalName)
-> (GlobalName -> GlobalName -> GlobalName)
-> Ord GlobalName
GlobalName -> GlobalName -> Bool
GlobalName -> GlobalName -> Ordering
GlobalName -> GlobalName -> GlobalName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: GlobalName -> GlobalName -> Ordering
compare :: GlobalName -> GlobalName -> Ordering
$c< :: GlobalName -> GlobalName -> Bool
< :: GlobalName -> GlobalName -> Bool
$c<= :: GlobalName -> GlobalName -> Bool
<= :: GlobalName -> GlobalName -> Bool
$c> :: GlobalName -> GlobalName -> Bool
> :: GlobalName -> GlobalName -> Bool
$c>= :: GlobalName -> GlobalName -> Bool
>= :: GlobalName -> GlobalName -> Bool
$cmax :: GlobalName -> GlobalName -> GlobalName
max :: GlobalName -> GlobalName -> GlobalName
$cmin :: GlobalName -> GlobalName -> GlobalName
min :: GlobalName -> GlobalName -> GlobalName
Ord, (forall ann. GlobalName -> Doc ann)
-> (forall ann. [GlobalName] -> Doc ann) -> Pretty GlobalName
forall ann. [GlobalName] -> Doc ann
forall ann. GlobalName -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. [a] -> Doc ann) -> Pretty a
$cpretty :: forall ann. GlobalName -> Doc ann
pretty :: forall ann. GlobalName -> Doc ann
$cprettyList :: forall ann. [GlobalName] -> Doc ann
prettyList :: forall ann. [GlobalName] -> Doc ann
PP.Pretty, Int -> GlobalName -> ShowS
[GlobalName] -> ShowS
GlobalName -> String
(Int -> GlobalName -> ShowS)
-> (GlobalName -> String)
-> ([GlobalName] -> ShowS)
-> Show GlobalName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GlobalName -> ShowS
showsPrec :: Int -> GlobalName -> ShowS
$cshow :: GlobalName -> String
show :: GlobalName -> String
$cshowList :: [GlobalName] -> ShowS
showList :: [GlobalName] -> ShowS
Show)

-- | Individual language keywords (reserved identifiers)
data Keyword = Defun | DefBlock | DefGlobal | Declare | Extern
             | Registers
             | Start
             | SetGlobal
             | SetRef | DropRef_
             | Plus | Minus | Times | Div | Negate | Abs
             | Just_ | Nothing_ | FromJust
             | Inj | Proj
             | AnyT | UnitT | BoolT | NatT | IntegerT | RealT | ComplexRealT | CharT | StringT
             | BitvectorT | VectorT | SequenceT | FPT | FunT | MaybeT | VariantT | StructT | RefT
             | Half_ | Float_ | Double_ | Quad_ | X86_80_ | DoubleDouble_
             | Unicode_ | Char8_ | Char16_
             | The
             | Equalp | Integerp
             | If
             | Not_ | And_ | Or_ | Xor_
             | Mod
             | Lt | Le
             | Show
             | StringConcat_ | StringEmpty_ | StringLength_
             | ToAny | FromAny
             | VectorLit_ | VectorReplicate_ | VectorIsEmpty_ | VectorSize_
             | VectorGetEntry_ | VectorSetEntry_ | VectorCons_
             | MkStruct_ | GetField_ | SetField_
             | SequenceNil_ | SequenceCons_ | SequenceAppend_
             | SequenceIsNil_ | SequenceLength_
             | SequenceHead_ | SequenceTail_ | SequenceUncons_
             | Deref | Ref | EmptyRef
             | Jump_ | Return_ | Branch_ | MaybeBranch_ | TailCall_ | Error_ | Output_ | Case
             | Print_ | PrintLn_
             | Let | Fresh
             | Assert_ | Assume_
             | SetRegister
             | Funcall
             | Breakpoint_
             | BV | BVConcat_ | BVSelect_ | BVTrunc_
             | BVZext_ | BVSext_ | BVNonzero_ | BoolToBV_
             | BVCarry_ | BVSCarry_ | BVSBorrow_
             | BVNot_ | BVAnd_ | BVOr_ | BVXor_ | BVShl_ | BVLshr_ | BVAshr_
             | Sle | Slt | Sdiv | Smod | ZeroExt | SignExt
             | RNE_ | RNA_ | RTP_ | RTN_ | RTZ_
             | FPToUBV_ | FPToSBV_ | UBVToFP_ | SBVToFP_ | BinaryToFP_ | FPToBinary_
             | FPToReal_ | RealToFP_
  deriving (Keyword -> Keyword -> Bool
(Keyword -> Keyword -> Bool)
-> (Keyword -> Keyword -> Bool) -> Eq Keyword
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Keyword -> Keyword -> Bool
== :: Keyword -> Keyword -> Bool
$c/= :: Keyword -> Keyword -> Bool
/= :: Keyword -> Keyword -> Bool
Eq, Eq Keyword
Eq Keyword =>
(Keyword -> Keyword -> Ordering)
-> (Keyword -> Keyword -> Bool)
-> (Keyword -> Keyword -> Bool)
-> (Keyword -> Keyword -> Bool)
-> (Keyword -> Keyword -> Bool)
-> (Keyword -> Keyword -> Keyword)
-> (Keyword -> Keyword -> Keyword)
-> Ord Keyword
Keyword -> Keyword -> Bool
Keyword -> Keyword -> Ordering
Keyword -> Keyword -> Keyword
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Keyword -> Keyword -> Ordering
compare :: Keyword -> Keyword -> Ordering
$c< :: Keyword -> Keyword -> Bool
< :: Keyword -> Keyword -> Bool
$c<= :: Keyword -> Keyword -> Bool
<= :: Keyword -> Keyword -> Bool
$c> :: Keyword -> Keyword -> Bool
> :: Keyword -> Keyword -> Bool
$c>= :: Keyword -> Keyword -> Bool
>= :: Keyword -> Keyword -> Bool
$cmax :: Keyword -> Keyword -> Keyword
max :: Keyword -> Keyword -> Keyword
$cmin :: Keyword -> Keyword -> Keyword
min :: Keyword -> Keyword -> Keyword
Ord)

keywords :: [(Text, Keyword)]
keywords :: [(Text, Keyword)]
keywords =
    -- function/block defintion
  [ (Text
"defun" , Keyword
Defun)
  , (Text
"start" , Keyword
Start)
  , (Text
"defblock", Keyword
DefBlock)
  , (Text
"defglobal", Keyword
DefGlobal)
  , (Text
"declare", Keyword
Declare)
  , (Text
"extern", Keyword
Extern)
  , (Text
"registers", Keyword
Registers)

    -- statements
  , (Text
"let", Keyword
Let)
  , (Text
"set-global!", Keyword
SetGlobal)
  , (Text
"set-ref!", Keyword
SetRef)
  , (Text
"drop-ref!", Keyword
DropRef_)
  , (Text
"fresh", Keyword
Fresh)
  , (Text
"jump" , Keyword
Jump_)
  , (Text
"case", Keyword
Case)
  , (Text
"return" , Keyword
Return_)
  , (Text
"branch" , Keyword
Branch_)
  , (Text
"maybe-branch" , Keyword
MaybeBranch_)
  , (Text
"tail-call" , Keyword
TailCall_)
  , (Text
"error", Keyword
Error_)
  , (Text
"output", Keyword
Output_)
  , (Text
"print" , Keyword
Print_)
  , (Text
"println" , Keyword
PrintLn_)
  , (Text
"Ref", Keyword
RefT)
  , (Text
"deref", Keyword
Deref)
  , (Text
"ref", Keyword
Ref)
  , (Text
"empty-ref", Keyword
EmptyRef)
  , (Text
"set-register!", Keyword
SetRegister)
  , (Text
"assert!", Keyword
Assert_)
  , (Text
"assume!", Keyword
Assume_)
  , (Text
"funcall", Keyword
Funcall)
  , (Text
"breakpoint", Keyword
Breakpoint_)

    -- types
  , (Text
"Any" , Keyword
AnyT)
  , (Text
"Unit" , Keyword
UnitT)
  , (Text
"Bool" , Keyword
BoolT)
  , (Text
"Nat" , Keyword
NatT)
  , (Text
"Integer" , Keyword
IntegerT)
  , (Text
"FP", Keyword
FPT)
  , (Text
"Real" , Keyword
RealT)
  , (Text
"ComplexReal" , Keyword
ComplexRealT)
  , (Text
"Char" , Keyword
CharT)
  , (Text
"String" , Keyword
StringT)
  , (Text
"Bitvector" , Keyword
BitvectorT)
  , (Text
"Vector", Keyword
VectorT)
  , (Text
"Sequence", Keyword
SequenceT)
  , (Text
"->", Keyword
FunT)
  , (Text
"Maybe", Keyword
MaybeT)
  , (Text
"Variant", Keyword
VariantT)
  , (Text
"Struct", Keyword
StructT)

    -- string sorts
  , (Text
"Unicode", Keyword
Unicode_)
  , (Text
"Char16", Keyword
Char16_)
  , (Text
"Char8", Keyword
Char8_)

    -- floating-point variants
  , (Text
"Half", Keyword
Half_)
  , (Text
"Float", Keyword
Float_)
  , (Text
"Double", Keyword
Double_)
  , (Text
"Quad", Keyword
Quad_)
  , (Text
"X86_80", Keyword
X86_80_)
  , (Text
"DoubleDouble", Keyword
DoubleDouble_)

    -- misc
  , (Text
"the" , Keyword
The)
  , (Text
"equal?" , Keyword
Equalp)
  , (Text
"if" , Keyword
If)

    -- ANY types
  , (Text
"to-any", Keyword
ToAny)
  , (Text
"from-any", Keyword
FromAny)

    -- booleans
  , (Text
"not" , Keyword
Not_)
  , (Text
"and" , Keyword
And_)
  , (Text
"or" , Keyword
Or_)
  , (Text
"xor" , Keyword
Xor_)

    -- arithmetic
  , (Text
"+" , Keyword
Plus)
  , (Text
"-" , Keyword
Minus)
  , (Text
"*" , Keyword
Times)
  , (Text
"/" , Keyword
Div)
  , (Text
"<" , Keyword
Lt)
  , (Text
"<=" , Keyword
Le)
  , (Text
"<=$" , Keyword
Sle)
  , (Text
"<$" , Keyword
Slt)
  , (Text
"/$" , Keyword
Sdiv)
  , (Text
"smod", Keyword
Smod)
  , (Text
"negate", Keyword
Negate)
  , (Text
"abs", Keyword
Abs)
  , (Text
"mod" , Keyword
Mod)
  , (Text
"integer?" , Keyword
Integerp)

    -- Variants
  , (Text
"inj", Keyword
Inj)
  , (Text
"proj", Keyword
Proj)

    -- Structs
  , (Text
"struct", Keyword
MkStruct_)
  , (Text
"get-field", Keyword
GetField_)
  , (Text
"set-field", Keyword
SetField_)

    -- Maybe
  , (Text
"just" , Keyword
Just_)
  , (Text
"nothing" , Keyword
Nothing_)
  , (Text
"from-just" , Keyword
FromJust)

    -- Vectors
  , (Text
"vector", Keyword
VectorLit_)
  , (Text
"vector-replicate", Keyword
VectorReplicate_)
  , (Text
"vector-empty?", Keyword
VectorIsEmpty_)
  , (Text
"vector-size", Keyword
VectorSize_)
  , (Text
"vector-get", Keyword
VectorGetEntry_)
  , (Text
"vector-set", Keyword
VectorSetEntry_)
  , (Text
"vector-cons", Keyword
VectorCons_)

    -- Sequences
  , (Text
"seq-nil", Keyword
SequenceNil_)
  , (Text
"seq-cons", Keyword
SequenceCons_)
  , (Text
"seq-append", Keyword
SequenceAppend_)
  , (Text
"seq-nil?", Keyword
SequenceIsNil_)
  , (Text
"seq-length", Keyword
SequenceLength_)
  , (Text
"seq-head", Keyword
SequenceHead_)
  , (Text
"seq-tail", Keyword
SequenceTail_)
  , (Text
"seq-uncons", Keyword
SequenceUncons_)

    -- strings
  , (Text
"show", Keyword
Show)
  , (Text
"string-concat", Keyword
StringConcat_)
  , (Text
"string-empty", Keyword
StringEmpty_)
  , (Text
"string-length", Keyword
StringLength_)

    -- bitvector
  , (Text
"bv", Keyword
BV)
  , (Text
"bv-concat", Keyword
BVConcat_)
  , (Text
"bv-select", Keyword
BVSelect_)
  , (Text
"bv-trunc", Keyword
BVTrunc_)
  , (Text
"zero-extend", Keyword
BVZext_)
  , (Text
"sign-extend", Keyword
BVSext_)
  , (Text
"bv-nonzero", Keyword
BVNonzero_)
  , (Text
"bool-to-bv", Keyword
BoolToBV_)
  , (Text
"bv-carry", Keyword
BVCarry_)
  , (Text
"bv-scarry", Keyword
BVSCarry_)
  , (Text
"bv-sborrow", Keyword
BVSBorrow_)
  , (Text
"bv-not", Keyword
BVNot_)
  , (Text
"bv-and", Keyword
BVAnd_)
  , (Text
"bv-or", Keyword
BVOr_)
  , (Text
"bv-xor", Keyword
BVXor_)
  , (Text
"shl", Keyword
BVShl_)
  , (Text
"lshr", Keyword
BVLshr_)
  , (Text
"ashr", Keyword
BVAshr_)

    -- floating-point
  , (Text
"fp-to-ubv", Keyword
FPToUBV_)
  , (Text
"fp-to-sbv", Keyword
FPToSBV_)
  , (Text
"ubv-to-fp", Keyword
UBVToFP_)
  , (Text
"sbv-to-fp", Keyword
SBVToFP_)
  , (Text
"fp-to-binary", Keyword
FPToBinary_)
  , (Text
"binary-to-fp", Keyword
BinaryToFP_)
  , (Text
"real-to-fp", Keyword
RealToFP_)
  , (Text
"fp-to-real", Keyword
FPToReal_)
  , (Text
"rne" , Keyword
RNE_)
  , (Text
"rna" , Keyword
RNA_)
  , (Text
"rtp" , Keyword
RTP_)
  , (Text
"rtn" , Keyword
RTN_)
  , (Text
"rtz" , Keyword
RTZ_)
  ]

instance Show Keyword where
  show :: Keyword -> String
show Keyword
k = case [Text
str | (Text
str, Keyword
k') <- [(Text, Keyword)]
keywords, Keyword
k Keyword -> Keyword -> Bool
forall a. Eq a => a -> a -> Bool
== Keyword
k'] of
             [] -> String
"UNKNOWN KW"
             (Text
s:[Text]
_) -> Text -> String
T.unpack Text
s


-- | The atoms of the language
data Atomic = Kw !Keyword -- ^ Keywords are all the built-in operators and expression formers
            | Lbl !LabelName -- ^ Labels, but not the trailing colon
            | At !AtomName -- ^ Atom names (which look like Scheme symbols)
            | Rg !RegName -- ^ Registers, whose names have a leading single $
            | Gl !GlobalName -- ^ Global variables, whose names have a leading double $$
            | Fn !FunName -- ^ Function names, minus the leading @
            | Int !Integer -- ^ Literal integers
            | Rat !Rational -- ^ Literal rational numbers
            | Bool !Bool   -- ^ Literal Booleans
            | StrLit !Text -- ^ Literal strings
  deriving (Atomic -> Atomic -> Bool
(Atomic -> Atomic -> Bool)
-> (Atomic -> Atomic -> Bool) -> Eq Atomic
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Atomic -> Atomic -> Bool
== :: Atomic -> Atomic -> Bool
$c/= :: Atomic -> Atomic -> Bool
/= :: Atomic -> Atomic -> Bool
Eq, Eq Atomic
Eq Atomic =>
(Atomic -> Atomic -> Ordering)
-> (Atomic -> Atomic -> Bool)
-> (Atomic -> Atomic -> Bool)
-> (Atomic -> Atomic -> Bool)
-> (Atomic -> Atomic -> Bool)
-> (Atomic -> Atomic -> Atomic)
-> (Atomic -> Atomic -> Atomic)
-> Ord Atomic
Atomic -> Atomic -> Bool
Atomic -> Atomic -> Ordering
Atomic -> Atomic -> Atomic
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Atomic -> Atomic -> Ordering
compare :: Atomic -> Atomic -> Ordering
$c< :: Atomic -> Atomic -> Bool
< :: Atomic -> Atomic -> Bool
$c<= :: Atomic -> Atomic -> Bool
<= :: Atomic -> Atomic -> Bool
$c> :: Atomic -> Atomic -> Bool
> :: Atomic -> Atomic -> Bool
$c>= :: Atomic -> Atomic -> Bool
>= :: Atomic -> Atomic -> Bool
$cmax :: Atomic -> Atomic -> Atomic
max :: Atomic -> Atomic -> Atomic
$cmin :: Atomic -> Atomic -> Atomic
min :: Atomic -> Atomic -> Atomic
Ord, Int -> Atomic -> ShowS
[Atomic] -> ShowS
Atomic -> String
(Int -> Atomic -> ShowS)
-> (Atomic -> String) -> ([Atomic] -> ShowS) -> Show Atomic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Atomic -> ShowS
showsPrec :: Int -> Atomic -> ShowS
$cshow :: Atomic -> String
show :: Atomic -> String
$cshowList :: [Atomic] -> ShowS
showList :: [Atomic] -> ShowS
Show)


instance IsAtom Atomic where
  showAtom :: Atomic -> Text
showAtom (Kw Keyword
s) = String -> Text
T.pack (Keyword -> String
forall a. Show a => a -> String
show Keyword
s)
  showAtom (Lbl (LabelName Text
l)) = Text
l Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
":"
  showAtom (Rg (RegName Text
r)) = Text
"$" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
r
  showAtom (Gl (GlobalName Text
r)) = Text
"$$" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
r
  showAtom (At (AtomName Text
a)) = Text
a
  showAtom (Fn (FunName Text
a)) = Text
"@" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
a
  showAtom (Int Integer
i) = String -> Text
T.pack (Integer -> String
forall a. Show a => a -> String
show Integer
i)
  showAtom (Rat Rational
r) = String -> Text
T.pack (Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"/" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r))
  showAtom (Bool Bool
b) = if Bool
b then Text
"#t" else Text
"#f"
  showAtom (StrLit Text
s) = String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Text -> String
forall a. Show a => a -> String
show Text
s

-- | Parse an atom
atom :: Parser Atomic
atom :: Parser Atomic
atom =  Parser Atomic -> Parser Atomic
forall a.
ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (LabelName -> Atomic
Lbl (LabelName -> Atomic) -> (Text -> LabelName) -> Text -> Atomic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> LabelName
LabelName (Text -> Atomic)
-> ParsecT Void Text Identity Text -> Parser Atomic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Text
identifier Parser Atomic -> ParsecT Void Text Identity Char -> Parser Atomic
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
':')
    Parser Atomic -> Parser Atomic -> Parser Atomic
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FunName -> Atomic
Fn (FunName -> Atomic) -> (Text -> FunName) -> Text -> Atomic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FunName
FunName (Text -> Atomic)
-> ParsecT Void Text Identity Text -> Parser Atomic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'@' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity Text
identifier)
    Parser Atomic -> Parser Atomic -> Parser Atomic
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'$' ParsecT Void Text Identity Char -> Parser Atomic -> Parser Atomic
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ((Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'$' ParsecT Void Text Identity Char -> Parser Atomic -> Parser Atomic
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (GlobalName -> Atomic
Gl (GlobalName -> Atomic) -> (Text -> GlobalName) -> Text -> Atomic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> GlobalName
GlobalName (Text -> Atomic)
-> ParsecT Void Text Identity Text -> Parser Atomic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Text
identifier)) Parser Atomic -> Parser Atomic -> Parser Atomic
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> RegName -> Atomic
Rg (RegName -> Atomic) -> (Text -> RegName) -> Text -> Atomic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> RegName
RegName (Text -> Atomic)
-> ParsecT Void Text Identity Text -> Parser Atomic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Text
identifier))
    Parser Atomic -> Parser Atomic -> Parser Atomic
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Atomic -> Parser Atomic
forall a.
ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Integer -> Maybe Integer -> Atomic
mkNum (Integer -> Maybe Integer -> Atomic)
-> ParsecT Void Text Identity Integer
-> ParsecT Void Text Identity (Maybe Integer -> Atomic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Integer
forall a. (Eq a, Num a) => Parser a
signedPrefixedNumber ParsecT Void Text Identity (Maybe Integer -> Atomic)
-> ParsecT Void Text Identity (Maybe Integer) -> Parser Atomic
forall a b.
ParsecT Void Text Identity (a -> b)
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer)
-> ParsecT Void Text Identity Integer
-> ParsecT Void Text Identity (Maybe Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Void Text Identity Char -> ParsecT Void Text Identity Char
forall a.
ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'/') ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Integer
-> ParsecT Void Text Identity Integer
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity Integer
forall a. (Eq a, Num a) => Parser a
prefixedNumber)) ParsecT Void Text Identity (Maybe Integer)
-> ParsecT Void Text Identity (Maybe Integer)
-> ParsecT Void Text Identity (Maybe Integer)
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Integer -> ParsecT Void Text Identity (Maybe Integer)
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Integer
forall a. Maybe a
Nothing))
    Parser Atomic -> Parser Atomic -> Parser Atomic
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Atomic
kwOrAtom
    Parser Atomic -> Parser Atomic -> Parser Atomic
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'#' ParsecT Void Text Identity Char -> Parser Atomic -> Parser Atomic
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>  ((Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
't' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'T') ParsecT Void Text Identity Char -> Atomic -> Parser Atomic
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Bool -> Atomic
Bool Bool
True Parser Atomic -> Parser Atomic -> Parser Atomic
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'f' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'F') ParsecT Void Text Identity Char -> Atomic -> Parser Atomic
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Bool -> Atomic
Bool Bool
False)
    Parser Atomic -> Parser Atomic -> Parser Atomic
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'"' ParsecT Void Text Identity Char -> Parser Atomic -> Parser Atomic
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> Atomic
StrLit (Text -> Atomic) -> (String -> Text) -> String -> Atomic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack (String -> Atomic)
-> ParsecT Void Text Identity String -> Parser Atomic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity String
stringContents)
  where
    mkNum :: Integer -> Maybe Integer -> Atomic
mkNum Integer
x Maybe Integer
Nothing = Integer -> Atomic
Int Integer
x
    mkNum Integer
x (Just Integer
y) = Rational -> Atomic
Rat (Integer
x Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
y)

stringContents :: Parser [Char]
stringContents :: ParsecT Void Text Identity String
stringContents =  (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'\\' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ((:) (Char -> ShowS)
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity ShowS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Char
escapeChar ParsecT Void Text Identity ShowS
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
forall a b.
ParsecT Void Text Identity (a -> b)
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Void Text Identity String
stringContents))
              ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'"' ParsecT Void Text Identity Char
-> String -> ParsecT Void Text Identity String
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> [])
              ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((:) (Char -> ShowS)
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity ShowS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Token Text -> Bool) -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy (Bool -> Char -> Bool
forall a b. a -> b -> a
const Bool
True) ParsecT Void Text Identity ShowS
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
forall a b.
ParsecT Void Text Identity (a -> b)
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Void Text Identity String
stringContents)

escapeChar :: Parser Char
escapeChar :: ParsecT Void Text Identity Char
escapeChar =  (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'\\' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ParsecT Void Text Identity Char
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Char
'\\')
          ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'"' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ParsecT Void Text Identity Char
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Char
'"')
          ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'n' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ParsecT Void Text Identity Char
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Char
'\n')
          ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
't' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Char
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ParsecT Void Text Identity Char
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Char
'\t')
          ParsecT Void Text Identity Char
-> String -> ParsecT Void Text Identity Char
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"valid escape character"

kwOrAtom :: Parser Atomic
kwOrAtom :: Parser Atomic
kwOrAtom = do Text
x <- ParsecT Void Text Identity Text
identifier
              Atomic -> Parser Atomic
forall a. a -> ParsecT Void Text Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Atomic -> Parser Atomic) -> Atomic -> Parser Atomic
forall a b. (a -> b) -> a -> b
$ Atomic -> (Keyword -> Atomic) -> Maybe Keyword -> Atomic
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (AtomName -> Atomic
At (Text -> AtomName
AtomName Text
x)) Keyword -> Atomic
Kw (Text -> [(Text, Keyword)] -> Maybe Keyword
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Text
x [(Text, Keyword)]
keywords)


signedPrefixedNumber :: (Eq a, Num a) => Parser a
signedPrefixedNumber :: forall a. (Eq a, Num a) => Parser a
signedPrefixedNumber =
  Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'+' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity a
forall a. (Eq a, Num a) => Parser a
prefixedNumber ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'-' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (a -> a
forall a. Num a => a -> a
negate (a -> a)
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity a
forall a. (Eq a, Num a) => Parser a
prefixedNumber) ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  ParsecT Void Text Identity a
forall a. (Eq a, Num a) => Parser a
prefixedNumber

prefixedNumber :: (Eq a, Num a) => Parser a
prefixedNumber :: forall a. (Eq a, Num a) => Parser a
prefixedNumber = ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall a.
ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'0' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity a
maybehex) ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT Void Text Identity a
decimal
  where decimal :: ParsecT Void Text Identity a
decimal = Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> (String -> Integer) -> String -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Integer
forall a. Read a => String -> a
read (String -> a)
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity String
forall a.
ParsecT Void Text Identity a -> ParsecT Void Text Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some ((Token Text -> Bool) -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy Char -> Bool
Token Text -> Bool
isDigit ParsecT Void Text Identity Char
-> String -> ParsecT Void Text Identity Char
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"decimal digit")
        maybehex :: ParsecT Void Text Identity a
maybehex = Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'x' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity a
hex ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> a -> ParsecT Void Text Identity a
forall a. a -> ParsecT Void Text Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return a
0
        hex :: ParsecT Void Text Identity a
hex = ParsecT Void Text Identity [(a, String)]
-> ParsecT Void Text Identity a
forall {m :: * -> *} {a} {b}.
(Monad m, Eq a, IsString a, Alternative m) =>
m [(b, a)] -> m b
reading (ParsecT Void Text Identity [(a, String)]
 -> ParsecT Void Text Identity a)
-> ParsecT Void Text Identity [(a, String)]
-> ParsecT Void Text Identity a
forall a b. (a -> b) -> a -> b
$ ReadS a
forall a. (Eq a, Num a) => ReadS a
readHex ReadS a
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity [(a, String)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity String
forall a.
ParsecT Void Text Identity a -> ParsecT Void Text Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some ((Token Text -> Bool) -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy (\Token Text
c -> Char -> Bool
isDigit Char
Token Text
c Bool -> Bool -> Bool
|| Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
Token Text
c (String
"abcdefABCDEF" :: String)) ParsecT Void Text Identity Char
-> String -> ParsecT Void Text Identity Char
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"hex digit")
        reading :: m [(b, a)] -> m b
reading m [(b, a)]
p =
          m [(b, a)]
p m [(b, a)] -> ([(b, a)] -> m b) -> m b
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
            \case
              [(b
x, a
"")] -> b -> m b
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
x
              [(b, a)]
_ -> m b
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
empty