{-# LANGUAGE OverloadedStrings #-}
module Funcons.Core.Values.Primitive.Characters.Characters where
import Funcons.EDSL
import Funcons.Operations hiding (Values)
entities = []
types = typeEnvFromList
[]
funcons = libFromList
[("unicode-point",StrictFuncon stepUnicode_point),("unicode",StrictFuncon stepUnicode_point),("iso-latin-1-points",NullaryFuncon stepIso_latin_1_points),("ascii-points",NullaryFuncon stepAscii_points),("ascii-character",StrictFuncon stepAscii_character),("backspace",NullaryFuncon stepBackspace),("horizontal-tab",NullaryFuncon stepHorizontal_tab),("line-feed",NullaryFuncon stepLine_feed),("form-feed",NullaryFuncon stepForm_feed),("carriage-return",NullaryFuncon stepCarriage_return),("double-quote",NullaryFuncon stepDouble_quote),("single-quote",NullaryFuncon stepSingle_quote),("backslash",NullaryFuncon stepBackslash)]
unicode_point_ fargs = FApp "unicode-point" (fargs)
unicode_ fargs = FApp "unicode-point" (fargs)
stepUnicode_point fargs =
evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [PADT "unicode-character" [VPAnnotated (VPMetaVar "UP") (TName "unicode-points")]] env
rewriteTermTo (TVar "UP") env
iso_latin_1_points_ = FName "iso-latin-1-points"
stepIso_latin_1_points = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TApp "bounded-integers" [TFuncon (FValue (Nat 0)),TApp "unsigned-bit-vector-maximum" [TFuncon (FValue (Nat 8))]]) env
ascii_points_ = FName "ascii-points"
stepAscii_points = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TApp "bounded-integers" [TFuncon (FValue (Nat 0)),TApp "unsigned-bit-vector-maximum" [TFuncon (FValue (Nat 7))]]) env
ascii_character_ fargs = FApp "ascii-character" (fargs)
stepAscii_character fargs =
evalRules [rewrite1,rewrite2,rewrite3] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii 't')]),VPAnnotated (VPMetaVar "C") (TName "ascii-characters")]] env
rewriteTermTo (TVar "C") env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii 't')]),VPAnnotated (VPMetaVar "C") (TName "characters")]] env
env <- sideCondition (SCIsInSort (TVar "C") (TSortComplement (TName "ascii-characters"))) env
rewriteTermTo (TName "none") env
rewrite3 = do
let env = emptyEnv
env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii 't')]),VPAnnotated (VPSeqVar "C*" StarOp) (TSortSeq (TName "characters") StarOp)]] env
env <- sideCondition (SCInequality (TApp "length" [TVar "C*"]) (TFuncon (FValue (Nat 1)))) env
rewriteTermTo (TName "none") env
backspace_ = FName "backspace"
stepBackspace = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii '8')]))]]) env
horizontal_tab_ = FName "horizontal-tab"
stepHorizontal_tab = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii '9')]))]]) env
line_feed_ = FName "line-feed"
stepLine_feed = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii 'a')]))]]) env
form_feed_ = FName "form-feed"
stepForm_feed = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii 'c')]))]]) env
carriage_return_ = FName "carriage-return"
stepCarriage_return = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii 'd')]))]]) env
double_quote_ = FName "double-quote"
stepDouble_quote = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii '2'),FValue (Ascii '2')]))]]) env
single_quote_ = FName "single-quote"
stepSingle_quote = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii '2'),FValue (Ascii '7')]))]]) env
backslash_ = FName "backslash"
stepBackslash = evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Ascii '0'),FValue (Ascii '0'),FValue (Ascii '5'),FValue (Ascii 'c')]))]]) env