diff --git a/cbs/Funcons/Core/Computations/Abnormal/Breaking/Breaking.hs b/cbs/Funcons/Core/Computations/Abnormal/Breaking/Breaking.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Breaking/Breaking.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Breaking/Breaking.hs @@ -18,7 +18,7 @@ stepBroken = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'b'),FValue (Char 'r'),FValue (Char 'o'),FValue (Char 'k'),FValue (Char 'e'),FValue (Char 'n')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 98)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 107)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 110)])]))]) env finalise_breaking_ fargs = FApp "finalise-breaking" (fargs) stepFinalise_breaking fargs = diff --git a/cbs/Funcons/Core/Computations/Abnormal/Continuing/Continuing.hs b/cbs/Funcons/Core/Computations/Abnormal/Continuing/Continuing.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Continuing/Continuing.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Continuing/Continuing.hs @@ -18,7 +18,7 @@ stepContinued = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'c'),FValue (Char 'o'),FValue (Char 'n'),FValue (Char 't'),FValue (Char 'i'),FValue (Char 'n'),FValue (Char 'u'),FValue (Char 'e'),FValue (Char 'd')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 100)])]))]) env finalise_continuing_ fargs = FApp "finalise-continuing" (fargs) stepFinalise_continuing fargs = diff --git a/cbs/Funcons/Core/Computations/Abnormal/Controlling/Controlling.hs b/cbs/Funcons/Core/Computations/Abnormal/Controlling/Controlling.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Controlling/Controlling.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Controlling/Controlling.hs @@ -21,7 +21,7 @@ let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'c'),FValue (Char 'o'),FValue (Char 'n'),FValue (Char 't'),FValue (Char 'i'),FValue (Char 'n'),FValue (Char 'u'),FValue (Char 'a'),FValue (Char 't'),FValue (Char 'i'),FValue (Char 'o'),FValue (Char 'n')])),TVar "_X1"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 110)])])),TVar "_X1"]) env hole_ = FName "hole" stepHole = evalRules [] [step1] diff --git a/cbs/Funcons/Core/Computations/Abnormal/Failing/Failing.hs b/cbs/Funcons/Core/Computations/Abnormal/Failing/Failing.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Failing/Failing.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Failing/Failing.hs @@ -18,7 +18,7 @@ stepFailed = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'f'),FValue (Char 'a'),FValue (Char 'i'),FValue (Char 'l'),FValue (Char 'e'),FValue (Char 'd')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 102)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 100)])]))]) env finalise_failing_ fargs = FApp "finalise-failing" (fargs) stepFinalise_failing fargs = diff --git a/cbs/Funcons/Core/Computations/Abnormal/Returning/Returning.hs b/cbs/Funcons/Core/Computations/Abnormal/Returning/Returning.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Returning/Returning.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Returning/Returning.hs @@ -21,7 +21,7 @@ let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'r'),FValue (Char 'e'),FValue (Char 't'),FValue (Char 'u'),FValue (Char 'r'),FValue (Char 'n'),FValue (Char 'e'),FValue (Char 'd')])),TVar "_X1"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 100)])])),TVar "_X1"]) env finalise_returning_ fargs = FApp "finalise-returning" (fargs) stepFinalise_returning fargs = diff --git a/cbs/Funcons/Core/Computations/Abnormal/Throwing/Throwing.hs b/cbs/Funcons/Core/Computations/Abnormal/Throwing/Throwing.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Throwing/Throwing.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Throwing/Throwing.hs @@ -21,7 +21,7 @@ let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 't'),FValue (Char 'h'),FValue (Char 'r'),FValue (Char 'o'),FValue (Char 'w'),FValue (Char 'n')])),TVar "_X1"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 104)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 119)]),FValue (ADTVal "unicode-character" [FValue (Int 110)])])),TVar "_X1"]) env finalise_throwing_ fargs = FApp "finalise-throwing" (fargs) stepFinalise_throwing fargs = diff --git a/cbs/Funcons/Core/Computations/Normal/Binding/Binding.hs b/cbs/Funcons/Core/Computations/Normal/Binding/Binding.hs --- a/cbs/Funcons/Core/Computations/Normal/Binding/Binding.hs +++ b/cbs/Funcons/Core/Computations/Normal/Binding/Binding.hs @@ -30,13 +30,13 @@ env <- vsMatch fargs [VPMetaVar "_X1",VPMetaVar "_X2"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env env <- sideCondition (SCIsInSort (TVar "_X2") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'i'),FValue (Char 'd'),FValue (Char 'e'),FValue (Char 'n'),FValue (Char 't'),FValue (Char 'i'),FValue (Char 'f'),FValue (Char 'i'),FValue (Char 'e'),FValue (Char 'r'),FValue (Char '-'),FValue (Char 't'),FValue (Char 'a'),FValue (Char 'g'),FValue (Char 'g'),FValue (Char 'e'),FValue (Char 'd')])),TVar "_X1",TVar "_X2"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 100)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 102)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 103)]),FValue (ADTVal "unicode-character" [FValue (Int 103)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 100)])])),TVar "_X1",TVar "_X2"]) env fresh_identifier_ = FName "fresh-identifier" stepFresh_identifier = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "identifier-tagged" [TFuncon (FValue (ADTVal "list" [FValue (Char 'g'),FValue (Char 'e'),FValue (Char 'n'),FValue (Char 'e'),FValue (Char 'r'),FValue (Char 'a'),FValue (Char 't'),FValue (Char 'e'),FValue (Char 'd')])),TName "fresh-atom"]) env + rewriteTermTo (TApp "identifier-tagged" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 103)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 100)])])),TName "fresh-atom"]) env initialise_binding_ fargs = FApp "initialise-binding" (fargs) stepInitialise_binding fargs = diff --git a/cbs/Funcons/Core/Computations/Normal/Flowing/Flowing.hs b/cbs/Funcons/Core/Computations/Normal/Flowing/Flowing.hs --- a/cbs/Funcons/Core/Computations/Normal/Flowing/Flowing.hs +++ b/cbs/Funcons/Core/Computations/Normal/Flowing/Flowing.hs @@ -119,7 +119,7 @@ stepSignal = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 's'),FValue (Char 'i'),FValue (Char 'g'),FValue (Char 'n'),FValue (Char 'a'),FValue (Char 'l')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 103)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 108)])]))]) env yield_ = FName "yield" stepYield = evalRules [rewrite1] [] diff --git a/cbs/Funcons/Core/Computations/Normal/Linking/Linking.hs b/cbs/Funcons/Core/Computations/Normal/Linking/Linking.hs --- a/cbs/Funcons/Core/Computations/Normal/Linking/Linking.hs +++ b/cbs/Funcons/Core/Computations/Normal/Linking/Linking.hs @@ -21,7 +21,7 @@ let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 'n'),FValue (Char 'k')])),TVar "_X1"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 107)])])),TVar "_X1"]) env initialise_linking_ fargs = FApp "initialise-linking" (fargs) stepInitialise_linking fargs = diff --git a/cbs/Funcons/Core/Computations/Normal/Storing/Storing.hs b/cbs/Funcons/Core/Computations/Normal/Storing/Storing.hs --- a/cbs/Funcons/Core/Computations/Normal/Storing/Storing.hs +++ b/cbs/Funcons/Core/Computations/Normal/Storing/Storing.hs @@ -53,7 +53,7 @@ env <- vsMatch fargs [VPMetaVar "_X1",VPMetaVar "_X2"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env env <- sideCondition (SCIsInSort (TVar "_X2") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'v'),FValue (Char 'a'),FValue (Char 'r'),FValue (Char 'i'),FValue (Char 'a'),FValue (Char 'b'),FValue (Char 'l'),FValue (Char 'e')])),TVar "_X1",TVar "_X2"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 118)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 98)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 101)])])),TVar "_X1",TVar "_X2"]) env allocate_variable_ fargs = FApp "allocate-variable" (fargs) alloc_ fargs = FApp "allocate-variable" (fargs) diff --git a/cbs/Funcons/Core/Values/Abstraction/Functions/Functions.hs b/cbs/Funcons/Core/Values/Abstraction/Functions/Functions.hs --- a/cbs/Funcons/Core/Values/Abstraction/Functions/Functions.hs +++ b/cbs/Funcons/Core/Values/Abstraction/Functions/Functions.hs @@ -21,7 +21,7 @@ let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'f'),FValue (Char 'u'),FValue (Char 'n'),FValue (Char 'c'),FValue (Char 't'),FValue (Char 'i'),FValue (Char 'o'),FValue (Char 'n')])),TVar "_X1"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 102)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 110)])])),TVar "_X1"]) env apply_ fargs = FApp "apply" (fargs) stepApply fargs = diff --git a/cbs/Funcons/Core/Values/Abstraction/Generic/Generic.hs b/cbs/Funcons/Core/Values/Abstraction/Generic/Generic.hs --- a/cbs/Funcons/Core/Values/Abstraction/Generic/Generic.hs +++ b/cbs/Funcons/Core/Values/Abstraction/Generic/Generic.hs @@ -20,7 +20,7 @@ where rewrite1 = do let env = emptyEnv env <- fsMatch fargs [PMetaVar "_X1"] env - rewriteTermTo (TApp "non-strict-datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'a'),FValue (Char 'b'),FValue (Char 's'),FValue (Char 't'),FValue (Char 'r'),FValue (Char 'a'),FValue (Char 'c'),FValue (Char 't'),FValue (Char 'i'),FValue (Char 'o'),FValue (Char 'n')])),TVar "_X1"]) env + rewriteTermTo (TApp "non-strict-datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 98)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 110)])])),TVar "_X1"]) env closure_ fargs = FApp "closure" (fargs) stepClosure fargs = diff --git a/cbs/Funcons/Core/Values/Abstraction/Patterns/Patterns.hs b/cbs/Funcons/Core/Values/Abstraction/Patterns/Patterns.hs --- a/cbs/Funcons/Core/Values/Abstraction/Patterns/Patterns.hs +++ b/cbs/Funcons/Core/Values/Abstraction/Patterns/Patterns.hs @@ -21,7 +21,7 @@ let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'p'),FValue (Char 'a'),FValue (Char 't'),FValue (Char 't'),FValue (Char 'e'),FValue (Char 'r'),FValue (Char 'n')])),TVar "_X1"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 112)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 110)])])),TVar "_X1"]) env pattern_any_ = FName "pattern-any" stepPattern_any = evalRules [rewrite1] [] @@ -71,7 +71,7 @@ rewrite2 = do let env = emptyEnv env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I1") (TName "identifiers"),VPAnnotated (VPSeqVar "V1*" StarOp) (TSortSeq (TName "values") StarOp)],PADT "datatype-value" [VPAnnotated (VPMetaVar "I2") (TName "identifiers"),VPAnnotated (VPSeqVar "V2*" StarOp) (TSortSeq (TName "values") StarOp)]] env - env <- sideCondition (SCInequality (TVar "I2") (TFuncon (FValue (ADTVal "list" [FValue (Char 'p'),FValue (Char 'a'),FValue (Char 't'),FValue (Char 't'),FValue (Char 'e'),FValue (Char 'r'),FValue (Char 'n')])))) env + env <- sideCondition (SCInequality (TVar "I2") (TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 112)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 110)])])))) env rewriteTermTo (TApp "sequential" [TApp "check-true" [TApp "is-equal" [TVar "I1",TVar "I2"]],TApp "check-true" [TApp "is-equal" [TApp "length" [TVar "V1*"],TApp "length" [TVar "V2*"]]],TApp "collateral" [TApp "interleave-map" [TApp "match" [TApp "tuple-elements" [TName "given"]],TApp "tuple-zip" [TApp "tuple" [TVar "V1*"],TApp "tuple" [TVar "V2*"]]]]]) env rewrite3 = do let env = emptyEnv @@ -100,7 +100,7 @@ rewrite2 = do let env = emptyEnv env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I1") (TName "identifiers"),VPAnnotated (VPSeqVar "V1*" StarOp) (TSortSeq (TName "values") StarOp)],PADT "datatype-value" [VPAnnotated (VPMetaVar "I2") (TName "identifiers"),VPAnnotated (VPSeqVar "V2*" StarOp) (TSortSeq (TName "values") StarOp)]] env - env <- sideCondition (SCInequality (TVar "I2") (TFuncon (FValue (ADTVal "list" [FValue (Char 'p'),FValue (Char 'a'),FValue (Char 't'),FValue (Char 't'),FValue (Char 'e'),FValue (Char 'r'),FValue (Char 'n')])))) env + env <- sideCondition (SCInequality (TVar "I2") (TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 112)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 110)])])))) env rewriteTermTo (TApp "sequential" [TApp "check-true" [TApp "is-equal" [TVar "I1",TVar "I2"]],TApp "check-true" [TApp "is-equal" [TApp "length" [TVar "V1*"],TApp "length" [TVar "V2*"]]],TApp "collateral" [TApp "interleave-map" [TApp "match-loosely" [TApp "tuple-elements" [TName "given"]],TApp "tuple-zip" [TApp "tuple" [TVar "V1*"],TApp "tuple" [TVar "V2*"]]]]]) env rewrite3 = do let env = emptyEnv diff --git a/cbs/Funcons/Core/Values/Abstraction/Thunks/Thunks.hs b/cbs/Funcons/Core/Values/Abstraction/Thunks/Thunks.hs --- a/cbs/Funcons/Core/Values/Abstraction/Thunks/Thunks.hs +++ b/cbs/Funcons/Core/Values/Abstraction/Thunks/Thunks.hs @@ -21,7 +21,7 @@ let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 't'),FValue (Char 'h'),FValue (Char 'u'),FValue (Char 'n'),FValue (Char 'k')])),TVar "_X1"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 104)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 107)])])),TVar "_X1"]) env force_ fargs = FApp "force" (fargs) stepForce fargs = diff --git a/cbs/Funcons/Core/Values/Composite/ASTs/ASTs.hs b/cbs/Funcons/Core/Values/Composite/ASTs/ASTs.hs --- a/cbs/Funcons/Core/Values/Composite/ASTs/ASTs.hs +++ b/cbs/Funcons/Core/Values/Composite/ASTs/ASTs.hs @@ -28,7 +28,7 @@ env <- vsMatch fargs [VPMetaVar "_X1",VPMetaVar "_X2"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env env <- sideCondition (SCIsInSort (TVar "_X2") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'a'),FValue (Char 's'),FValue (Char 't'),FValue (Char '-'),FValue (Char 'v'),FValue (Char 'a'),FValue (Char 'l'),FValue (Char 'u'),FValue (Char 'e')])),TVar "_X1",TVar "_X2"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 118)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 101)])])),TVar "_X1",TVar "_X2"]) env ast_term_ fargs = FApp "ast-term" (fargs) stepAst_term fargs = @@ -38,7 +38,7 @@ env <- vsMatch fargs [VPMetaVar "_X1",VPSeqVar "_X2*" StarOp] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env env <- sideCondition (SCIsInSort (TVar "_X2*") (TSortSeq (TSortSeq (TName "values") QuestionMarkOp) StarOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'a'),FValue (Char 's'),FValue (Char 't'),FValue (Char '-'),FValue (Char 't'),FValue (Char 'e'),FValue (Char 'r'),FValue (Char 'm')])),TVar "_X1",TVar "_X2*"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 109)])])),TVar "_X1",TVar "_X2*"]) env asts_ = FName "asts" stepAsts = rewriteType "asts" [] diff --git a/cbs/Funcons/Core/Values/Composite/Bits/Bits.hs b/cbs/Funcons/Core/Values/Composite/Bits/Bits.hs --- a/cbs/Funcons/Core/Values/Composite/Bits/Bits.hs +++ b/cbs/Funcons/Core/Values/Composite/Bits/Bits.hs @@ -27,7 +27,7 @@ let env = emptyEnv env <- vsMatch fargs [VPSeqVar "_X1*" StarOp] env env <- sideCondition (SCIsInSort (TVar "_X1*") (TSortSeq (TSortSeq (TName "values") QuestionMarkOp) StarOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'b'),FValue (Char 'i'),FValue (Char 't'),FValue (Char '-'),FValue (Char 'v'),FValue (Char 'e'),FValue (Char 'c'),FValue (Char 't'),FValue (Char 'o'),FValue (Char 'r')])),TVar "_X1*"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 98)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 118)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 114)])])),TVar "_X1*"]) env bytes_ = FName "bytes" octets_ = FName "bytes" diff --git a/cbs/Funcons/Core/Values/Composite/Classes/Classes.hs b/cbs/Funcons/Core/Values/Composite/Classes/Classes.hs --- a/cbs/Funcons/Core/Values/Composite/Classes/Classes.hs +++ b/cbs/Funcons/Core/Values/Composite/Classes/Classes.hs @@ -23,7 +23,7 @@ env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env env <- sideCondition (SCIsInSort (TVar "_X2") (TSortSeq (TName "values") QuestionMarkOp)) env env <- sideCondition (SCIsInSort (TVar "_X3*") (TSortSeq (TSortSeq (TName "values") QuestionMarkOp) StarOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'c'),FValue (Char 'l'),FValue (Char 'a'),FValue (Char 's'),FValue (Char 's')])),TVar "_X1",TVar "_X2",TVar "_X3*"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 115)])])),TVar "_X1",TVar "_X2",TVar "_X3*"]) env class_instantiator_ fargs = FApp "class-instantiator" (fargs) stepClass_instantiator fargs = diff --git a/cbs/Funcons/Core/Values/Composite/Lists/Lists.hs b/cbs/Funcons/Core/Values/Composite/Lists/Lists.hs --- a/cbs/Funcons/Core/Values/Composite/Lists/Lists.hs +++ b/cbs/Funcons/Core/Values/Composite/Lists/Lists.hs @@ -21,7 +21,7 @@ let env = emptyEnv env <- vsMatch fargs [VPSeqVar "_X1*" StarOp] env env <- sideCondition (SCIsInSort (TVar "_X1*") (TSortSeq (TSortSeq (TName "values") QuestionMarkOp) StarOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')])),TVar "_X1*"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])])),TVar "_X1*"]) env list_elements_ fargs = FApp "list-elements" (fargs) stepList_elements fargs = @@ -44,7 +44,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')]),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env rewriteTermTo (TApp "list" [TVar "V",TVar "V*"]) env list_head_ fargs = FApp "list-head" (fargs) @@ -53,11 +53,11 @@ evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')]),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)]] env + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)]] env rewriteTermTo (TVar "V") env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')])]] env + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])])]] env rewriteTermTo (TSeq []) env list_tail_ fargs = FApp "list-tail" (fargs) @@ -66,11 +66,11 @@ evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')]),VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env rewriteTermTo (TApp "list" [TVar "V*"]) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')])]] env + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])])]] env rewriteTermTo (TSeq []) env list_length_ fargs = FApp "list-length" (fargs) @@ -78,7 +78,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')]),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env rewriteTermTo (TApp "length" [TVar "V*"]) env list_append_ fargs = FApp "list-append" (fargs) @@ -86,7 +86,7 @@ evalRules [rewrite1,rewrite2,rewrite3,rewrite4] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')]),VPAnnotated (VPSeqVar "V1*" StarOp) (TSortSeq (TName "values") StarOp)],PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')]),VPAnnotated (VPSeqVar "V2*" StarOp) (TSortSeq (TName "values") StarOp)]] env + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),VPAnnotated (VPSeqVar "V1*" StarOp) (TSortSeq (TName "values") StarOp)],PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),VPAnnotated (VPSeqVar "V2*" StarOp) (TSortSeq (TName "values") StarOp)]] env rewriteTermTo (TApp "list" [TVar "V1*",TVar "V2*"]) env rewrite2 = do let env = emptyEnv diff --git a/cbs/Funcons/Core/Values/Composite/Objects/Objects.hs b/cbs/Funcons/Core/Values/Composite/Objects/Objects.hs --- a/cbs/Funcons/Core/Values/Composite/Objects/Objects.hs +++ b/cbs/Funcons/Core/Values/Composite/Objects/Objects.hs @@ -24,7 +24,7 @@ env <- sideCondition (SCIsInSort (TVar "_X2") (TSortSeq (TName "values") QuestionMarkOp)) env env <- sideCondition (SCIsInSort (TVar "_X3") (TSortSeq (TName "values") QuestionMarkOp)) env env <- sideCondition (SCIsInSort (TVar "_X4*") (TSortSeq (TSortSeq (TName "values") QuestionMarkOp) StarOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'o'),FValue (Char 'b'),FValue (Char 'j'),FValue (Char 'e'),FValue (Char 'c'),FValue (Char 't')])),TVar "_X1",TVar "_X2",TVar "_X3",TVar "_X4*"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 98)]),FValue (ADTVal "unicode-character" [FValue (Int 106)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])])),TVar "_X1",TVar "_X2",TVar "_X3",TVar "_X4*"]) env object_identity_ fargs = FApp "object-identity" (fargs) stepObject_identity fargs = diff --git a/cbs/Funcons/Core/Values/Composite/Records/Records.hs b/cbs/Funcons/Core/Values/Composite/Records/Records.hs --- a/cbs/Funcons/Core/Values/Composite/Records/Records.hs +++ b/cbs/Funcons/Core/Values/Composite/Records/Records.hs @@ -21,7 +21,7 @@ let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'r'),FValue (Char 'e'),FValue (Char 'c'),FValue (Char 'o'),FValue (Char 'r'),FValue (Char 'd')])),TVar "_X1"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 100)])])),TVar "_X1"]) env record_map_ fargs = FApp "record-map" (fargs) stepRecord_map fargs = diff --git a/cbs/Funcons/Core/Values/Composite/References/References.hs b/cbs/Funcons/Core/Values/Composite/References/References.hs --- a/cbs/Funcons/Core/Values/Composite/References/References.hs +++ b/cbs/Funcons/Core/Values/Composite/References/References.hs @@ -21,13 +21,13 @@ let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'r'),FValue (Char 'e'),FValue (Char 'f'),FValue (Char 'e'),FValue (Char 'r'),FValue (Char 'e'),FValue (Char 'n'),FValue (Char 'c'),FValue (Char 'e')])),TVar "_X1"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 102)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 101)])])),TVar "_X1"]) env pointer_null_ = FName "pointer-null" stepPointer_null = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'p'),FValue (Char 'o'),FValue (Char 'i'),FValue (Char 'n'),FValue (Char 't'),FValue (Char 'e'),FValue (Char 'r'),FValue (Char '-'),FValue (Char 'n'),FValue (Char 'u'),FValue (Char 'l'),FValue (Char 'l')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 112)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 108)])]))]) env dereference_ fargs = FApp "dereference" (fargs) stepDereference fargs = diff --git a/cbs/Funcons/Core/Values/Composite/Trees/Trees.hs b/cbs/Funcons/Core/Values/Composite/Trees/Trees.hs --- a/cbs/Funcons/Core/Values/Composite/Trees/Trees.hs +++ b/cbs/Funcons/Core/Values/Composite/Trees/Trees.hs @@ -22,7 +22,7 @@ env <- vsMatch fargs [VPMetaVar "_X1",VPSeqVar "_X2*" StarOp] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env env <- sideCondition (SCIsInSort (TVar "_X2*") (TSortSeq (TSortSeq (TName "values") QuestionMarkOp) StarOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 't'),FValue (Char 'r'),FValue (Char 'e'),FValue (Char 'e')])),TVar "_X1",TVar "_X2*"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 101)])])),TVar "_X1",TVar "_X2*"]) env tree_root_value_ fargs = FApp "tree-root-value" (fargs) stepTree_root_value fargs = diff --git a/cbs/Funcons/Core/Values/Composite/Tuples/Tuples.hs b/cbs/Funcons/Core/Values/Composite/Tuples/Tuples.hs --- a/cbs/Funcons/Core/Values/Composite/Tuples/Tuples.hs +++ b/cbs/Funcons/Core/Values/Composite/Tuples/Tuples.hs @@ -21,7 +21,7 @@ let env = emptyEnv env <- vsMatch fargs [VPSeqVar "_X1*" StarOp] env env <- sideCondition (SCIsInSort (TVar "_X1*") (TSortSeq (TSortSeq (TName "values") QuestionMarkOp) StarOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 't'),FValue (Char 'u'),FValue (Char 'p'),FValue (Char 'l'),FValue (Char 'e')])),TVar "_X1*"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 112)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 101)])])),TVar "_X1*"]) env tuple_elements_ fargs = FApp "tuple-elements" (fargs) stepTuple_elements fargs = diff --git a/cbs/Funcons/Core/Values/Composite/Variants/Variants.hs b/cbs/Funcons/Core/Values/Composite/Variants/Variants.hs --- a/cbs/Funcons/Core/Values/Composite/Variants/Variants.hs +++ b/cbs/Funcons/Core/Values/Composite/Variants/Variants.hs @@ -22,7 +22,7 @@ env <- vsMatch fargs [VPMetaVar "_X1",VPMetaVar "_X2"] env env <- sideCondition (SCIsInSort (TVar "_X1") (TSortSeq (TName "values") QuestionMarkOp)) env env <- sideCondition (SCIsInSort (TVar "_X2") (TSortSeq (TName "values") QuestionMarkOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'v'),FValue (Char 'a'),FValue (Char 'r'),FValue (Char 'i'),FValue (Char 'a'),FValue (Char 'n'),FValue (Char 't')])),TVar "_X1",TVar "_X2"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 118)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])])),TVar "_X1",TVar "_X2"]) env variant_id_ fargs = FApp "variant-id" (fargs) stepVariant_id fargs = diff --git a/cbs/Funcons/Core/Values/Composite/Vectors/Vectors.hs b/cbs/Funcons/Core/Values/Composite/Vectors/Vectors.hs --- a/cbs/Funcons/Core/Values/Composite/Vectors/Vectors.hs +++ b/cbs/Funcons/Core/Values/Composite/Vectors/Vectors.hs @@ -21,7 +21,7 @@ let env = emptyEnv env <- vsMatch fargs [VPSeqVar "_X1*" StarOp] env env <- sideCondition (SCIsInSort (TVar "_X1*") (TSortSeq (TSortSeq (TName "values") QuestionMarkOp) StarOp)) env - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'v'),FValue (Char 'e'),FValue (Char 'c'),FValue (Char 't'),FValue (Char 'o'),FValue (Char 'r')])),TVar "_X1*"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 118)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 111)]),FValue (ADTVal "unicode-character" [FValue (Int 114)])])),TVar "_X1*"]) env vector_elements_ fargs = FApp "vector-elements" (fargs) stepVector_elements fargs = diff --git a/cbs/Funcons/Core/Values/Primitive/Booleans/Booleans.hs b/cbs/Funcons/Core/Values/Primitive/Booleans/Booleans.hs --- a/cbs/Funcons/Core/Values/Primitive/Booleans/Booleans.hs +++ b/cbs/Funcons/Core/Values/Primitive/Booleans/Booleans.hs @@ -18,13 +18,13 @@ stepTrue = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 't'),FValue (Char 'r'),FValue (Char 'u'),FValue (Char 'e')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 116)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 101)])]))]) env false_ = FName "false" stepFalse = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'f'),FValue (Char 'a'),FValue (Char 'l'),FValue (Char 's'),FValue (Char 'e')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 102)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 101)])]))]) env not_ fargs = FApp "not" (fargs) stepNot fargs = diff --git a/cbs/Funcons/Core/Values/Primitive/Characters/Characters.hs b/cbs/Funcons/Core/Values/Primitive/Characters/Characters.hs --- a/cbs/Funcons/Core/Values/Primitive/Characters/Characters.hs +++ b/cbs/Funcons/Core/Values/Primitive/Characters/Characters.hs @@ -41,16 +41,16 @@ evalRules [rewrite1,rewrite2,rewrite3] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')]),VPAnnotated (VPMetaVar "C") (TName "ascii-characters")]] env + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),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 (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')]),VPAnnotated (VPMetaVar "C") (TName "characters")]] env + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),VPAnnotated (VPMetaVar "C") (TName "characters")]] env env <- sideCondition (SCIsInSort (TVar "C") (TSortComplement (TName "ascii-characters"))) env rewriteTermTo (TSeq []) env rewrite3 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')]),VPAnnotated (VPSeqVar "C*" StarOp) (TSortSeq (TName "characters") StarOp)]] env + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 115)]),FValue (ADTVal "unicode-character" [FValue (Int 116)])]),VPAnnotated (VPSeqVar "C*" StarOp) (TSortSeq (TName "characters") StarOp)]] env env <- sideCondition (SCInequality (TApp "length" [TVar "C*"]) (TFuncon (FValue (Nat 1)))) env rewriteTermTo (TSeq []) env @@ -58,46 +58,46 @@ stepBackspace = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Char '0'),FValue (Char '0'),FValue (Char '0'),FValue (Char '8')]))]]) env + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 56)])]))]]) 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 (Char '0'),FValue (Char '0'),FValue (Char '0'),FValue (Char '9')]))]]) env + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 57)])]))]]) 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 (Char '0'),FValue (Char '0'),FValue (Char '0'),FValue (Char 'a')]))]]) env + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 97)])]))]]) 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 (Char '0'),FValue (Char '0'),FValue (Char '0'),FValue (Char 'c')]))]]) env + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 99)])]))]]) 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 (Char '0'),FValue (Char '0'),FValue (Char '0'),FValue (Char 'd')]))]]) env + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 100)])]))]]) 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 (Char '0'),FValue (Char '0'),FValue (Char '2'),FValue (Char '2')]))]]) env + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 50)]),FValue (ADTVal "unicode-character" [FValue (Int 50)])]))]]) 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 (Char '0'),FValue (Char '0'),FValue (Char '2'),FValue (Char '7')]))]]) env + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 50)]),FValue (ADTVal "unicode-character" [FValue (Int 55)])]))]]) 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 (Char '0'),FValue (Char '0'),FValue (Char '5'),FValue (Char 'c')]))]]) env + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 48)]),FValue (ADTVal "unicode-character" [FValue (Int 53)]),FValue (ADTVal "unicode-character" [FValue (Int 99)])]))]]) env diff --git a/cbs/Funcons/Core/Values/Primitive/Floats/Floats.hs b/cbs/Funcons/Core/Values/Primitive/Floats/Floats.hs --- a/cbs/Funcons/Core/Values/Primitive/Floats/Floats.hs +++ b/cbs/Funcons/Core/Values/Primitive/Floats/Floats.hs @@ -18,31 +18,31 @@ stepBinary32 = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'b'),FValue (Char 'i'),FValue (Char 'n'),FValue (Char 'a'),FValue (Char 'r'),FValue (Char 'y'),FValue (Char '3'),FValue (Char '2')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 98)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 121)]),FValue (ADTVal "unicode-character" [FValue (Int 51)]),FValue (ADTVal "unicode-character" [FValue (Int 50)])]))]) env binary64_ = FName "binary64" stepBinary64 = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'b'),FValue (Char 'i'),FValue (Char 'n'),FValue (Char 'a'),FValue (Char 'r'),FValue (Char 'y'),FValue (Char '6'),FValue (Char '4')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 98)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 121)]),FValue (ADTVal "unicode-character" [FValue (Int 54)]),FValue (ADTVal "unicode-character" [FValue (Int 52)])]))]) env binary128_ = FName "binary128" stepBinary128 = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'b'),FValue (Char 'i'),FValue (Char 'n'),FValue (Char 'a'),FValue (Char 'r'),FValue (Char 'y'),FValue (Char '1'),FValue (Char '2'),FValue (Char '8')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 98)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 114)]),FValue (ADTVal "unicode-character" [FValue (Int 121)]),FValue (ADTVal "unicode-character" [FValue (Int 49)]),FValue (ADTVal "unicode-character" [FValue (Int 50)]),FValue (ADTVal "unicode-character" [FValue (Int 56)])]))]) env decimal64_ = FName "decimal64" stepDecimal64 = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'd'),FValue (Char 'e'),FValue (Char 'c'),FValue (Char 'i'),FValue (Char 'm'),FValue (Char 'a'),FValue (Char 'l'),FValue (Char '6'),FValue (Char '4')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 100)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 109)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 54)]),FValue (ADTVal "unicode-character" [FValue (Int 52)])]))]) env decimal128_ = FName "decimal128" stepDecimal128 = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'd'),FValue (Char 'e'),FValue (Char 'c'),FValue (Char 'i'),FValue (Char 'm'),FValue (Char 'a'),FValue (Char 'l'),FValue (Char '1'),FValue (Char '2'),FValue (Char '8')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 100)]),FValue (ADTVal "unicode-character" [FValue (Int 101)]),FValue (ADTVal "unicode-character" [FValue (Int 99)]),FValue (ADTVal "unicode-character" [FValue (Int 105)]),FValue (ADTVal "unicode-character" [FValue (Int 109)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 49)]),FValue (ADTVal "unicode-character" [FValue (Int 50)]),FValue (ADTVal "unicode-character" [FValue (Int 56)])]))]) env float_formats_ = FName "float-formats" stepFloat_formats = rewriteType "float-formats" [] diff --git a/cbs/Funcons/Core/Values/Primitive/Null/Null.hs b/cbs/Funcons/Core/Values/Primitive/Null/Null.hs --- a/cbs/Funcons/Core/Values/Primitive/Null/Null.hs +++ b/cbs/Funcons/Core/Values/Primitive/Null/Null.hs @@ -19,7 +19,7 @@ stepNull_value = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'n'),FValue (Char 'u'),FValue (Char 'l'),FValue (Char 'l'),FValue (Char '-'),FValue (Char 'v'),FValue (Char 'a'),FValue (Char 'l'),FValue (Char 'u'),FValue (Char 'e')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (ADTVal "unicode-character" [FValue (Int 110)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 45)]),FValue (ADTVal "unicode-character" [FValue (Int 118)]),FValue (ADTVal "unicode-character" [FValue (Int 97)]),FValue (ADTVal "unicode-character" [FValue (Int 108)]),FValue (ADTVal "unicode-character" [FValue (Int 117)]),FValue (ADTVal "unicode-character" [FValue (Int 101)])]))]) env null_type_ = FName "null-type" stepNull_type = rewriteType "null-type" [] diff --git a/funcons-tools.cabal b/funcons-tools.cabal --- a/funcons-tools.cabal +++ b/funcons-tools.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: funcons-tools -version: 0.2.0.7 +version: 0.2.0.9 synopsis: A modular interpreter for executing funcons description: The PLanCompS project () has developed a component-based approach to formal semantics. @@ -44,11 +44,11 @@ , Funcons.GLLParser , Funcons.RunOptions build-depends: base >=4.8 && <= 5 - ,text >= 1.2 && <1.3 - ,containers >= 0.5 && < 0.6 + ,text >= 1.2 + ,containers >= 0.5 && <= 0.6.0.1 ,vector>=0.12 ,bv >= 0.5 - ,multiset >= 0.3 && < 0.4 + ,multiset >= 0.3 ,split ,directory ,mtl >= 2.2.1 @@ -122,6 +122,7 @@ , Funcons.Core.Values.Composite.MultisetsBuiltin -- , Funcons.Core.Values.Composite.ListsBuiltin , Funcons.Core.Values.Composite.MapsBuiltin + , Funcons.Core.Values.Composite.GraphsBuiltin -- , Funcons.Core.Values.Composite.VectorsBuiltin , Funcons.Core.Values.Composite.DatatypesBuiltin -- , Funcons.Core.Values.Composite.TuplesBuiltin @@ -139,12 +140,12 @@ main-is: Main.hs other-extensions: OverloadedStrings build-depends: base >=4.8 && <= 5 - ,text >= 1.2 && <1.3 - ,containers >= 0.5 && < 0.6 + ,text >= 1.2 + ,containers >= 0.5 && <= 0.6.0.1 ,vector>=0.12 ,bv >= 0.5 ,funcons-tools - ,multiset >= 0.3 && < 0.4 + ,multiset >= 0.3 ,split ,directory ,mtl >= 2.2.1 @@ -152,7 +153,81 @@ ,TypeCompose>=0.9.10 ,regex-applicative ,random-strings - ,funcons-values >= 0.1.0.4 + ,funcons-values >= 0.1.0.5 hs-source-dirs: src, manual, cbs default-language: Haskell2010 -- ghc-options: -rtsopts + other-modules: + Funcons.Core.Computations.Abnormal.Abrupting.Abrupting + Funcons.Core.Computations.Abnormal.Breaking.Breaking + Funcons.Core.Computations.Abnormal.Continuing.Continuing + Funcons.Core.Computations.Abnormal.Controlling.Controlling + Funcons.Core.Computations.Abnormal.Failing.Failing + Funcons.Core.Computations.Abnormal.Returning.Returning + Funcons.Core.Computations.Abnormal.Sticking + Funcons.Core.Computations.Abnormal.Throwing.Throwing + Funcons.Core.Computations.AbnormalBuiltin + Funcons.Core.Computations.Normal.Binding.Binding + Funcons.Core.Computations.Normal.Flowing.Flowing + Funcons.Core.Computations.Normal.Generating.Generating + Funcons.Core.Computations.Normal.GeneratingBuiltin + Funcons.Core.Computations.Normal.Giving.Giving + Funcons.Core.Computations.Normal.Interacting.Interacting + Funcons.Core.Computations.Normal.Linking.Linking + Funcons.Core.Computations.Normal.Storing.Storing + Funcons.Core.Computations.TypesBuiltin + Funcons.Core.Library + Funcons.Core.Manual + Funcons.Core.Values.Abstraction.Functions.Functions + Funcons.Core.Values.Abstraction.Generic.Generic + Funcons.Core.Values.Abstraction.Patterns.Patterns + Funcons.Core.Values.Abstraction.Thunks.Thunks + Funcons.Core.Values.Composite.ASTs.ASTs + Funcons.Core.Values.Composite.Bits.Bits + Funcons.Core.Values.Composite.Classes.Classes + Funcons.Core.Values.Composite.Datatypes.Datatypes + Funcons.Core.Values.Composite.DatatypesBuiltin + Funcons.Core.Values.Composite.Graphs.Graphs + Funcons.Core.Values.Composite.GraphsBuiltin + Funcons.Core.Values.Composite.Lists.Lists + Funcons.Core.Values.Composite.MapsBuiltin + Funcons.Core.Values.Composite.MultisetsBuiltin + Funcons.Core.Values.Composite.Objects.Objects + Funcons.Core.Values.Composite.Records.Records + Funcons.Core.Values.Composite.References.References + Funcons.Core.Values.Composite.Sequences.Sequences + Funcons.Core.Values.Composite.SetsBuiltin + Funcons.Core.Values.Composite.Strings.Strings + Funcons.Core.Values.Composite.Trees.Trees + Funcons.Core.Values.Composite.Tuples.Tuples + Funcons.Core.Values.Composite.Variants.Variants + Funcons.Core.Values.Composite.Vectors.Vectors + Funcons.Core.Values.Primitive.Atoms + Funcons.Core.Values.Primitive.BitsBuiltin + Funcons.Core.Values.Primitive.BoolBuiltin + Funcons.Core.Values.Primitive.Booleans.Booleans + Funcons.Core.Values.Primitive.Characters.Characters + Funcons.Core.Values.Primitive.CharactersBuiltin + Funcons.Core.Values.Primitive.Floats.Floats + Funcons.Core.Values.Primitive.FloatsBuiltin + Funcons.Core.Values.Primitive.Integers.Integers + Funcons.Core.Values.Primitive.IntegersBuiltin + Funcons.Core.Values.Primitive.Null.Null + Funcons.Core.Values.Primitive.StringsBuiltin + Funcons.Core.Values.TypesBuiltin + Funcons.Core.Values.ValueTypes.ValueTypes + Funcons.EDSL + Funcons.Entities + Funcons.Exceptions + Funcons.GLLParser + Funcons.MSOS + Funcons.Parser + Funcons.Patterns + Funcons.Printer + Funcons.RunOptions + Funcons.Simulation + Funcons.Substitution + Funcons.Tools + Funcons.TypeSubstitution + Funcons.Types + diff --git a/manual/Funcons/Core/Manual.hs b/manual/Funcons/Core/Manual.hs --- a/manual/Funcons/Core/Manual.hs +++ b/manual/Funcons/Core/Manual.hs @@ -6,6 +6,7 @@ , module Funcons.Core.Values.Composite.MultisetsBuiltin -- , module Funcons.Core.Values.Composite.ListsBuiltin , module Funcons.Core.Values.Composite.MapsBuiltin + , module Funcons.Core.Values.Composite.GraphsBuiltin -- , module Funcons.Core.Values.Composite.VectorsBuiltin , module Funcons.Core.Values.Composite.DatatypesBuiltin , module Funcons.Core.Values.Primitive.StringsBuiltin @@ -17,6 +18,7 @@ , module Funcons.Core.Values.Primitive.CharactersBuiltin -- , module Funcons.Core.Values.Composite.TuplesBuiltin , module Funcons.Core.Values.TypesBuiltin + , module Funcons.Core.Computations.TypesBuiltin )where import Funcons.EDSL @@ -24,6 +26,7 @@ import Funcons.Core.Values.Composite.MultisetsBuiltin hiding (library) --import Funcons.Core.Values.Composite.ListsBuiltin hiding (library) import Funcons.Core.Values.Composite.MapsBuiltin hiding (library) +import Funcons.Core.Values.Composite.GraphsBuiltin hiding (library) --import Funcons.Core.Values.Composite.VectorsBuiltin hiding (library) import Funcons.Core.Values.Composite.DatatypesBuiltin hiding (library) import Funcons.Core.Values.Primitive.StringsBuiltin hiding (library) @@ -33,6 +36,8 @@ import Funcons.Core.Values.Primitive.Atoms hiding (library) import Funcons.Core.Values.Primitive.BoolBuiltin hiding (library) import Funcons.Core.Values.Primitive.CharactersBuiltin hiding (library) +import Funcons.Core.Values.TypesBuiltin hiding (library) +import Funcons.Core.Computations.TypesBuiltin hiding (library) --import Funcons.Core.Values.Composite.TuplesBuiltin hiding (library) import qualified Funcons.Core.Computations.Normal.GeneratingBuiltin @@ -41,6 +46,7 @@ import qualified Funcons.Core.Values.Composite.MultisetsBuiltin --import qualified Funcons.Core.Values.Composite.ListsBuiltin import qualified Funcons.Core.Values.Composite.MapsBuiltin +import qualified Funcons.Core.Values.Composite.GraphsBuiltin --import qualified Funcons.Core.Values.Composite.VectorsBuiltin import qualified Funcons.Core.Values.Composite.DatatypesBuiltin import qualified Funcons.Core.Values.Primitive.StringsBuiltin @@ -62,6 +68,7 @@ , Funcons.Core.Values.Composite.MultisetsBuiltin.library -- , Funcons.Core.Values.Composite.ListsBuiltin.library , Funcons.Core.Values.Composite.MapsBuiltin.library + , Funcons.Core.Values.Composite.GraphsBuiltin.library -- , Funcons.Core.Values.Composite.VectorsBuiltin.library , Funcons.Core.Values.Composite.DatatypesBuiltin.library , Funcons.Core.Values.Primitive.StringsBuiltin.library diff --git a/manual/Funcons/Core/Values/Composite/GraphsBuiltin.hs b/manual/Funcons/Core/Values/Composite/GraphsBuiltin.hs new file mode 100644 --- /dev/null +++ b/manual/Funcons/Core/Values/Composite/GraphsBuiltin.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Values.Composite.GraphsBuiltin where + +import Funcons.EDSL +import qualified Funcons.Operations as VAL + +library = libFromList [ + ("is-cyclic", fromValOp is_cyclic_ VAL.is_cyclic_) + , ("topological-sort", fromValOp topological_sort_ VAL.topological_sort_) + ] + +is_cyclic_ = applyFuncon "is-cyclic" +topological_sort_ = applyFuncon "topological-sort" diff --git a/manual/Funcons/Core/Values/Composite/MultisetsBuiltin.hs b/manual/Funcons/Core/Values/Composite/MultisetsBuiltin.hs --- a/manual/Funcons/Core/Values/Composite/MultisetsBuiltin.hs +++ b/manual/Funcons/Core/Values/Composite/MultisetsBuiltin.hs @@ -3,78 +3,23 @@ module Funcons.Core.Values.Composite.MultisetsBuiltin where import Funcons.EDSL -import Funcons.Operations hiding (Values,libFromList) -import Funcons.Core.Values.Primitive.BoolBuiltin - -import qualified Data.MultiSet as MS +import qualified Funcons.Operations as VAL library = libFromList [ - ("multiset-empty", NullaryFuncon (rewritten (Multiset MS.empty))) - , ("sets-to-multiset", ValueOp stepSetsToMultiset) - , ("multiset-to-set", ValueOp stepMultisetToSet) --- , ("multiset-to-list", ValueOp stepMultisetToList) --- , ("list-to-multiset", ValueOp list_to_multiset_op) - , ("multiset-occurrences", ValueOp stepMultisetOccurrences) - , ("multiset-insert", ValueOp stepMultisetInsert) - , ("multiset-delete", ValueOp stepMultisetDelete) - , ("is-submultiset", ValueOp stepIsSubMultiset) + ("multisets", fromValOp multisets_ VAL.multisets_) + , ("multiset", fromValOp multiset_ VAL.multiset_) + , ("multiset-elements", fromValOp multiset_elements_ VAL.multiset_elements_) + , ("multiset-occurrences", fromValOp multiset_occurrences_ VAL.multiset_occurrences_) + , ("multiset-insert", fromValOp multiset_insert_ VAL.multiset_insert_) + , ("multiset-delete", fromValOp multiset_delete_ VAL.multiset_delete_) + , ("is-submultiset", fromValOp is_submultiset_ VAL.is_submultiset_) ] -is_sub_multiset = applyFuncon "is-sub-multiset" -stepIsSubMultiset [Multiset s1, Multiset s2] = - rewriteTo $ FValue $ tobool (s1 `MS.isSubsetOf`s2) -stepIsSubMultiset vs = sortErr (is_sub_multiset (map FValue vs)) - "is-sub-multiset not applied to two multisets" - -multiset_delete = applyFuncon "multiset-delete" -stepMultisetDelete [Multiset ms, v, vn] - | Nat n <- upcastNaturals vn = rewriteTo $ FValue $ Multiset (MS.deleteMany v (fromInteger n) ms) -stepMultisetDelete vs = sortErr (multiset_delete (map FValue vs)) - "multiset-delete not applied to a multiset, value and natural number" - -multiset_insert = applyFuncon "multiset-insert" -stepMultisetInsert [v, vn, Multiset ms] - | Nat n <- upcastNaturals vn = rewriteTo $ FValue $ Multiset (MS.insertMany v (fromInteger n) ms) -stepMultisetInsert vs = sortErr (multiset_insert (map FValue vs)) - "multiset-insert not applied to a value, natural number and multiset" - -multiset_occurrences = applyFuncon "multiset-occurrences" -stepMultisetOccurrences [v, Multiset ms] = rewriteTo $ int_ (MS.occur v ms) -stepMultisetOccurrences vs = sortErr (multiset_occurrences (map FValue vs)) - "multiset-occurrences not applied to a value and a multiset" - -multiset_to_set = applyFuncon "multiset-to-set" -stepMultisetToSet [Multiset ms] = rewriteTo $ FValue $ Set (MS.toSet ms) -stepMultisetToSet vs = sortErr (multiset_to_set (map FValue vs)) - "multiset-to-set not applied to a multiset" - -{- -multiset_to_list = applyFuncon "multiset-to-list" -stepMultisetToList [Multiset ms] = rewriteTo $ FValue $ List $ map intPairToNatTuple (MS.toOccurList ms) - where - intPairToNatTuple :: (Values,Int) -> Values - intPairToNatTuple (v,i) = NonEmptyTuple v (Nat $ toInteger i) [] -stepMultisetToList vs = sortErr (multiset_to_list (map FValue vs)) - "multiset-to-list not applied to a multiset" - -list_to_multiset_op vs@[List xs] = do ps <- mapM natTupleToIntPair xs - rewriteTo $ FValue $ Multiset $ MS.fromOccurList ps - where - natTupleToIntPair :: Values -> Rewrite (Values,Int) - natTupleToIntPair (NonEmptyTuple v m []) | Nat n <- upcastNaturals m = return (v,fromIntegral n) - natTupleToIntPair _ = sortErr (applyFuncon "list-to-multiset" (fvalues vs)) - "list-to-multiset not applied to a list of tuples of values and naturals" -list_to_multiset_op vs = sortErr (applyFuncon "list-to-multiset" (fvalues vs)) - "list-to-multiset not applied to a list" --} - +multisets_ = applyFuncon "multisets" +multiset_ = applyFuncon "multiset" +multiset_elements_ = applyFuncon "multiset-elements" +multiset_occurrences_ = applyFuncon "multiset-occurrences" +multiset_insert_ = applyFuncon "multiset-insert" +multiset_delete_ = applyFuncon "multiset-delete" +is_submultiset_ = applyFuncon "is-submultiset" -sets_to_multiset = applyFuncon "sets-to-multiset" -stepSetsToMultiset vs - | all isSet_ vs = rewriteTo $ FValue $ Multiset (MS.unions (map toMS vs)) - | otherwise = sortErr (sets_to_multiset (map FValue vs)) - "sets-to-multiset not applied to sets" - where isSet_ (Set _) = True - isSet_ _ = False - toMS (Set s) = MS.fromSet s - toMS _ = error "sets-to-multiset" diff --git a/manual/Funcons/Core/Values/Composite/SetsBuiltin.hs b/manual/Funcons/Core/Values/Composite/SetsBuiltin.hs --- a/manual/Funcons/Core/Values/Composite/SetsBuiltin.hs +++ b/manual/Funcons/Core/Values/Composite/SetsBuiltin.hs @@ -4,7 +4,6 @@ import Funcons.EDSL hiding (set_) import qualified Funcons.Operations as VAL -import Funcons.Core.Values.Primitive.BoolBuiltin import qualified Data.Set as S diff --git a/manual/Funcons/Core/Values/Primitive/Atoms.hs b/manual/Funcons/Core/Values/Primitive/Atoms.hs --- a/manual/Funcons/Core/Values/Primitive/Atoms.hs +++ b/manual/Funcons/Core/Values/Primitive/Atoms.hs @@ -7,7 +7,9 @@ library = libFromList [ ("atom", fromValOp atom_ VAL.atom_) + , ("atoms", fromValOp atoms_ VAL.atoms_) ] +atoms_ = applyFuncon "atoms" atom_ = applyFuncon "atom" diff --git a/manual/Funcons/Core/Values/Primitive/BitsBuiltin.hs b/manual/Funcons/Core/Values/Primitive/BitsBuiltin.hs --- a/manual/Funcons/Core/Values/Primitive/BitsBuiltin.hs +++ b/manual/Funcons/Core/Values/Primitive/BitsBuiltin.hs @@ -3,67 +3,28 @@ module Funcons.Core.Values.Primitive.BitsBuiltin where import Funcons.EDSL -import Funcons.Types - -import qualified Data.BitVector as BV +import qualified Funcons.Operations as VAL library = libFromList [ - ("bits-to-integer", ValueOp stepBits_To_Integer) - , ("integer-to-bits", ValueOp stepInteger_To_Bits) - , ("bits-not", ValueOp stepBits_Not) - , ("bits-or", ValueOp stepBits_Or) - , ("bits-and", ValueOp stepBits_And) - , ("bits-xor", ValueOp stepBits_Xor) - , ("bits-shift-left", ValueOp stepBits_Shift_Left) - , ("bits-logical-shift-right", ValueOp stepBits_Logical_Shift_Right) - , ("bits-arithmetic-shift-right", ValueOp stepBits_Arithmetic_Shift_Right) - , ("bits-to-integer", ValueOp stepBits_To_Integer) - , ("bits-to-natural", ValueOp stepBits_To_Natural) - , ("integer-to-bits", ValueOp stepInteger_To_Bits) + ("bit-vector-not", fromValOp bit_vector_not_ VAL.bit_vector_not_) + , ("bit-vector-and", fromValOp bit_vector_and_ VAL.bit_vector_and_) + , ("bit-vector-or", fromValOp bit_vector_or_ VAL.bit_vector_or_) + , ("bit-vector-xor", fromValOp bit_vector_xor_ VAL.bit_vector_xor_) + , ("bit-vector-shift-left", fromValOp bit_vector_shift_left_ VAL.bit_vector_shift_left_) + , ("bit-vector-logical-shift-right", fromValOp bit_vector_logical_shift_right_ VAL.bit_vector_logical_shift_right_) + , ("bit-vector-arithmetic-shift-right", fromValOp bit_vector_arithmetical_shift_right_ VAL.bit_vector_arithmetical_shift_right_) + , ("integer-to-bit-vector", fromValOp integer_to_bit_vector_ VAL.integer_to_bit_vector_) + , ("bit-vector-to-integer", fromValOp bit_vector_to_integer_ VAL.bit_vector_to_integer_) + , ("bit-vector-to-natural", fromValOp bit_vector_to_natural_ VAL.bit_vector_to_natural_) ] -stepBits_Not [Bit bv] = rewriteTo $ FValue $ Bit $ BV.not bv -stepBits_Not vs = sortErr (applyFuncon "bits-not" (fvalues vs)) "bits-not not applied to bits" -stepBits_And [Bit bv1, Bit bv2] = rewriteTo $ FValue $ Bit (bv1 BV..&. bv2) -stepBits_And vs = sortErr (applyFuncon "bits-and" (fvalues vs)) "bits-and not applied to bits" - -bits_or = applyFuncon "bits-or" -stepBits_Or [Bit bv1, Bit bv2] = rewriteTo $ FValue $ Bit (bv1 BV..|. bv2) -stepBits_Or vs = sortErr (bits_or (fvalues vs)) "bits-or not applied to bits" - -bits_xor = applyFuncon "bits-xor" -stepBits_Xor [Bit bv1, Bit bv2] = rewriteTo $ FValue $ Bit (bv1 `BV.xor` bv2) -stepBits_Xor vs = sortErr (bits_xor (fvalues vs)) "bits-xor not applied to bits" - -bits_shift_left = applyFuncon "bits-shift-left" -stepBits_Shift_Left [Bit bv1, vn] - | Nat n <- upcastNaturals vn = rewriteTo $ FValue $ Bit (bv1 `BV.shl` (fromInteger n)) -stepBits_Shift_Left vs = sortErr (bits_shift_left (fvalues vs)) "bits-shift not applied to bits" - -bits_arithmetic_shift_right = applyFuncon "bits-arithmetic-shift_right" -stepBits_Arithmetic_Shift_Right [Bit bv1, vn] - | Nat n <- upcastNaturals vn = rewriteTo $ FValue $ Bit (bv1 `BV.ashr` (fromInteger n)) -stepBits_Arithmetic_Shift_Right vs = - sortErr (bits_arithmetic_shift_right (fvalues vs)) - "bits-arithmetic-shift-right not applied to bits" - -bits_logical_shift_right = applyFuncon "bits-logical-shift-right" -stepBits_Logical_Shift_Right [Bit bv1, vn] - | Nat n <- upcastNaturals vn = rewriteTo $ FValue $ Bit (bv1 `BV.shr` (fromInteger n)) -stepBits_Logical_Shift_Right vs = - sortErr (bits_logical_shift_right (fvalues vs)) "bits-logical-shift-right" - -bits_to_integer = applyFuncon "bits-to-integer" -stepBits_To_Integer [Bit bv] = rewriteTo $ int_ $ fromInteger $ (BV.int bv) -stepBits_To_Integer vs = sortErr (bits_to_integer (fvalues vs)) - "bits-to-integer not applied to bits" - -bits_to_natural = applyFuncon "bits-to-natural" -stepBits_To_Natural [Bit bv] = rewriteTo $ FValue $ mk_naturals (BV.nat bv) -stepBits_To_Natural vs = sortErr (bits_to_natural (fvalues vs)) "bits-to-natural not applied to bits" -integer_to_bits = applyFuncon "integer-to-bits" -stepInteger_To_Bits [vn,vi] - | (Nat n, Int i) <- (upcastNaturals vn, upcastIntegers vi) - = rewriteTo $ FValue $ Bit (BV.bitVec (fromInteger n) (i `mod` (2 ^ n))) -stepInteger_To_Bits vs = sortErr (applyFuncon "integer-to-bits" (fvalues vs)) - "sort check: integer-to-bits(_:naturals,_:integers)" +bit_vector_not_ = applyFuncon "bit-vector-not" +bit_vector_and_ = applyFuncon "bit-vector-and" +bit_vector_or_ = applyFuncon "bit-vector-or" +bit_vector_xor_ = applyFuncon "bit-vector-xor" +bit_vector_shift_left_ = applyFuncon "bit-vector-shift-left" +bit_vector_logical_shift_right_ = applyFuncon "bit-vector-logical-shift-right" +bit_vector_arithmetical_shift_right_ = applyFuncon "bit-vector-arithmetical-shift-right" +integer_to_bit_vector_ = applyFuncon "integer-to-bit-vector" +bit_vector_to_integer_ = applyFuncon "bit-vector-to-integer" +bit_vector_to_natural_ = applyFuncon "bit-vector-to-natural" diff --git a/manual/Funcons/Core/Values/Primitive/CharactersBuiltin.hs b/manual/Funcons/Core/Values/Primitive/CharactersBuiltin.hs --- a/manual/Funcons/Core/Values/Primitive/CharactersBuiltin.hs +++ b/manual/Funcons/Core/Values/Primitive/CharactersBuiltin.hs @@ -6,17 +6,35 @@ import qualified Funcons.Operations as VAL library = libFromList [ - ("ascii-characters", fromNullaryValOp ascii_characters_ VAL.ascii_characters_) --- , ("ascii-character", fromValOp ascii_character_ VAL.ascii_character_) - , ("unicode", fromValOp unicode_ VAL.unicode_) - , ("unicode-character-code", fromValOp unicode_character_code_ VAL.unicode_character_code_) - , ("characters", fromNullaryValOp characters_ VAL.characters_) + ("characters", fromNullaryValOp characters_ VAL.characters_) , ("chars", fromNullaryValOp characters_ VAL.characters_) + , ("unicode-characters", fromNullaryValOp unicode_characters_ VAL.unicode_characters_) + , ("unicode-chars", fromNullaryValOp unicode_characters_ VAL.unicode_characters_) + , ("unicode-points", fromNullaryValOp unicode_points_ VAL.unicode_points_) + , ("basic-multilingual-plane-points", fromNullaryValOp basic_multilingual_plane_points_ VAL.bmp_points_) + , ("unicode-character", fromValOp unicode_character_ VAL.unicode_character_) + , ("unicode-char", fromValOp unicode_character_ VAL.unicode_character_) + , ("basic-multilingual-plane-characters", fromNullaryValOp basic_multilingual_plane_characters_ VAL.bmp_characters_) + , ("bmp-chars", fromNullaryValOp basic_multilingual_plane_characters_ VAL.bmp_characters_) + , ("iso-latin-1-characters", fromNullaryValOp iso_latin_1_characters_ VAL.iso_latin_characters_) + , ("latin-1-chars", fromNullaryValOp iso_latin_1_characters_ VAL.iso_latin_characters_) + , ("ascii-characters", fromNullaryValOp ascii_characters_ VAL.ascii_characters_) + , ("ascii-chars", fromNullaryValOp ascii_characters_ VAL.ascii_characters_) ] ascii_characters_ = applyFuncon "ascii-characters" +ascii_chars_ = applyFuncon "ascii-characters" +unicode_characters_ = applyFuncon "unicode-characters" +iso_latin_1_characters_ = applyFuncon "iso-latin-1-characters" +latin_1_chars_ = applyFuncon "iso-latin-1-characters" +basic_multilingual_plane_characters_ = applyFuncon "basic-multilingual-plane-characters" +bmp_chars_ = applyFuncon "basic-multilingual-plane-characters" +unicode_points_ = applyFuncon "unicode-points" +basic_multilingual_plane_points_ = applyFuncon "basic-multilingual-plane-points" ascii_character_ = applyFuncon "ascii-character" -unicode_ = applyFuncon "unicode" -unicode_character_code_ = applyFuncon "unicode-character-code" +unicode_character_ = applyFuncon "unicode-character" +unicode_char_ = applyFuncon "unicode-character" +--unicode_point_ = applyFuncon "unicode-point" TODO reveal once built-in +--unicode_ = applyFuncon "unicode-point" TODO reveal once built-in characters_ = applyFuncon "characters" chars_ = applyFuncon "characters" diff --git a/manual/Funcons/Core/Values/Primitive/IntegersBuiltin.hs b/manual/Funcons/Core/Values/Primitive/IntegersBuiltin.hs --- a/manual/Funcons/Core/Values/Primitive/IntegersBuiltin.hs +++ b/manual/Funcons/Core/Values/Primitive/IntegersBuiltin.hs @@ -20,9 +20,17 @@ , ("int-pow", fromValOp integer_power_ VAL.integer_power_) , ("integer-list", fromValOp integer_list_ VAL.integer_list_) , ("integer-modulo", fromValOp integer_modulo_ VAL.integer_modulo_) + , ("int-mod", fromValOp integer_modulo_ VAL.integer_modulo_) , ("integer-absolute-value", fromValOp integer_absolute_value_ VAL.integer_absolute_value_) , ("integer-abs", fromValOp integer_absolute_value_ VAL.integer_absolute_value_) , ("decimal-natural", fromValOp decimal_natural_ VAL.decimal_natural_) + , ("decimal", fromValOp decimal_natural_ VAL.decimal_natural_) + , ("hexadecimal-natural", fromValOp hexadecimal_natural_ VAL.hexadecimal_natural_) + , ("hexadecimal", fromValOp hexadecimal_natural_ VAL.hexadecimal_natural_) + , ("octal-natural", fromValOp octal_natural_ VAL.octal_natural_) + , ("octal", fromValOp octal_natural_ VAL.octal_natural_) + , ("binary-natural", fromValOp binary_natural_ VAL.binary_natural_) + , ("binary", fromValOp binary_natural_ VAL.binary_natural_) , ("natural-predecessor", fromValOp natural_predecessor_ VAL.natural_predecessor_) , ("nat-pred", fromValOp natural_predecessor_ VAL.natural_predecessor_) , ("natural-successor", fromValOp natural_successor_ VAL.natural_successor_) @@ -48,7 +56,7 @@ integers_from_ = applyFuncon "integers-from" from_ = applyFuncon "from" integers_up_to_ = applyFuncon "integers-up-to" -up_to_ = applyFuncon "integers-up-to" +up_to_ = applyFuncon "up-to" natural_predecessor_, nat_pred_ :: [Funcons] -> Funcons natural_predecessor_ = applyFuncon "natural-predecessor" nat_pred_ = applyFuncon "nat-pred" @@ -65,9 +73,17 @@ "integer-power not applied to two integers" integer_list_ = applyFuncon "integer-list" integer_modulo_ = applyFuncon "integer-modulo" +int_mod_ = applyFuncon "int-mod" integer_mod_ = applyFuncon "integer-modulo" integer_absolute_value_ = applyFuncon "integer-absolute-value" decimal_natural_ = FApp "decimal-natural" +decimal_ = FApp "decimal" +octal_natural_ = FApp "octal-natural" +octal_ = FApp "octal" +binary_natural_ = FApp "binary-natural" +binary_ = FApp "binary" +hexadecimal_natural_ = FApp "hexadecimal-natural" +hexadecimal_ = FApp "hexadecimal" is_less_ = applyFuncon "is-less" integer_is_less_ = applyFuncon "is-less" is_less_or_equal_ = FApp "is-less-or-equal" diff --git a/manual/Funcons/Core/Values/TypesBuiltin.hs b/manual/Funcons/Core/Values/TypesBuiltin.hs --- a/manual/Funcons/Core/Values/TypesBuiltin.hs +++ b/manual/Funcons/Core/Values/TypesBuiltin.hs @@ -9,15 +9,14 @@ ("datatype-values", fromNullaryValOp datatype_values_ VAL.datatype_values_) , ("ground-values", fromNullaryValOp ground_values_ VAL.ground_values_) , ("ground-vals", fromNullaryValOp ground_values_ VAL.ground_values_) --- , ("null", fromNullaryValOp null_ VAL.null_) --- , ("null-type", fromNullaryValOp nulltype_ VAL.nulltype_) , ("types", fromNullaryValOp types_ VAL.types_) , ("value-types", fromNullaryValOp value_types_ VAL.value_types_) + , ("empty-type", fromNullaryValOp empty_type_ VAL.empty_type_) ] -types_ = applyFuncon "types" -value_types_ = applyFuncon "value-types" -nulltype_ = applyFuncon "null-type" datatype_values_ = applyFuncon "datatype-values" -null_ = applyFuncon "null" ground_values_ = applyFuncon "ground-values" +ground_vals_ = applyFuncon "ground-vals" +types_ = applyFuncon "types" +value_types_ = applyFuncon "value-types" +empty_type_ = applyFuncon "empty-type" diff --git a/src/Funcons/EDSL.hs b/src/Funcons/EDSL.hs --- a/src/Funcons/EDSL.hs +++ b/src/Funcons/EDSL.hs @@ -13,17 +13,17 @@ -- *** Funcon terms set_, vec_, env_fromlist_, null__, -- *** Values - int_, bool_, bool__, list__, vector__, tuple__, ascii_, ascii__,char_, char__, nat_, float_, ieee_float_32_, ieee_float_64_, string_, string__, atom_, + int_, bool_, bool__, list__, vector__, tuple__, char_, char__, nat_, float_, ieee_float_32_, ieee_float_64_, string_, string__, atom_, -- *** Types - values_, integers_, atoms_, unicode_characters_, vectors_, type_, ty_star, ty_plus, ty_opt, ty_union, ty_neg, ty_inter, ty_power, + values_, integers_, vectors_, type_, ty_star, ty_plus, ty_opt, ty_union, ty_neg, ty_inter, ty_power, -- ** Pretty-print funcon terms showValues, showValuesSeq, showFuncons, showFunconsSeq, showTypes, showTerms, showOp, -- ** Is a funcon term a certain value? isVal, isInt, isNat, isList, isMap, isType, - isVec, isAscii, isChar, isTup, isString, isString_, unString, + isVec, isChar, isTup, isString, isString_, unString, -- ** Up and downcasting between funcon terms downcastValue, downcastType, downcastValueType, - upcastNaturals, upcastIntegers, upcastRationals, upcastUnicode, + upcastNaturals, upcastIntegers, upcastRationals,upcastCharacter, -- ** Evaluation functions EvalFunction(..), Strictness(..), StrictFuncon, PartiallyStrictFuncon, NonStrictFuncon, ValueOp, NullaryFuncon, diff --git a/src/Funcons/GLLParser.hs b/src/Funcons/GLLParser.hs --- a/src/Funcons/GLLParser.hs +++ b/src/Funcons/GLLParser.hs @@ -112,7 +112,7 @@ pValues :: Parser Values pValues = "VALUES" - <:=> Char <$$> char_lit + <:=> mk_unicode_characters <$$> char_lit <||> string__ <$$> string_lit <||> mk_integers . toInteger <$$> int_lit <||> IEEE_Float_64 . fst . head . readFloat <$$> pRatioAsString diff --git a/src/Funcons/MSOS.hs b/src/Funcons/MSOS.hs --- a/src/Funcons/MSOS.hs +++ b/src/Funcons/MSOS.hs @@ -47,10 +47,12 @@ import Control.Applicative import Control.Arrow ((***)) -import Control.Monad.Writer +import Control.Monad.Writer hiding ((<>)) +import Control.Monad.Fail import Data.Maybe (isJust, isNothing, fromJust) import Data.List (foldl', intercalate) import Data.Text (unpack) +import Data.Semigroup import qualified Data.Map as M @@ -210,6 +212,9 @@ (a2,st2,cs2) = h ctxt st1 in (a2,st2,cs1 <> cs2)) +instance Semigroup RewriteWriterr where + (<>) = mappend + instance Monoid RewriteWriterr where mempty = RewriteWriterr mempty (RewriteWriterr cs1) `mappend` (RewriteWriterr cs2) = RewriteWriterr (cs1 `mappend` cs2) @@ -315,6 +320,12 @@ (a2,mut2,wr2) <- h ctxt mut1 return (a2,mut2,wr1 <> wr2)) +instance MonadFail MSOS where + fail = liftRewrite . internal + +instance Semigroup MSOSWriter where + (<>) = mappend + instance Monoid MSOSWriter where mempty = MSOSWriter mempty mempty mempty (MSOSWriter x1 x2 x3) `mappend` (MSOSWriter y1 y2 y3) = @@ -440,6 +451,9 @@ ----------- -- steps, rewrites, restarts, refocus, delegations, backtracking (outer/inner) data Counters = Counters !Int !Int !Int !Int !Int !Int !Int !Int + +instance Semigroup Counters where + (<>) = mappend instance Monoid Counters where mempty = Counters 0 0 0 0 0 0 0 0 diff --git a/src/Funcons/Patterns.hs b/src/Funcons/Patterns.hs --- a/src/Funcons/Patterns.hs +++ b/src/Funcons/Patterns.hs @@ -450,6 +450,11 @@ ty <- rewritesToType ty' and <$> mapM (flip Funcons.Patterns.isInType ty) (toList ls) _ -> return False +-- characters +isInType v AsciiCharacters = isInUnicodeType v "ascii-points" +isInType v ISOLatinCharacters = isInUnicodeType v "iso-latin-1-points" +isInType v BMPCharacters = isInUnicodeType v "basic-multilingual-plane-points" +-- type operators and datatypes isInType v (ADT nm tys) = do DataTypeMemberss _ tpats alts <- typeEnvLookup nm or <$> mapM (isInAlt tpats) alts @@ -476,6 +481,15 @@ isInType v (Complement t) = not <$> Funcons.Patterns.isInType v t isInType v t = maybe (return False) return (Funcons.Types.isInType v t) + +isInUnicodeType v@(ADTVal c [p]) fname = do + rangeTy <- rewritesToType (applyFuncon fname []) + isUnicode <- Funcons.Patterns.isInType v UnicodeCharacters + point <- rewritesToValue p + inRange <- Funcons.Patterns.isInType point rangeTy + return (and [isUnicode,inRange]) +isInUnicodeType _ _ = return False + isInTupleType :: [Values] -> [TTParam] -> Rewrite Bool isInTupleType vs ttparams = diff --git a/src/Funcons/Types.hs b/src/Funcons/Types.hs --- a/src/Funcons/Types.hs +++ b/src/Funcons/Types.hs @@ -5,13 +5,14 @@ module VAL,) where import qualified Funcons.Operations as VAL hiding (SortErr, ValueOp) -import Funcons.Operations hiding (Name, Values, ComputationTypes, Types, isMap, isAscii, isNull, isSet, map_empty_, isEnv, isDefinedVal, isChar, isVec, isType, isList, isNat, isInt, atoms_, integers_, values_, set_, list_, tuple_, atom_, nulltype_, non_null_values_, types_, value_types_, toList, isList, libFromList, listUnites, null) +import Funcons.Operations hiding (Name, Values, ComputationTypes, Types, isMap, isNull, isSet, map_empty_, isEnv, isDefinedVal, isChar, isVec, isType, isList, isNat, isInt, atoms_, integers_, values_, set_, list_, tuple_, atom_, nulltype_, non_null_values_, types_, value_types_, toList, isList, libFromList, listUnites, null) import qualified Data.Char as C import qualified Data.Map as M import qualified Data.Set as S import qualified Data.MultiSet as MS import qualified Data.Vector as V +import Data.Maybe (isJust) import Data.Text (Text) import Data.Ratio @@ -124,12 +125,9 @@ nullaryTypes = [ ("algebraic-datatypes", ADTs) , ("adts" , ADTs) - , ("atoms", Atoms) - , ("empty-type", EmptyType) -- , ("naturals", Naturals) -- , ("nats", Naturals) , ("rationals", Rationals) - , ("unicode-characters", UnicodeCharacters) , ("values", VAL.Values) ] @@ -181,13 +179,7 @@ char_ = FValue . char__ char__ :: Char -> Values -char__ = Char - -ascii_ :: Char -> Funcons -ascii_ = FValue . ascii__ - -ascii__ :: Char -> Values -ascii__ = Ascii +char__ = mk_unicode_characters list__ :: [Values] -> Values list__ = VAL.list @@ -281,14 +273,6 @@ mk_naturals :: Integer -> Values mk_naturals = Nat -mk_unicode_characters :: Char -> Values -mk_unicode_characters c | C.isAscii c = mk_ascii_characters c - | otherwise = Char c - --- TODO: haven't included `basic-characters` in the subtyping heirarchy yet. - -mk_ascii_characters :: Char -> Values -mk_ascii_characters = Ascii -} -- | Returns the /unicode/ representation of an assci value. @@ -337,13 +321,9 @@ -- functions that check simple properties of funcons -- TODO: Some of these are used, and all are exported by Funcons.EDSL -- But are all of them still needed. E.g isId doesn't seem very useful now that ids are just strings. -isAscii (FValue (Ascii _)) = True -isAscii _ = False -isAscii_ (Ascii _) = True -isAscii_ _ = False isString (FValue v) = isString_ v isString _ = False -isChar (FValue (Char _)) = True +isChar (FValue v) = isJust (upcastCharacter v) isChar _ = False isNat (FValue (Int _)) = True isNat _ = False @@ -365,18 +345,14 @@ isType _ = False isVec (FValue (Vector _)) = True isVec _ = False -isCharacter_ (Char _) = True -isCharacter_ (Ascii _) = True -isCharacter_ _ = False +isCharacter_ v = isJust (upcastCharacter v) -integers_,atoms_,values_,unicode_characters_ :: Funcons +integers_,values_ :: Funcons integers_ = type_ Integers -unicode_characters_ = type_ UnicodeCharacters values_ = type_ VAL.Values nulltype_ = type_ NullType vectors_ :: Types -> Funcons vectors_ = type_ . vectors -atoms_ = type_ Atoms -- type environment