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 (Ascii 'b'),FValue (Ascii 'r'),FValue (Ascii 'o'),FValue (Ascii 'k'),FValue (Ascii 'e'),FValue (Ascii 'n')]))]) env + 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 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 (Ascii 'c'),FValue (Ascii 'o'),FValue (Ascii 'n'),FValue (Ascii 't'),FValue (Ascii 'i'),FValue (Ascii 'n'),FValue (Ascii 'u'),FValue (Ascii 'e'),FValue (Ascii 'd')]))]) 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 'e'),FValue (Char 'd')]))]) 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 @@ -9,7 +9,7 @@ entities = [] types = typeEnvFromList - [("continuations",DataTypeMemberss "continuations" [TPVar "T1",TPVar "T2"] [DataTypeMemberConstructor "continuation" [TApp "abstractions" [TSortComputesFrom (TName "null-type") (TVar "T2")]] (Just [TPVar "T1",TPVar "T2"])])] + [("continuations",DataTypeMemberss "continuations" [TPVar "T1",TPVar "T2"] [DataTypeMemberConstructor "continuation" [TApp "abstractions" [TSortComputesFrom (TSeq []) (TVar "T2")]] (Just [TPVar "T1",TPVar "T2"])])] funcons = libFromList [("continuation",StrictFuncon stepContinuation),("hole",NullaryFuncon stepHole),("resume-continuation",StrictFuncon stepResume_continuation),("control",StrictFuncon stepControl),("delimit-current-continuation",NonStrictFuncon stepDelimit_current_continuation),("delimit-cc",NonStrictFuncon stepDelimit_current_continuation),("continuations",StrictFuncon stepContinuations)] @@ -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 (Ascii 'c'),FValue (Ascii 'o'),FValue (Ascii 'n'),FValue (Ascii 't'),FValue (Ascii 'i'),FValue (Ascii 'n'),FValue (Ascii 'u'),FValue (Ascii 'a'),FValue (Ascii 't'),FValue (Ascii 'i'),FValue (Ascii 'o'),FValue (Ascii 'n')])),TVar "_X1"]) 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 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 (Ascii 'f'),FValue (Ascii 'a'),FValue (Ascii 'i'),FValue (Ascii 'l'),FValue (Ascii 'e'),FValue (Ascii 'd')]))]) env + 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 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 (Ascii 'r'),FValue (Ascii 'e'),FValue (Ascii 't'),FValue (Ascii 'u'),FValue (Ascii 'r'),FValue (Ascii 'n'),FValue (Ascii 'e'),FValue (Ascii 'd')])),TVar "_X1"]) 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 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 (Ascii 't'),FValue (Ascii 'h'),FValue (Ascii 'r'),FValue (Ascii 'o'),FValue (Ascii 'w'),FValue (Ascii 'n')])),TVar "_X1"]) 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 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 (Ascii 'i'),FValue (Ascii 'd'),FValue (Ascii 'e'),FValue (Ascii 'n'),FValue (Ascii 't'),FValue (Ascii 'i'),FValue (Ascii 'f'),FValue (Ascii 'i'),FValue (Ascii 'e'),FValue (Ascii 'r'),FValue (Ascii '-'),FValue (Ascii 't'),FValue (Ascii 'a'),FValue (Ascii 'g'),FValue (Ascii 'g'),FValue (Ascii 'e'),FValue (Ascii 'd')])),TVar "_X1",TVar "_X2"]) 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 fresh_identifier_ = FName "fresh-identifier" stepFresh_identifier = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "identifier-tagged" [TFuncon (FValue (ADTVal "list" [FValue (Ascii 'g'),FValue (Ascii 'e'),FValue (Ascii 'n'),FValue (Ascii 'e'),FValue (Ascii 'r'),FValue (Ascii 'a'),FValue (Ascii 't'),FValue (Ascii 'e'),FValue (Ascii 'd')])),TName "fresh-atom"]) env + 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 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 @@ -12,7 +12,7 @@ [("yielding",DataTypeMemberss "yielding" [] [DataTypeMemberConstructor "signal" [] (Just [])])] funcons = libFromList - [("left-to-right",NonStrictFuncon stepLeft_to_right),("l-to-r",NonStrictFuncon stepLeft_to_right),("sequential",NonStrictFuncon stepSequential),("seq",NonStrictFuncon stepSequential),("effect",StrictFuncon stepEffect),("choice",NonStrictFuncon stepChoice),("if-true-else",PartiallyStrictFuncon [Strict,NonStrict,NonStrict] NonStrict stepIf_true_else),("if-else",PartiallyStrictFuncon [Strict,NonStrict,NonStrict] NonStrict stepIf_true_else),("while-true",NonStrictFuncon stepWhile_true),("while",NonStrictFuncon stepWhile_true),("do-while-true",NonStrictFuncon stepDo_while_true),("do-while",NonStrictFuncon stepDo_while_true),("interleave",StrictFuncon stepInterleave),("signal",NullaryFuncon stepSignal),("yield",NullaryFuncon stepYield),("yield-on-value",StrictFuncon stepYield_on_value),("yield-on-abrupt",NonStrictFuncon stepYield_on_abrupt),("yielding",NullaryFuncon stepYielding)] + [("left-to-right",NonStrictFuncon stepLeft_to_right),("l-to-r",NonStrictFuncon stepLeft_to_right),("right-to-left",NonStrictFuncon stepRight_to_left),("r-to-l",NonStrictFuncon stepRight_to_left),("sequential",NonStrictFuncon stepSequential),("seq",NonStrictFuncon stepSequential),("effect",StrictFuncon stepEffect),("choice",NonStrictFuncon stepChoice),("if-true-else",PartiallyStrictFuncon [Strict,NonStrict,NonStrict] NonStrict stepIf_true_else),("if-else",PartiallyStrictFuncon [Strict,NonStrict,NonStrict] NonStrict stepIf_true_else),("while-true",NonStrictFuncon stepWhile_true),("while",NonStrictFuncon stepWhile_true),("do-while-true",NonStrictFuncon stepDo_while_true),("do-while",NonStrictFuncon stepDo_while_true),("interleave",StrictFuncon stepInterleave),("signal",NullaryFuncon stepSignal),("yield",NullaryFuncon stepYield),("yield-on-value",StrictFuncon stepYield_on_value),("yield-on-abrupt",NonStrictFuncon stepYield_on_abrupt),("yielding",NullaryFuncon stepYielding)] left_to_right_ fargs = FApp "left-to-right" (fargs) l_to_r_ fargs = FApp "left-to-right" (fargs) @@ -28,6 +28,20 @@ env <- premise (TVar "Y") [PMetaVar "Y'"] env stepTermTo (TApp "left-to-right" [TVar "V*",TVar "Y'",TVar "Z*"]) env +right_to_left_ fargs = FApp "right-to-left" (fargs) +r_to_l_ fargs = FApp "right-to-left" (fargs) +stepRight_to_left fargs = + evalRules [rewrite1] [step1] + where rewrite1 = do + let env = emptyEnv + env <- fsMatch fargs [PAnnotated (PSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env + rewriteTermTo (TVar "V*") env + step1 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PSeqVar "X*" StarOp,PMetaVar "Y",PAnnotated (PSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env + env <- premise (TVar "Y") [PMetaVar "Y'"] env + stepTermTo (TApp "right-to-left" [TVar "X*",TVar "Y'",TVar "V*"]) env + sequential_ fargs = FApp "sequential" (fargs) seq_ fargs = FApp "sequential" (fargs) stepSequential fargs = @@ -105,7 +119,7 @@ stepSignal = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Ascii 's'),FValue (Ascii 'i'),FValue (Ascii 'g'),FValue (Ascii 'n'),FValue (Ascii 'a'),FValue (Ascii 'l')]))]) env + 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 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 (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 'n'),FValue (Ascii 'k')])),TVar "_X1"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 'n'),FValue (Char 'k')])),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 @@ -12,7 +12,7 @@ [("variables",DataTypeMemberss "variables" [] [DataTypeMemberConstructor "variable" [TName "locations",TName "value-types"] (Just [])]),("vars",DataTypeMemberss "vars" [] [DataTypeMemberConstructor "variable" [TName "locations",TName "value-types"] (Just [])])] funcons = libFromList - [("locations",NullaryFuncon stepLocations),("locs",NullaryFuncon stepLocations),("stores",NullaryFuncon stepStores),("store-clear",NullaryFuncon stepStore_clear),("initialise-storing",NonStrictFuncon stepInitialise_storing),("init-storing",NonStrictFuncon stepInitialise_storing),("variable",StrictFuncon stepVariable),("var",StrictFuncon stepVariable),("allocate-variable",StrictFuncon stepAllocate_variable),("alloc",StrictFuncon stepAllocate_variable),("recycle-variables",StrictFuncon stepRecycle_variables),("recycle",StrictFuncon stepRecycle_variables),("initialise-variable",StrictFuncon stepInitialise_variable),("init",StrictFuncon stepInitialise_variable),("allocate-initialised-variable",PartiallyStrictFuncon [NonStrict,Strict] NonStrict stepAllocate_initialised_variable),("alloc-init",PartiallyStrictFuncon [NonStrict,Strict] NonStrict stepAllocate_initialised_variable),("assign",StrictFuncon stepAssign),("assigned",StrictFuncon stepAssigned),("un-assign",StrictFuncon stepUn_assign),("structural-assign",StrictFuncon stepStructural_assign),("structural-assigned",StrictFuncon stepStructural_assigned),("current-value",StrictFuncon stepStructural_assigned),("variables",NullaryFuncon stepVariables),("vars",NullaryFuncon stepVariables)] + [("locations",NullaryFuncon stepLocations),("locs",NullaryFuncon stepLocations),("stores",NullaryFuncon stepStores),("store-clear",NullaryFuncon stepStore_clear),("initialise-storing",NonStrictFuncon stepInitialise_storing),("init-storing",NonStrictFuncon stepInitialise_storing),("variable",StrictFuncon stepVariable),("var",StrictFuncon stepVariable),("allocate-variable",StrictFuncon stepAllocate_variable),("alloc",StrictFuncon stepAllocate_variable),("recycle-variables",StrictFuncon stepRecycle_variables),("recycle",StrictFuncon stepRecycle_variables),("initialise-variable",StrictFuncon stepInitialise_variable),("init",StrictFuncon stepInitialise_variable),("allocate-initialised-variable",PartiallyStrictFuncon [NonStrict,Strict] NonStrict stepAllocate_initialised_variable),("alloc-init",PartiallyStrictFuncon [NonStrict,Strict] NonStrict stepAllocate_initialised_variable),("assign",StrictFuncon stepAssign),("assigned",StrictFuncon stepAssigned),("current-value",StrictFuncon stepCurrent_value),("un-assign",StrictFuncon stepUn_assign),("structural-assign",StrictFuncon stepStructural_assign),("structural-assigned",StrictFuncon stepStructural_assigned),("variables",NullaryFuncon stepVariables),("vars",NullaryFuncon stepVariables)] locations_ = FName "locations" locs_ = FName "locations" @@ -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 (Ascii 'v'),FValue (Ascii 'a'),FValue (Ascii 'r'),FValue (Ascii 'i'),FValue (Ascii 'a'),FValue (Ascii 'b'),FValue (Ascii 'l'),FValue (Ascii 'e')])),TVar "_X1",TVar "_X2"]) 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 allocate_variable_ fargs = FApp "allocate-variable" (fargs) alloc_ fargs = FApp "allocate-variable" (fargs) @@ -157,6 +157,18 @@ putMutTerm "store" (TVar "Sigma") env stepTermTo (TName "fail") env +current_value_ fargs = FApp "current-value" (fargs) +stepCurrent_value fargs = + evalRules [rewrite1,rewrite2] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "Var") (TName "variables")] env + rewriteTermTo (TApp "assigned" [TVar "Var"]) env + rewrite2 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "U") (TSortComplement (TName "variables"))] env + rewriteTermTo (TVar "U") env + un_assign_ fargs = FApp "un-assign" (fargs) stepUn_assign fargs = evalRules [] [step1,step2] @@ -184,8 +196,10 @@ rewriteTermTo (TApp "assign" [TVar "V1",TVar "V2"]) env 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 "I1") (TFuncon (FValue (ADTVal "list" [FValue (Ascii 'v'),FValue (Ascii 'a'),FValue (Ascii 'r'),FValue (Ascii 'i'),FValue (Ascii 'a'),FValue (Ascii 'b'),FValue (Ascii 'l'),FValue (Ascii 'e')])))) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "datatype-values"),VPAnnotated (VPMetaVar "V2") (TName "datatype-values")] env + env <- sideCondition (SCIsInSort (TVar "V1") (TSortComplement (TName "variables"))) env + env <- sideCondition (SCPatternMatch (TVar "V1") [PADT "datatype-value" [VPAnnotated (VPMetaVar "I1") (TName "identifiers"),VPAnnotated (VPSeqVar "V1*" StarOp) (TSortSeq (TName "values") StarOp)]]) env + env <- sideCondition (SCPatternMatch (TVar "V2") [PADT "datatype-value" [VPAnnotated (VPMetaVar "I2") (TName "identifiers"),VPAnnotated (VPSeqVar "V2*" StarOp) (TSortSeq (TName "values") StarOp)]]) env rewriteTermTo (TApp "sequential" [TApp "check-true" [TApp "is-equal" [TVar "I1",TVar "I2"]],TApp "effect" [TApp "tuple" [TApp "interleave-map" [TApp "structural-assign" [TApp "tuple-elements" [TName "given"]],TApp "tuple-zip" [TApp "tuple" [TVar "V1*"],TApp "tuple" [TVar "V2*"]]]]],TName "null-value"]) env rewrite3 = do let env = emptyEnv @@ -200,11 +214,10 @@ rewrite5 = do let env = emptyEnv env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "values"),VPAnnotated (VPMetaVar "V2") (TName "values")] env - env <- sideCondition (SCIsInSort (TVar "V1") (TSortComplement (TSortUnion (TName "variables") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])))) env + env <- sideCondition (SCIsInSort (TVar "V1") (TSortComplement (TSortUnion (TName "datatype-values") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])))) env rewriteTermTo (TApp "check-true" [TApp "is-equal" [TVar "V1",TVar "V2"]]) env structural_assigned_ fargs = FApp "structural-assigned" (fargs) -current_value_ fargs = FApp "structural-assigned" (fargs) stepStructural_assigned fargs = evalRules [rewrite1,rewrite2,rewrite3,rewrite4] [] where rewrite1 = do @@ -213,8 +226,9 @@ rewriteTermTo (TApp "assigned" [TVar "Var"]) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I") (TName "identifiers"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env - env <- sideCondition (SCInequality (TVar "I") (TFuncon (FValue (ADTVal "list" [FValue (Ascii 'v'),FValue (Ascii 'a'),FValue (Ascii 'r'),FValue (Ascii 'i'),FValue (Ascii 'a'),FValue (Ascii 'b'),FValue (Ascii 'l'),FValue (Ascii 'e')])))) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "datatype-values")] env + env <- sideCondition (SCIsInSort (TVar "V") (TSortComplement (TName "variables"))) env + env <- sideCondition (SCPatternMatch (TVar "V") [PADT "datatype-value" [VPAnnotated (VPMetaVar "I") (TName "identifiers"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]]) env rewriteTermTo (TApp "datatype-value" [TVar "I",TApp "interleave-map" [TApp "structural-assigned" [TName "given"],TVar "V*"]]) env rewrite3 = do let env = emptyEnv @@ -223,7 +237,7 @@ rewrite4 = do let env = emptyEnv env <- vsMatch fargs [VPAnnotated (VPMetaVar "U") (TName "values")] env - env <- sideCondition (SCIsInSort (TVar "U") (TSortComplement (TSortUnion (TName "variables") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])))) env + env <- sideCondition (SCIsInSort (TVar "U") (TSortComplement (TSortUnion (TName "datatype-values") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])))) env rewriteTermTo (TVar "U") env variables_ = FName "variables" diff --git a/cbs/Funcons/Core/Library.hs b/cbs/Funcons/Core/Library.hs --- a/cbs/Funcons/Core/Library.hs +++ b/cbs/Funcons/Core/Library.hs @@ -15,7 +15,7 @@ module Funcons.Core.Computations.Abnormal.Sticking, module Funcons.Core.Computations.Abnormal.Breaking.Breaking, module Funcons.Core.Computations.Abnormal.Continuing.Continuing, - module Funcons.Core.Values.Composite.Maps.Maps, + module Funcons.Core.Values.Composite.ASTs.ASTs, module Funcons.Core.Values.Composite.Records.Records, module Funcons.Core.Values.Composite.Strings.Strings, module Funcons.Core.Values.Composite.References.References, @@ -72,8 +72,8 @@ import qualified Funcons.Core.Computations.Abnormal.Breaking.Breaking import Funcons.Core.Computations.Abnormal.Continuing.Continuing hiding (funcons,types,entities) import qualified Funcons.Core.Computations.Abnormal.Continuing.Continuing -import Funcons.Core.Values.Composite.Maps.Maps hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Maps.Maps +import Funcons.Core.Values.Composite.ASTs.ASTs hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.ASTs.ASTs import Funcons.Core.Values.Composite.Records.Records hiding (funcons,types,entities) import qualified Funcons.Core.Values.Composite.Records.Records import Funcons.Core.Values.Composite.Strings.Strings hiding (funcons,types,entities) @@ -139,7 +139,7 @@ , Funcons.Core.Computations.Abnormal.Sticking.funcons , Funcons.Core.Computations.Abnormal.Breaking.Breaking.funcons , Funcons.Core.Computations.Abnormal.Continuing.Continuing.funcons - , Funcons.Core.Values.Composite.Maps.Maps.funcons + , Funcons.Core.Values.Composite.ASTs.ASTs.funcons , Funcons.Core.Values.Composite.Records.Records.funcons , Funcons.Core.Values.Composite.Strings.Strings.funcons , Funcons.Core.Values.Composite.References.References.funcons @@ -182,7 +182,7 @@ , Funcons.Core.Computations.Abnormal.Sticking.entities , Funcons.Core.Computations.Abnormal.Breaking.Breaking.entities , Funcons.Core.Computations.Abnormal.Continuing.Continuing.entities - , Funcons.Core.Values.Composite.Maps.Maps.entities + , Funcons.Core.Values.Composite.ASTs.ASTs.entities , Funcons.Core.Values.Composite.Records.Records.entities , Funcons.Core.Values.Composite.Strings.Strings.entities , Funcons.Core.Values.Composite.References.References.entities @@ -225,7 +225,7 @@ , Funcons.Core.Computations.Abnormal.Sticking.types , Funcons.Core.Computations.Abnormal.Breaking.Breaking.types , Funcons.Core.Computations.Abnormal.Continuing.Continuing.types - , Funcons.Core.Values.Composite.Maps.Maps.types + , Funcons.Core.Values.Composite.ASTs.ASTs.types , Funcons.Core.Values.Composite.Records.Records.types , Funcons.Core.Values.Composite.Strings.Strings.types , Funcons.Core.Values.Composite.References.References.types 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 (Ascii 'f'),FValue (Ascii 'u'),FValue (Ascii 'n'),FValue (Ascii 'c'),FValue (Ascii 't'),FValue (Ascii 'i'),FValue (Ascii 'o'),FValue (Ascii 'n')])),TVar "_X1"]) 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 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 (Ascii 'a'),FValue (Ascii 'b'),FValue (Ascii 's'),FValue (Ascii 't'),FValue (Ascii 'r'),FValue (Ascii 'a'),FValue (Ascii 'c'),FValue (Ascii 't'),FValue (Ascii 'i'),FValue (Ascii 'o'),FValue (Ascii 'n')])),TVar "_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 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 (Ascii 'p'),FValue (Ascii 'a'),FValue (Ascii 't'),FValue (Ascii 't'),FValue (Ascii 'e'),FValue (Ascii 'r'),FValue (Ascii 'n')])),TVar "_X1"]) 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 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 (Ascii 'p'),FValue (Ascii 'a'),FValue (Ascii 't'),FValue (Ascii 't'),FValue (Ascii 'e'),FValue (Ascii 'r'),FValue (Ascii 'n')])))) 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 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 (Ascii 'p'),FValue (Ascii 'a'),FValue (Ascii 't'),FValue (Ascii 't'),FValue (Ascii 'e'),FValue (Ascii 'r'),FValue (Ascii 'n')])))) 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 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 @@ -9,7 +9,7 @@ entities = [] types = typeEnvFromList - [("thunks",DataTypeMemberss "thunks" [TPVar "T"] [DataTypeMemberConstructor "thunk" [TApp "abstractions" [TSortComputesFrom (TName "null-type") (TVar "T")]] (Just [TPVar "T"])])] + [("thunks",DataTypeMemberss "thunks" [TPVar "T"] [DataTypeMemberConstructor "thunk" [TApp "abstractions" [TSortComputesFrom (TSeq []) (TVar "T")]] (Just [TPVar "T"])])] funcons = libFromList [("thunk",StrictFuncon stepThunk),("force",StrictFuncon stepForce),("thunks",StrictFuncon stepThunks)] @@ -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 (Ascii 't'),FValue (Ascii 'h'),FValue (Ascii 'u'),FValue (Ascii 'n'),FValue (Ascii 'k')])),TVar "_X1"]) 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 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 new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Values/Composite/ASTs/ASTs.hs @@ -0,0 +1,44 @@ +-- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/ASTs/ASTs.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Values.Composite.ASTs.ASTs where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) +entities = [] + +types = typeEnvFromList + [("asts",DataTypeMemberss "asts" [] [DataTypeMemberConstructor "ast-value" [TName "types",TName "values"] (Just []),DataTypeMemberConstructor "ast-term" [TName "tags",TSortSeq (TName "asts") StarOp] (Just [])])] + +funcons = libFromList + [("tags",NullaryFuncon stepTags),("ast-value",StrictFuncon stepAst_value),("ast-term",StrictFuncon stepAst_term),("asts",NullaryFuncon stepAsts)] + +tags_ = FName "tags" +stepTags = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TName "strings") env + +ast_value_ fargs = FApp "ast-value" (fargs) +stepAst_value fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + 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 + +ast_term_ fargs = FApp "ast-term" (fargs) +stepAst_term fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + 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 + +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 (Ascii 'b'),FValue (Ascii 'i'),FValue (Ascii 't'),FValue (Ascii '-'),FValue (Ascii 'v'),FValue (Ascii 'e'),FValue (Ascii 'c'),FValue (Ascii 't'),FValue (Ascii 'o'),FValue (Ascii 'r')])),TVar "_X1*"]) 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 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 (Ascii 'c'),FValue (Ascii 'l'),FValue (Ascii 'a'),FValue (Ascii 's'),FValue (Ascii 's')])),TVar "_X1",TVar "_X2",TVar "_X3*"]) 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 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 (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii 't')])),TVar "_X1*"]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')])),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 (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii '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 (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')]),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 (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii 't')]),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)]] env + 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 rewriteTermTo (TVar "V") 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')])]] env + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')])]] 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 (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii 't')]),VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env + 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 rewriteTermTo (TApp "list" [TVar "V*"]) 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')])]] env + env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Char 'l'),FValue (Char 'i'),FValue (Char 's'),FValue (Char 't')])]] 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 (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii 't')]),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env + 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 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 (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii 't')]),VPAnnotated (VPSeqVar "V1*" StarOp) (TSortSeq (TName "values") StarOp)],PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii 't')]),VPAnnotated (VPSeqVar "V2*" StarOp) (TSortSeq (TName "values") StarOp)]] env + 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 rewriteTermTo (TApp "list" [TVar "V1*",TVar "V2*"]) env rewrite2 = do let env = emptyEnv diff --git a/cbs/Funcons/Core/Values/Composite/Maps/Maps.hs b/cbs/Funcons/Core/Values/Composite/Maps/Maps.hs deleted file mode 100644 --- a/cbs/Funcons/Core/Values/Composite/Maps/Maps.hs +++ /dev/null @@ -1,24 +0,0 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Maps/Maps.cbs -{-# LANGUAGE OverloadedStrings #-} - -module Funcons.Core.Values.Composite.Maps.Maps where - -import Funcons.EDSL - -import Funcons.Operations hiding (Values,libFromList) -entities = [] - -types = typeEnvFromList - [("no-values",DataTypeMemberss "no-values" [] [DataTypeMemberConstructor "no-value" [] (Just [])])] - -funcons = libFromList - [("no-value",NullaryFuncon stepNo_value),("no-values",NullaryFuncon stepNo_values)] - -no_value_ = FName "no-value" -stepNo_value = evalRules [rewrite1] [] - where rewrite1 = do - let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Ascii 'n'),FValue (Ascii 'o'),FValue (Ascii '-'),FValue (Ascii 'v'),FValue (Ascii 'a'),FValue (Ascii 'l'),FValue (Ascii 'u'),FValue (Ascii 'e')]))]) env - -no_values_ = FName "no-values" -stepNo_values = rewriteType "no-values" [] 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 (Ascii 'o'),FValue (Ascii 'b'),FValue (Ascii 'j'),FValue (Ascii 'e'),FValue (Ascii 'c'),FValue (Ascii 't')])),TVar "_X1",TVar "_X2",TVar "_X3",TVar "_X4*"]) 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 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 (Ascii 'r'),FValue (Ascii 'e'),FValue (Ascii 'c'),FValue (Ascii 'o'),FValue (Ascii 'r'),FValue (Ascii 'd')])),TVar "_X1"]) 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 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 (Ascii 'r'),FValue (Ascii 'e'),FValue (Ascii 'f'),FValue (Ascii 'e'),FValue (Ascii 'r'),FValue (Ascii 'e'),FValue (Ascii 'n'),FValue (Ascii 'c'),FValue (Ascii 'e')])),TVar "_X1"]) 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 pointer_null_ = FName "pointer-null" stepPointer_null = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Ascii 'p'),FValue (Ascii 'o'),FValue (Ascii 'i'),FValue (Ascii 'n'),FValue (Ascii 't'),FValue (Ascii 'e'),FValue (Ascii 'r'),FValue (Ascii '-'),FValue (Ascii 'n'),FValue (Ascii 'u'),FValue (Ascii 'l'),FValue (Ascii 'l')]))]) env + 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 dereference_ fargs = FApp "dereference" (fargs) stepDereference fargs = diff --git a/cbs/Funcons/Core/Values/Composite/Sequences/Sequences.hs b/cbs/Funcons/Core/Values/Composite/Sequences/Sequences.hs --- a/cbs/Funcons/Core/Values/Composite/Sequences/Sequences.hs +++ b/cbs/Funcons/Core/Values/Composite/Sequences/Sequences.hs @@ -43,7 +43,7 @@ evalRules [rewrite1,rewrite2,rewrite3,rewrite4] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPLit (Nat 1),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)] env + env <- vsMatch fargs [VPLit (Nat 1),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env rewriteTermTo (TVar "V") env rewrite2 = do let env = emptyEnv @@ -52,7 +52,7 @@ rewriteTermTo (TApp "index" [TVar "N'",TVar "V*"]) env rewrite3 = do let env = emptyEnv - env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)] env + env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env rewriteTermTo (TSeq []) env rewrite4 = do let env = emptyEnv @@ -64,7 +64,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env rewriteTermTo (TVar "V") env second_ fargs = FApp "second" (fargs) @@ -72,7 +72,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)] env + env <- vsMatch fargs [VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env rewriteTermTo (TVar "V") env third_ fargs = FApp "third" (fargs) @@ -80,7 +80,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated VPWildCard (TName "values"),VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)] env + env <- vsMatch fargs [VPAnnotated VPWildCard (TName "values"),VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env rewriteTermTo (TVar "V") env first_n_ fargs = FApp "first-n" (fargs) @@ -88,13 +88,13 @@ evalRules [rewrite1,rewrite2,rewrite3] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)] env + env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env rewriteTermTo (TSeq []) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "positive-integers"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp),VPAnnotated VPWildCard (TName "values")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "positive-integers"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env env <- sideCondition (SCPatternMatch (TApp "natural-predecessor" [TVar "N"]) [VPMetaVar "N'"]) env - rewriteTermTo (TApp "first-n" [TVar "N'",TVar "V*"]) env + rewriteTermTo (TSeq [TVar "V",TApp "first-n" [TVar "N'",TVar "V*"]]) env rewrite3 = do let env = emptyEnv env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "positive-integers")] env 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 (Ascii 't'),FValue (Ascii 'r'),FValue (Ascii 'e'),FValue (Ascii 'e')])),TVar "_X1",TVar "_X2*"]) 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 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 (Ascii 't'),FValue (Ascii 'u'),FValue (Ascii 'p'),FValue (Ascii 'l'),FValue (Ascii 'e')])),TVar "_X1*"]) 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 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 (Ascii 'v'),FValue (Ascii 'a'),FValue (Ascii 'r'),FValue (Ascii 'i'),FValue (Ascii 'a'),FValue (Ascii 'n'),FValue (Ascii 't')])),TVar "_X1",TVar "_X2"]) 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 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 (Ascii 'v'),FValue (Ascii 'e'),FValue (Ascii 'c'),FValue (Ascii 't'),FValue (Ascii 'o'),FValue (Ascii 'r')])),TVar "_X1*"]) 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 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 (Ascii 't'),FValue (Ascii 'r'),FValue (Ascii 'u'),FValue (Ascii 'e')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 't'),FValue (Char 'r'),FValue (Char 'u'),FValue (Char 'e')]))]) env false_ = FName "false" stepFalse = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Ascii 'f'),FValue (Ascii 'a'),FValue (Ascii 'l'),FValue (Ascii 's'),FValue (Ascii 'e')]))]) env + rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Char 'f'),FValue (Char 'a'),FValue (Char 'l'),FValue (Char 's'),FValue (Char 'e')]))]) 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 @@ -12,7 +12,7 @@ [] 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",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),("ascii-char",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) @@ -36,20 +36,21 @@ 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) +ascii_char_ 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 + 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 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 <- 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 <- 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 (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii 't')]),VPAnnotated (VPSeqVar "C*" StarOp) (TSortSeq (TName "characters") StarOp)]] env + 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 <- sideCondition (SCInequality (TApp "length" [TVar "C*"]) (TFuncon (FValue (Nat 1)))) env rewriteTermTo (TSeq []) env @@ -57,46 +58,46 @@ 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 + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Char '0'),FValue (Char '0'),FValue (Char '0'),FValue (Char '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 + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Char '0'),FValue (Char '0'),FValue (Char '0'),FValue (Char '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 + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Char '0'),FValue (Char '0'),FValue (Char '0'),FValue (Char '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 + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Char '0'),FValue (Char '0'),FValue (Char '0'),FValue (Char '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 + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Char '0'),FValue (Char '0'),FValue (Char '0'),FValue (Char '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 + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Char '0'),FValue (Char '0'),FValue (Char '2'),FValue (Char '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 + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Char '0'),FValue (Char '0'),FValue (Char '2'),FValue (Char '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 + rewriteTermTo (TApp "unicode-character" [TApp "hexadecimal-natural" [TFuncon (FValue (ADTVal "list" [FValue (Char '0'),FValue (Char '0'),FValue (Char '5'),FValue (Char 'c')]))]]) 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 (Ascii 'b'),FValue (Ascii 'i'),FValue (Ascii 'n'),FValue (Ascii 'a'),FValue (Ascii 'r'),FValue (Ascii 'y'),FValue (Ascii '3'),FValue (Ascii '2')]))]) env + 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 binary64_ = FName "binary64" stepBinary64 = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Ascii 'b'),FValue (Ascii 'i'),FValue (Ascii 'n'),FValue (Ascii 'a'),FValue (Ascii 'r'),FValue (Ascii 'y'),FValue (Ascii '6'),FValue (Ascii '4')]))]) env + 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 binary128_ = FName "binary128" stepBinary128 = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Ascii 'b'),FValue (Ascii 'i'),FValue (Ascii 'n'),FValue (Ascii 'a'),FValue (Ascii 'r'),FValue (Ascii 'y'),FValue (Ascii '1'),FValue (Ascii '2'),FValue (Ascii '8')]))]) env + 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 decimal64_ = FName "decimal64" stepDecimal64 = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Ascii 'd'),FValue (Ascii 'e'),FValue (Ascii 'c'),FValue (Ascii 'i'),FValue (Ascii 'm'),FValue (Ascii 'a'),FValue (Ascii 'l'),FValue (Ascii '6'),FValue (Ascii '4')]))]) env + 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 decimal128_ = FName "decimal128" stepDecimal128 = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "datatype-value" [TFuncon (FValue (ADTVal "list" [FValue (Ascii 'd'),FValue (Ascii 'e'),FValue (Ascii 'c'),FValue (Ascii 'i'),FValue (Ascii 'm'),FValue (Ascii 'a'),FValue (Ascii 'l'),FValue (Ascii '1'),FValue (Ascii '2'),FValue (Ascii '8')]))]) env + 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 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 (Ascii 'n'),FValue (Ascii 'u'),FValue (Ascii 'l'),FValue (Ascii 'l'),FValue (Ascii '-'),FValue (Ascii 'v'),FValue (Ascii 'a'),FValue (Ascii 'l'),FValue (Ascii 'u'),FValue (Ascii 'e')]))]) env + 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 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.5 +version: 0.2.0.7 synopsis: A modular interpreter for executing funcons description: The PLanCompS project () has developed a component-based approach to formal semantics. @@ -43,20 +43,20 @@ , Funcons.Parser , Funcons.GLLParser , Funcons.RunOptions - build-depends: base >=4.3 && <= 5 - ,text - ,containers - ,vector>=0.12.0.0 + build-depends: base >=4.8 && <= 5 + ,text >= 1.2 && <1.3 + ,containers >= 0.5 && < 0.6 + ,vector>=0.12 ,bv >= 0.5 - ,multiset + ,multiset >= 0.3 && < 0.4 ,split ,directory - ,mtl >= 2.0 - ,gll >= 0.4.0.2 + ,mtl >= 2.2.1 + ,gll >= 0.4.0.9 ,TypeCompose>=0.9.10 ,regex-applicative ,random-strings - ,funcons-values >= 0.1.0.3 + ,funcons-values >= 0.1.0.5 hs-source-dirs: src, cbs, manual default-language: Haskell2010 other-extensions: OverloadedStrings @@ -90,6 +90,7 @@ Funcons.Core.Computations.Abnormal.Controlling.Controlling, Funcons.Core.Values.ValueTypes.ValueTypes, -- Funcons.Core.Values.Composite.Sets, + Funcons.Core.Values.Composite.ASTs.ASTs, Funcons.Core.Values.Composite.Bits.Bits, Funcons.Core.Values.Composite.Classes.Classes, Funcons.Core.Values.Composite.Objects.Objects, @@ -101,7 +102,6 @@ Funcons.Core.Values.Composite.Sequences.Sequences, Funcons.Core.Values.Composite.Variants.Variants, Funcons.Core.Values.Composite.Records.Records, - Funcons.Core.Values.Composite.Maps.Maps, Funcons.Core.Values.Composite.Vectors.Vectors, Funcons.Core.Values.Composite.Tuples.Tuples, Funcons.Core.Values.Composite.References.References, @@ -117,6 +117,7 @@ Funcons.Core.Values.Abstraction.Thunks.Thunks -- manual , Funcons.Core.Computations.Normal.GeneratingBuiltin + , Funcons.Core.Computations.AbnormalBuiltin , Funcons.Core.Values.Composite.SetsBuiltin , Funcons.Core.Values.Composite.MultisetsBuiltin -- , Funcons.Core.Values.Composite.ListsBuiltin @@ -137,21 +138,21 @@ executable runfct main-is: Main.hs other-extensions: OverloadedStrings - build-depends: base >=4.3 && <= 5 - ,text - ,containers - ,vector + build-depends: base >=4.8 && <= 5 + ,text >= 1.2 && <1.3 + ,containers >= 0.5 && < 0.6 + ,vector>=0.12 ,bv >= 0.5 ,funcons-tools - ,multiset + ,multiset >= 0.3 && < 0.4 ,split ,directory - ,mtl >= 2.0 - ,gll >= 0.4.0.2 + ,mtl >= 2.2.1 + ,gll >= 0.4.0.9 ,TypeCompose>=0.9.10 ,regex-applicative ,random-strings - ,funcons-values + ,funcons-values >= 0.1.0.4 hs-source-dirs: src, manual, cbs default-language: Haskell2010 -- ghc-options: -rtsopts diff --git a/manual/Funcons/Core/Computations/AbnormalBuiltin.hs b/manual/Funcons/Core/Computations/AbnormalBuiltin.hs new file mode 100644 --- /dev/null +++ b/manual/Funcons/Core/Computations/AbnormalBuiltin.hs @@ -0,0 +1,73 @@ +-- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Computations/Abnormal/Throwing/Throwing.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Computations.AbnormalBuiltin where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) + +library = libFromList + [("handle-thrown",NonStrictFuncon stepHandle_thrown) + ,("handle-return",NonStrictFuncon stepHandle_return) + ,("else", NonStrictFuncon stepElse) + ] + + +handle_thrown_ fargs = FApp "handle-thrown" (fargs) +stepHandle_thrown fargs = + evalRules [rewrite1] [step1] + where rewrite1 = do + let env = emptyEnv + env <- fsMatch fargs [PAnnotated (PMetaVar "V") (TName "values"),PMetaVar "Y"] env + rewriteTermTo (TVar "V") env + step1 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X",PMetaVar "Y"] env + env <- getControlPatt "abrupted" (Nothing) env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) + case __varabrupted of + Nothing -> stepTermTo (TApp "handle-thrown" [TVar "X'",TVar "Y"]) env + Just (ADTVal "thrown" [v]) -> stepTermTo (TApp "give" [TFuncon v, TVar "Y"]) env + Just v -> do raiseSignal "abrupted" v + stepTermTo (TApp "handle-thrown" [TVar "X'",TVar "Y"]) env + +stepHandle_return fargs = + evalRules [rewrite1] [step1] + where rewrite1 = do + let env = emptyEnv + env <- fsMatch fargs [PAnnotated (PMetaVar "V") (TName "values")] env + rewriteTermTo (TVar "V") env + step1 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getControlPatt "abrupted" (Nothing) env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) + case __varabrupted of + Nothing -> stepTermTo (TApp "handle-return" [TVar "X'"]) env + Just (ADTVal "returned" [v]) -> stepTo v + Just v -> do raiseSignal "abrupted" v + stepTermTo (TApp "handle-return" [TVar "X'"]) env + +stepElse fargs = + evalRules [rewrite1,rewrite2] [step1] + where rewrite1 = do + let env = emptyEnv + env <- fsMatch fargs [PAnnotated (PMetaVar "V") (TName "values"),PMetaVar "Y"] env + rewriteTermTo (TVar "V") env + rewrite2 = do + let env = emptyEnv + env <- fsMatch fargs [PMetaVar "X",PMetaVar "Y",PSeqVar "Z+" PlusOp] env + rewriteTermTo (TApp "else" [TVar "X",TApp "else" [TVar "Y",TVar "Z+"]]) env + step1 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X",PMetaVar "Y"] env + env <- getControlPatt "abrupted" (Nothing) env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) + case __varabrupted of + Nothing -> stepTermTo (TApp "else" [TVar "X'",TVar "Y"]) env + Just (ADTVal "failed" _) -> stepTermTo (TVar "Y") env + Just v -> do raiseSignal "abrupted" v + stepTermTo (TApp "else" [TVar "X'",TVar "Y"]) env + + 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 @@ -1,6 +1,7 @@ module Funcons.Core.Manual ( Funcons.Core.Manual.library , module Funcons.Core.Computations.Normal.GeneratingBuiltin + , module Funcons.Core.Computations.AbnormalBuiltin , module Funcons.Core.Values.Composite.SetsBuiltin , module Funcons.Core.Values.Composite.MultisetsBuiltin -- , module Funcons.Core.Values.Composite.ListsBuiltin @@ -35,6 +36,7 @@ --import Funcons.Core.Values.Composite.TuplesBuiltin hiding (library) import qualified Funcons.Core.Computations.Normal.GeneratingBuiltin +import qualified Funcons.Core.Computations.AbnormalBuiltin import qualified Funcons.Core.Values.Composite.SetsBuiltin import qualified Funcons.Core.Values.Composite.MultisetsBuiltin --import qualified Funcons.Core.Values.Composite.ListsBuiltin @@ -55,6 +57,7 @@ library = libUnions [ Funcons.Core.Computations.Normal.GeneratingBuiltin.library +-- , Funcons.Core.Computations.AbnormalBuiltin.library , Funcons.Core.Values.Composite.SetsBuiltin.library , Funcons.Core.Values.Composite.MultisetsBuiltin.library -- , Funcons.Core.Values.Composite.ListsBuiltin.library diff --git a/manual/Funcons/Core/Values/Composite/DatatypesBuiltin.hs b/manual/Funcons/Core/Values/Composite/DatatypesBuiltin.hs --- a/manual/Funcons/Core/Values/Composite/DatatypesBuiltin.hs +++ b/manual/Funcons/Core/Values/Composite/DatatypesBuiltin.hs @@ -23,10 +23,9 @@ evalADT (f:fs) = evalStrictSequence (f:fs) cont adt_val_ where cont [] = error "eval-adt assert" - cont (v:vs) = case v of - ADTVal "list" s | all isAscii s - -> rewritten $ ADTVal (pack (map (\(FValue (Ascii c)) -> c) s)) $ map FValue vs - _ -> sortErr (adt_val_ (map FValue (v:vs))) ("first argument of datatype-value not a string") + cont (v:vs) = if isString_ v + then rewritten $ ADTVal (pack (unString v)) $ map FValue vs + else sortErr (adt_val_ (map FValue (v:vs))) ("first argument of datatype-value not a string") evalADT [] = sortErr (adt_val_ []) "algebraic-datatype not applied to a string and a sequence of fields" @@ -36,17 +35,17 @@ where cont [] = error "lazy-eval-adt assert" cont (v:vs) = case v of - FValue (ADTVal "list" s) | all isAscii s - -> rewritten $ ADTVal (pack (map (\(FValue (Ascii c)) -> c) s)) vs + FValue s | isString_ s + -> rewritten $ ADTVal (pack (unString s)) vs _ -> sortErr (lazy_adt_val_ (v:vs)) ("first argument of value constructor not a string") evalLazyADT [] = sortErr (lazy_adt_val_ []) "value constructor not applied to a string and a sequence of computations" adt_construct_ = applyFuncon "adt-construct" -adtConstruct (v:vs) = case v of - ADTVal "list" s | all isAscii s - -> rewritten $ ADTVal (pack (map (\(FValue (Ascii c)) -> c) s)) $ map FValue vs - _ -> sortErr (adt_val_ (map FValue (v:vs))) ("first argument of adt-construct not a string") +adtConstruct (v:vs) = + if isString_ v + then rewritten $ ADTVal (pack (unString v)) $ map FValue vs + else sortErr (adt_val_ (map FValue (v:vs))) ("first argument of adt-construct not a string") adtConstruct [] = sortErr (adt_val_ []) "adt-construct not applied to a string and a sequence of fields" 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 @@ -37,10 +37,18 @@ , ("is-less-or-equal", fromValOp is_less_or_equal_ VAL.is_less_or_equal_) , ("integers", fromNullaryValOp integers_ VAL.integers_) , ("ints", fromNullaryValOp integers_ VAL.integers_) + , ("integers-from", fromValOp integers_from_ VAL.integers_from_) + , ("from", fromValOp integers_from_ VAL.integers_from_) + , ("integers-up-to", fromValOp integers_up_to_ VAL.integers_up_to_) + , ("up-to", fromValOp integers_up_to_ VAL.integers_up_to_) ] ints_ = integers_ integers_ = applyFuncon "integers" +integers_from_ = applyFuncon "integers-from" +from_ = applyFuncon "from" +integers_up_to_ = applyFuncon "integers-up-to" +up_to_ = applyFuncon "integers-up-to" natural_predecessor_, nat_pred_ :: [Funcons] -> Funcons natural_predecessor_ = applyFuncon "natural-predecessor" nat_pred_ = applyFuncon "nat-pred" diff --git a/manual/Funcons/MetaProgramming.hs b/manual/Funcons/MetaProgramming.hs --- a/manual/Funcons/MetaProgramming.hs +++ b/manual/Funcons/MetaProgramming.hs @@ -12,6 +12,7 @@ import Funcons.RunOptions import Funcons.Simulation +import Data.Maybe (fromJust) import Data.Text (pack, unpack) import qualified Data.Map as M import qualified Data.Set as S @@ -35,6 +36,9 @@ -- FList fs -> FList <$> mapM ctRel fs FSet fs -> FSet <$> mapM ctRel fs FMap fs -> FMap <$> mapM ctRel fs + FValue (ADTVal nm fs) -> FValue . ADTVal nm <$> mapM ctRel fs + FValue (ComputationType (Type (ADT nm fs))) + -> FValue . ComputationType . Type . ADT nm <$> mapM ctRel fs FValue v -> return (FValue v) _ -> liftRewrite (sortErr f ("ctRel not defined")) where staticEval m = ctRel m >>= evalRel >>= liftRewrite . dlRel @@ -43,14 +47,14 @@ -- Translating a funcon into its meta-representation ulRel :: Funcons -> MSOS Funcons ulRel f = case f of - FName nm -> return $ ast_ [string_ (unpack nm)] + FName nm -> return $ ast_term [string_ (unpack nm)] FApp "meta-down" [f] -> ctRel f FApp "meta-up" [m] -> ulRel m >>= ulRel - FApp nm fs -> ast_ . (string_ (unpack nm):) <$> mapM ulRel fs --- FList fs -> ast_ . (string_ "list":) <$> mapM ulRel fs - FSet fs -> ast_ . (string_ "set":) <$> mapM ulRel fs - FMap fs -> ast_ . (string_ "map":) <$> mapM ulRel fs - FValue v -> return $ ast_ [type_ (tyOf v), FValue v] + FApp nm fs -> ast_term . (string_ (unpack nm):) <$> mapM ulRel fs +-- FList fs -> ast_term . (string_ "list":) <$> mapM ulRel fs + FSet fs -> ast_term . (string_ "set":) <$> mapM ulRel fs + FMap fs -> ast_term . (string_ "map":) <$> mapM ulRel fs + FValue v -> return $ ast_value [type_ (tyOf v), FValue v] -- What TODO with type annotations? _ -> liftRewrite (sortErr f ("ulRel not defined")) @@ -58,16 +62,19 @@ -- Translating a meta-representation of a program into the actual program dlRel :: Values -> Rewrite Funcons dlRel v = case v of - VMeta tag -> dlRel' tag - _ -> sortErr (meta_down_ (fvalues [v])) "meta-down not applied to a meta-representation" - where - dlRel' :: TaggedSyntax -> Rewrite Funcons - dlRel' t = case t of - TagType ty lit -> return (FValue lit) - TagName nm [] -> return $ FName nm - TagName "set" vs -> FSet <$> mapM dlRel vs - TagName "map" vs -> FMap <$> mapM dlRel vs - TagName nm vs -> FApp nm <$> mapM dlRel vs + ADTVal "ast-value" [t,v] | Just (ComputationType _) <- project t -> return v + ADTVal "ast-term" [nm] | isString nm -> return (FName (pack (unString (fromJust (project nm))))) + ADTVal "ast-term" (s:vs') + | Just vs <- mapM project vs' + , isString s, "set" <- unString (fromJust (project s)) -> FSet <$> mapM dlRel vs + ADTVal "ast-term" (m:vs') + | Just vs <- mapM project vs' + , isString m, "map" <- unString (fromJust (project m)) -> FMap <$> mapM dlRel vs + ADTVal "ast-term" (nm:vs') + | Just vs <- mapM project vs' + , isString nm -> FApp (pack (unString (fromJust (project nm)))) <$> + mapM dlRel vs + _ -> sortErr (meta_down_ (fvalues [v])) "meta-down not applied to a meta-representation" evalRel :: Funcons -> MSOS Values evalRel f = evalFuncons f >>= \case @@ -106,7 +113,6 @@ -- , ("meta-down", StrictFuncon step_meta_down) -- static funcon ("eval", StrictFuncon step_meta_eval) , ("code", NonStrictFuncon step_code) - , ("ast", StrictFuncon step_ast) , ("type-of", StrictFuncon step_ty_of) ] @@ -124,16 +130,8 @@ step_code [f] = compstep (toStepRes <$> ulRel f) step_code fs = sortErr (code_ fs) "code not applied to a single term" -ast_ = applyFuncon "ast" -step_ast :: [Values] -> Rewrite Rewritten -step_ast vs@(s:args) | isString_ s = - Funcons.Patterns.isInTupleType args [(ASTs, Just StarOp)] >>= \case - True -> rewriteTo $ FValue $ VMeta (TagName (pack (unString s)) args) - False -> sortErr (ast_ (fvalues vs)) "'ast' is not applied to a string and a sequence of meta-representations" -step_ast vs@[ComputationType (Type ty), v] = Funcons.Patterns.isInType v ty >>= \case - True -> rewriteTo $ FValue $ VMeta (TagType ty v) - False -> sortErr (ast_ (fvalues vs)) "type-checking failed during evaluation of 'ast'" -step_ast vs = sortErr (ast_ (fvalues vs)) "'ast' is not applied to a string or not to a type and a member of that type" +ast_term = applyFuncon "ast-term" +ast_value = applyFuncon "ast-value" type_of_ = applyFuncon "type-of" step_ty_of :: [Values] -> Rewrite Rewritten diff --git a/src/Funcons/Core.hs b/src/Funcons/Core.hs --- a/src/Funcons/Core.hs +++ b/src/Funcons/Core.hs @@ -20,7 +20,7 @@ module Funcons.Core.Manual) where import Funcons.Types hiding (set_) -- Haddock dependency -import Funcons.Core.Library +import Funcons.Core.Library import Funcons.Core.Manual hiding (unicode_, ascii_character_) diff --git a/src/Funcons/EDSL.hs b/src/Funcons/EDSL.hs --- a/src/Funcons/EDSL.hs +++ b/src/Funcons/EDSL.hs @@ -6,16 +6,16 @@ -- Module "Funcons.Tools" provides functions for creating executables. module Funcons.EDSL ( -- * Funcon representation - Funcons(..), Values(..), Types(..), ComputationTypes(..),SeqSortOp(..),TaggedSyntax(..), + Funcons(..), Values(..), Types(..), ComputationTypes(..),SeqSortOp(..), applyFuncon, -- ** Smart construction of funcon terms app0_, app1_, app2_, app3_, -- *** Funcon terms - tuple_, list_, set_, map_, vec_, env_fromlist_, null__, + set_, vec_, env_fromlist_, null__, -- *** Values - int_, nat_, float_, ieee_float_32_, ieee_float_64_, string_, string__, atom_, + int_, bool_, bool__, list__, vector__, tuple__, ascii_, ascii__,char_, char__, nat_, float_, ieee_float_32_, ieee_float_64_, string_, string__, atom_, -- *** Types - values_, integers_, atoms_, unicode_characters_, vectors_, type_, + values_, integers_, atoms_, unicode_characters_, 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? @@ -174,7 +174,18 @@ app3_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons -> Funcons -> Funcons app3_ cons x y z = cons [x,y,z] - + + +ty_star,ty_opt,ty_plus,ty_neg :: Funcons -> Funcons +ty_star = flip FSortSeq StarOp +ty_opt = flip FSortSeq QuestionMarkOp +ty_plus = flip FSortSeq PlusOp +ty_neg = FSortComplement + +ty_inter,ty_union,ty_power :: Funcons -> Funcons -> Funcons +ty_inter = FSortInter +ty_union = FSortUnion +ty_power = FSortPower -- $cbsintro -- This section describes functions that extend the interpreter with diff --git a/src/Funcons/MSOS.hs b/src/Funcons/MSOS.hs --- a/src/Funcons/MSOS.hs +++ b/src/Funcons/MSOS.hs @@ -83,11 +83,10 @@ Error _ (ProjErr str) -> sortErr f str Error _ (Normal (FValue v)) -> rewritten' v Error _ (Normal t) -> rewriteFuncons t - Success (FValue (ADTVal "no-value" _)) -> rewrittens [] Success (FValue (ADTVal "null" _)) -> rewrittens [] Success (FValue v) -> rewritten' v Success t -> rewriteFuncons t - where rewritten' v | seqRes, ADTVal "list" fs <- v, + where rewritten' v | seqRes, ValSeq fs <- v, let mvs = map project fs, all isJust mvs = rewrittens (map fromJust mvs) | otherwise = rewritten v @@ -766,6 +765,8 @@ do mystepf <- lookupFuncon nm case mystepf of NullaryFuncon mystep -> mystep + StrictFuncon _ -> rewriteFuncons' (FApp nm []) + ValueOp _ -> rewriteFuncons' (FApp nm []) _ -> error ("funcon " ++ unpack nm ++ " not applied to any arguments") rewriteFuncons' (FApp nm arg) = do mystepf <- lookupFuncon nm diff --git a/src/Funcons/Patterns.hs b/src/Funcons/Patterns.hs --- a/src/Funcons/Patterns.hs +++ b/src/Funcons/Patterns.hs @@ -9,6 +9,7 @@ import Funcons.Types import Funcons.Substitution import Funcons.Exceptions +import Funcons.Operations (isGround) import Control.Applicative import Control.Monad (foldM, forM) @@ -41,7 +42,7 @@ StarOp -> makeResults (const True) where makeResults filter_op = do furthest <- takeWhileM (\a -> p a mty env) (drop k str) - return (map ins (filter filter_op $ ordered_subsequences furthest)) + return (sortWithPref $ map ins (filter filter_op $ ordered_subsequences furthest)) where ins fs = (k+length fs, envInsert var (level (concat fs)) env) @@ -53,35 +54,30 @@ Left ie | failsRule ie -> return [] | otherwise -> rewrite_rethrow ie + -- sorts the result in order of preference + sortWithPref :: [(Int, Env)] -> [(Int, Env)] + sortWithPref = sortBy (comparison `on` fst) + where comparison = case mty of + Nothing -> compare -- no annotation => shortest match + Just _ -> flip compare -- annoration => longest match + matching :: (a -> String) -> [a] -> [Matcher a] -> Env -> Rewrite Env matching show str ps env = do - matches <- (seqms ps) str 0 env + matches <- foldr seqWith lastMatcher ps str 0 env let rule_fail = PatternMismatch ("Pattern match failed: " ++ intercalate "," (map show str)) case matches of [] -> rewrite_throw rule_fail [(_,env')] -> return env' _ -> internal ("ambiguity not resolved") where m = length str - - seqms :: [Matcher a] -> Matcher a - seqms = foldr seqlongest lastMatcher - -- sequencing of matchers specifically to disambiguate safely lastMatcher :: Matcher a lastMatcher _ k env | k == m = return [(k,env)] | otherwise = return [] - seqlongest :: Matcher a -> Matcher a -> Matcher a - seqlongest p q str k env = do - matches <- p str k env - -- implement `longest match' such that it always returns at least one - -- pattern match (if at least one exists). - -- (in combination with (`seqm` lastMatcher) it will always - -- produce exactly one match) - -- Strategy: try all `pivots' from largest to smallest and `use' - -- the first that does not yield an empty result list - foldM tryLargest [] (sortBy (((flip compare) `on` fst)) matches) - where tryLargest acc (r, env) + seqWith :: Matcher a -> Matcher a -> Matcher a + seqWith p q str k env = p str k env >>= foldM acceptFirst [] + where acceptFirst acc (r, env) | null acc = q str r env | otherwise = return acc @@ -424,9 +420,10 @@ isInTuple vs mtys = case sequence (map castType mtys) of Nothing -> sortErr (FValue $ ADTVal "" (map FValue mtys)) "rhs of annotation is not a type" - Just tys -> Funcons.Patterns.isInTupleType vs (map mkParam tys) - where mkParam (AnnotatedType ty op) = (ty, Just op) - mkParam ty = (ty, Nothing) + Just tys -> Funcons.Patterns.isInTupleType vs (map paramFromType tys) + +paramFromType (AnnotatedType ty op) = (ty, Just op) +paramFromType ty = (ty, Nothing) isIn :: Values -> Values -> Rewrite Bool isIn v mty = case castType mty of @@ -434,13 +431,14 @@ Just ty -> Funcons.Patterns.isInType v ty isInType :: Values -> Types -> Rewrite Bool +isInType v (ADT "ground-values" []) = return (isGround v) isInType v (ADT "maps" [kt', vt']) = case v of Map m -> do kt <- rewritesToType kt' vt <- rewritesToType vt' and <$> sequence [and <$> mapM (flip Funcons.Patterns.isInType kt) (M.keys m) - ,and <$> mapM (flip Funcons.Patterns.isInType vt) (concat $ M.elems m)] + ,and <$> mapM (flip Funcons.Patterns.isInTupleType [paramFromType vt]) (M.elems m)] _ -> return False isInType v (ADT "multisets" [ty']) = case v of Multiset ls -> do diff --git a/src/Funcons/Substitution.hs b/src/Funcons/Substitution.hs --- a/src/Funcons/Substitution.hs +++ b/src/Funcons/Substitution.hs @@ -144,6 +144,9 @@ substitute (TSortSeq t1 op) env = flip FSortSeq op <$> substitute t1 env substitute (TSortPower t1 t2) env = FSortPower <$> substitute t1 env <*> substitute t2 env substitute (TSortComputes t1) env = FSortComputes <$> substitute t1 env +-- special case for thunks/continuations +substitute (TSortComputesFrom (TSeq []) t2) env = + FSortComputesFrom nulltype_ <$> substitute t2 env substitute (TSortComputesFrom t1 t2) env = FSortComputesFrom <$> substitute t1 env <*> substitute t2 env substitute TAny env = internal "missing substitution (wildcard)" diff --git a/src/Funcons/Tools.hs b/src/Funcons/Tools.hs --- a/src/Funcons/Tools.hs +++ b/src/Funcons/Tools.hs @@ -107,9 +107,9 @@ runWithExtensionsNoCore :: FunconLibrary -> EntityDefaults -> TypeRelation -> [String] -> Maybe Funcons -> IO () runWithExtensionsNoCore lib defaults tyenv = runWithExtensionsNoNothing full_lib defaults tyenv - where full_lib = libUnions [lib - ,Funcons.EDSL.library - ,Funcons.Core.Manual.library] + where full_lib = libUnions [lib + ,Funcons.EDSL.library + ,Funcons.Core.Manual.library] -- | Same as 'run', except receiving additional interpreter extensions as arguments. -- Useful when a translation to 'Funcons' has been implemented in Haskell as diff --git a/src/Funcons/Types.hs b/src/Funcons/Types.hs --- a/src/Funcons/Types.hs +++ b/src/Funcons/Types.hs @@ -5,7 +5,7 @@ module VAL,) where import qualified Funcons.Operations as VAL hiding (SortErr, ValueOp) -import Funcons.Operations hiding (Name, Values, ComputationTypes, TaggedSyntax, Types, isMap, isAscii, isNull, isSet, map_empty_, isEnv, isDefinedVal, isString_, 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, 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 qualified Data.Char as C import qualified Data.Map as M @@ -91,7 +91,6 @@ type Values = VAL.Values Funcons -type TaggedSyntax = VAL.TaggedSyntax Funcons instance HasValues Funcons where inject = FValue @@ -125,7 +124,6 @@ nullaryTypes = [ ("algebraic-datatypes", ADTs) , ("adts" , ADTs) - , ("non-grounded-values", Complement GroundValues) , ("atoms", Atoms) , ("empty-type", EmptyType) -- , ("naturals", Naturals) @@ -147,11 +145,7 @@ [] boundedIntegerTypes :: [(Name, Integer -> Types)] -boundedIntegerTypes = [("integers-from", IntegersFrom) - ,("from", IntegersFrom) - ,("integers-up-to", IntegersUpTo) - ,("up-to", IntegersUpTo) - ] +boundedIntegerTypes = [] floatTypes :: [(Name, IEEEFormats -> Types)] floatTypes = [("ieee-floats", IEEEFloats)] @@ -167,6 +161,12 @@ nat_ i | i < 0 = int_ i | otherwise = FValue $ mk_naturals $ toInteger i +bool_ :: Bool -> Funcons +bool_ = FValue . bool__ + +bool__ :: Bool -> Values +bool__ = VAL.tobool + -- | Creates an atom from a 'String'. atom_ :: String -> Funcons atom_ = FValue . Atom @@ -175,8 +175,30 @@ string_ :: String -> Funcons string_ = FValue . string__ string__ :: String -> Values -string__ = ADTVal "list" . map (FValue . Ascii) +string__ = ADTVal "list" . map char_ +char_ :: Char -> Funcons +char_ = FValue . char__ + +char__ :: Char -> Values +char__ = Char + +ascii_ :: Char -> Funcons +ascii_ = FValue . ascii__ + +ascii__ :: Char -> Values +ascii__ = Ascii + +list__ :: [Values] -> Values +list__ = VAL.list + +vector__ :: [Values] -> Values +vector__ = VAL.vector + +tuple__ :: [Values] -> Values +tuple__ = VAL.tuple + + float_ :: Double -> Funcons float_ = FValue . Float @@ -319,10 +341,8 @@ isAscii _ = False isAscii_ (Ascii _) = True isAscii_ _ = False -isString (FValue (ADTVal "list" s)) = all isAscii s +isString (FValue v) = isString_ v isString _ = False -isString_ (ADTVal "list" s) = all isAscii s -isString_ _ = False isChar (FValue (Char _)) = True isChar _ = False isNat (FValue (Int _)) = True