diff --git a/cbs/Funcons/Core/Computations/Abnormal/Abrupting/Abrupting.hs b/cbs/Funcons/Core/Computations/Abnormal/Abrupting/Abrupting.hs --- a/cbs/Funcons/Core/Computations/Abnormal/Abrupting/Abrupting.hs +++ b/cbs/Funcons/Core/Computations/Abnormal/Abrupting/Abrupting.hs @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -20,14 +20,14 @@ where rewrite1 = do let env = emptyEnv env <- fsMatch fargs [PMetaVar "X"] env - rewriteTermTo (TApp "handle-abrupt" [TVar "X",TName "none"]) env + rewriteTermTo (TApp "handle-abrupt" [TVar "X",TName "null-value"]) env abrupt_ fargs = FApp "abrupt" (fargs) stepAbrupt fargs = evalRules [] [step1] where step1 = do let env = emptyEnv - env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "defined-values")] env + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values")] env env <- getControlPatt "abrupted" (Just (VPMetaVar "V")) env raiseTerm "abrupted" (TVar "V") env stepTermTo (TName "stuck") env @@ -43,15 +43,15 @@ 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)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Nothing) env stepTermTo (TApp "handle-abrupt" [TVar "X'",TVar "Y"]) env step2 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X",PMetaVar "Y"] env env <- getControlPatt "abrupted" (Nothing) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V")) env (premise (TVar "X") (PMetaVar "X'") env)) - env <- receiveSignalPatt __varabrupted (Just (VPAnnotated (VPMetaVar "V") (TName "defined-values"))) env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V")) env (premise (TVar "X") [PMetaVar "X'"] env)) + env <- receiveSignalPatt __varabrupted (Just (VPAnnotated (VPMetaVar "V") (TName "values"))) env stepTermTo (TApp "give" [TVar "V",TVar "Y"]) env finally_ fargs = FApp "finally" (fargs) @@ -65,13 +65,13 @@ 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)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Nothing) env stepTermTo (TApp "finally" [TVar "X'",TVar "Y"]) env step2 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X",PMetaVar "Y"] env env <- getControlPatt "abrupted" (Nothing) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V")) env (premise (TVar "X") (PMetaVar "X'") env)) - env <- receiveSignalPatt __varabrupted (Just (VPAnnotated (VPMetaVar "V") (TName "defined-values"))) env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V")) env (premise (TVar "X") [PMetaVar "X'"] env)) + env <- receiveSignalPatt __varabrupted (Just (VPAnnotated (VPMetaVar "V") (TName "values"))) env stepTermTo (TApp "sequential" [TVar "Y",TApp "abrupt" [TVar "V"]]) env 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 @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -39,27 +39,27 @@ evalRules [rewrite1] [step1,step2,step3] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PValue (PADT "none" [])] env - rewriteTermTo (TName "none") env + env <- fsMatch fargs [PValue (PADT "null-value" [])] env + rewriteTermTo (TName "null-value") 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)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Nothing) env stepTermTo (TApp "handle-break" [TVar "X'"]) env step2 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X"] env env <- getControlPatt "abrupted" (Nothing) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TName "broken")) env (premise (TVar "X") (PWildCard) env)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TName "broken")) env (premise (TVar "X") [PWildCard] env)) env <- receiveSignalPatt __varabrupted (Just (PADT "broken" [])) env - stepTermTo (TName "none") env + stepTermTo (TName "null-value") env step3 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X"] env env <- getControlPatt "abrupted" (Just (VPMetaVar "V")) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V")) env (premise (TVar "X") (PMetaVar "X'") env)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V")) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Just (VPAnnotated (VPMetaVar "V") (TSortComplement (TName "breaking")))) env raiseTerm "abrupted" (TVar "V") env stepTermTo (TApp "handle-break" [TVar "X'"]) env 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 @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -39,27 +39,27 @@ evalRules [rewrite1] [step1,step2,step3] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PValue (PADT "none" [])] env - rewriteTermTo (TName "none") env + env <- fsMatch fargs [PValue (PADT "null-value" [])] env + rewriteTermTo (TName "null-value") 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)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Nothing) env stepTermTo (TApp "handle-continue" [TVar "X'"]) env step2 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X"] env env <- getControlPatt "abrupted" (Nothing) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TName "continued")) env (premise (TVar "X") (PWildCard) env)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TName "continued")) env (premise (TVar "X") [PWildCard] env)) env <- receiveSignalPatt __varabrupted (Just (PADT "continued" [])) env - stepTermTo (TName "none") env + stepTermTo (TName "null-value") env step3 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X"] env env <- getControlPatt "abrupted" (Just (VPMetaVar "V")) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V")) env (premise (TVar "X") (PMetaVar "X'") env)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V")) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Just (VPAnnotated (VPMetaVar "V") (TSortComplement (TName "continuing")))) env raiseTerm "abrupted" (TVar "V") env stepTermTo (TApp "handle-continue" [TVar "X'"]) env 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 @@ -5,14 +5,14 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList - [("continuations",DataTypeMemberss "continuations" [TPVar "T1",TPVar "T2"] [DataTypeMemberConstructor "continuation" [TApp "abstractions" [TVar "T2"]] (Just [TPVar "T1",TPVar "T2"])])] + [("continuations",DataTypeMemberss "continuations" [TPVar "T1",TPVar "T2"] [DataTypeMemberConstructor "continuation" [TApp "abstractions" [TSortComputesFrom (TName "null-type") (TVar "T2")]] (Just [TPVar "T1",TPVar "T2"])])] funcons = libFromList - [("continuation",StrictFuncon stepContinuation),("hole",NullaryFuncon stepHole),("resume-continuation",StrictFuncon stepResume_continuation),("control",StrictFuncon stepControl),("delimit-continuations",NonStrictFuncon stepDelimit_continuations),("continuations",StrictFuncon stepContinuations)] + [("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)] continuation_ fargs = FApp "continuation" (fargs) stepContinuation fargs = @@ -20,7 +20,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) 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 hole_ = FName "hole" @@ -38,7 +38,7 @@ let env = emptyEnv env <- lifted_vsMatch fargs [PADT "continuation" [PADT "abstraction" [VPMetaVar "X"]],VPAnnotated (VPMetaVar "V") (TName "values")] env env <- getControlPatt "plug-signal" (Nothing) env - (env,[__varplug_signal]) <- receiveSignals ["plug-signal"] (withControlTerm "plug-signal" (Just (TVar "V")) env (premise (TVar "X") (PMetaVar "X'") env)) + (env,[__varplug_signal]) <- receiveSignals ["plug-signal"] (withControlTerm "plug-signal" (Just (TVar "V")) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varplug_signal (Just (VPMetaVar "V")) env stepTermTo (TVar "X'") env @@ -47,13 +47,14 @@ evalRules [] [step1] where step1 = do let env = emptyEnv - env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "F") (TApp "functions" [TApp "continuations" [TName "values",TName "values"],TName "values"])] env + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "F") (TApp "functions" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])] env env <- getControlPatt "control-signal" (Just (VPMetaVar "F")) env raiseTerm "control-signal" (TVar "F") env stepTermTo (TName "hole") env -delimit_continuations_ fargs = FApp "delimit-continuations" (fargs) -stepDelimit_continuations fargs = +delimit_current_continuation_ fargs = FApp "delimit-current-continuation" (fargs) +delimit_cc_ fargs = FApp "delimit-current-continuation" (fargs) +stepDelimit_current_continuation fargs = evalRules [rewrite1] [step1,step2] where rewrite1 = do let env = emptyEnv @@ -61,18 +62,18 @@ rewriteTermTo (TVar "V") env step1 = do let env = emptyEnv - env <- lifted_fsMatch fargs [PMetaVar "E"] env + env <- lifted_fsMatch fargs [PMetaVar "X"] env env <- getControlPatt "control-signal" (Nothing) env - (env,[__varcontrol_signal]) <- receiveSignals ["control-signal"] (withControlTerm "control-signal" (Nothing) env (premise (TVar "E") (PMetaVar "E'") env)) + (env,[__varcontrol_signal]) <- receiveSignals ["control-signal"] (withControlTerm "control-signal" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varcontrol_signal (Nothing) env - stepTermTo (TApp "delimit-continuations" [TVar "E'"]) env + stepTermTo (TApp "delimit-current-continuation" [TVar "X'"]) env step2 = do let env = emptyEnv - env <- lifted_fsMatch fargs [PMetaVar "E"] env + env <- lifted_fsMatch fargs [PMetaVar "X"] env env <- getControlPatt "control-signal" (Nothing) env - (env,[__varcontrol_signal]) <- receiveSignals ["control-signal"] (withControlTerm "control-signal" (Just (TVar "F")) env (premise (TVar "E") (PMetaVar "E'") env)) + (env,[__varcontrol_signal]) <- receiveSignals ["control-signal"] (withControlTerm "control-signal" (Just (TVar "F")) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varcontrol_signal (Just (VPMetaVar "F")) env - stepTermTo (TApp "delimit-continuations" [TApp "apply" [TVar "F",TApp "continuation" [TApp "closure" [TVar "E'"]]]]) env + stepTermTo (TApp "delimit-current-continuation" [TApp "apply" [TVar "F",TApp "continuation" [TApp "closure" [TVar "X'"]]]]) env continuations_ = FApp "continuations" stepContinuations ts = rewriteType "continuations" ts 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 @@ -5,14 +5,14 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList [("failing",DataTypeMemberss "failing" [] [DataTypeMemberConstructor "failed" [] (Just [])])] funcons = libFromList - [("failed",NullaryFuncon stepFailed),("finalise-failing",NonStrictFuncon stepFinalise_failing),("fail",NullaryFuncon stepFail),("else",NonStrictFuncon stepElse),("else-choice",NonStrictFuncon stepElse_choice),("check-true",StrictFuncon stepCheck_true),("check",StrictFuncon stepCheck_true),("defined",StrictFuncon stepDefined),("def",StrictFuncon stepDefined),("failing",NullaryFuncon stepFailing)] + [("failed",NullaryFuncon stepFailed),("finalise-failing",NonStrictFuncon stepFinalise_failing),("fail",NullaryFuncon stepFail),("else",NonStrictFuncon stepElse),("else-choice",NonStrictFuncon stepElse_choice),("check-true",StrictFuncon stepCheck_true),("check",StrictFuncon stepCheck_true),("checked",StrictFuncon stepChecked),("failing",NullaryFuncon stepFailing)] failed_ = FName "failed" stepFailed = evalRules [rewrite1] [] @@ -49,21 +49,21 @@ 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)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Nothing) env stepTermTo (TApp "else" [TVar "X'",TVar "Y"]) env step2 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X",PMetaVar "Y"] env env <- getControlPatt "abrupted" (Nothing) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TName "failed")) env (premise (TVar "X") (PWildCard) env)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TName "failed")) env (premise (TVar "X") [PWildCard] env)) env <- receiveSignalPatt __varabrupted (Just (PADT "failed" [])) env stepTermTo (TVar "Y") env step3 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X",PMetaVar "Y"] env env <- getControlPatt "abrupted" (Just (VPMetaVar "V")) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V")) env (premise (TVar "X") (PMetaVar "X'") env)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V")) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Just (VPAnnotated (VPMetaVar "V") (TSortComplement (TName "failing")))) env raiseTerm "abrupted" (TVar "V") env stepTermTo (TApp "else" [TVar "X'",TVar "Y"]) env @@ -87,23 +87,22 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [PADT "true" []] env - rewriteTermTo (TName "none") env + rewriteTermTo (TName "null-value") env rewrite2 = do let env = emptyEnv env <- vsMatch fargs [PADT "false" []] env rewriteTermTo (TName "fail") env -defined_ fargs = FApp "defined" (fargs) -def_ fargs = FApp "defined" (fargs) -stepDefined fargs = +checked_ fargs = FApp "checked" (fargs) +stepChecked fargs = evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "defined-values")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values")] env rewriteTermTo (TVar "V") env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "none" []] env + env <- vsMatch fargs [] env rewriteTermTo (TName "fail") env failing_ = FName "failing" 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 @@ -5,11 +5,11 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList - [("returning",DataTypeMemberss "returning" [] [DataTypeMemberConstructor "returned" [TName "defined-values"] (Just [])])] + [("returning",DataTypeMemberss "returning" [] [DataTypeMemberConstructor "returned" [TName "values"] (Just [])])] funcons = libFromList [("returned",StrictFuncon stepReturned),("finalise-returning",NonStrictFuncon stepFinalise_returning),("return",StrictFuncon stepReturn),("handle-return",NonStrictFuncon stepHandle_return),("returning",NullaryFuncon stepReturning)] @@ -20,7 +20,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) 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 finalise_returning_ fargs = FApp "finalise-returning" (fargs) @@ -50,21 +50,21 @@ 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)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Nothing) env stepTermTo (TApp "handle-return" [TVar "X'"]) env step2 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X"] env env <- getControlPatt "abrupted" (Nothing) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TApp "returned" [TVar "V"])) env (premise (TVar "X") (PMetaVar "X'") env)) - env <- receiveSignalPatt __varabrupted (Just (PADT "returned" [VPAnnotated (VPMetaVar "V") (TName "defined-values")])) env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TApp "returned" [TVar "V"])) env (premise (TVar "X") [PMetaVar "X'"] env)) + env <- receiveSignalPatt __varabrupted (Just (PADT "returned" [VPAnnotated (VPMetaVar "V") (TName "values")])) env stepTermTo (TVar "V") env step3 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X"] env env <- getControlPatt "abrupted" (Just (VPMetaVar "V'")) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V'")) env (premise (TVar "X") (PMetaVar "X'") env)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V'")) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Just (VPAnnotated (VPMetaVar "V'") (TSortComplement (TName "returning")))) env raiseTerm "abrupted" (TVar "V'") env stepTermTo (TApp "handle-return" [TVar "X'"]) env 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 @@ -5,11 +5,11 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList - [("throwing",DataTypeMemberss "throwing" [] [DataTypeMemberConstructor "thrown" [TName "defined-values"] (Just [])])] + [("throwing",DataTypeMemberss "throwing" [] [DataTypeMemberConstructor "thrown" [TName "values"] (Just [])])] funcons = libFromList [("thrown",StrictFuncon stepThrown),("finalise-throwing",NonStrictFuncon stepFinalise_throwing),("throw",StrictFuncon stepThrow),("handle-thrown",NonStrictFuncon stepHandle_thrown),("handle-recursively",NonStrictFuncon stepHandle_recursively),("catch-else-throw",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepCatch_else_throw),("throwing",NullaryFuncon stepThrowing)] @@ -20,7 +20,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) 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 finalise_throwing_ fargs = FApp "finalise-throwing" (fargs) @@ -36,7 +36,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "defined-values")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values")] env rewriteTermTo (TApp "abrupt" [TApp "thrown" [TVar "V"]]) env handle_thrown_ fargs = FApp "handle-thrown" (fargs) @@ -50,21 +50,21 @@ 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)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Nothing) env stepTermTo (TApp "handle-thrown" [TVar "X'",TVar "Y"]) env step2 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X",PMetaVar "Y"] env env <- getControlPatt "abrupted" (Nothing) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TApp "thrown" [TVar "V"])) env (premise (TVar "X") (PMetaVar "X'") env)) - env <- receiveSignalPatt __varabrupted (Just (PADT "thrown" [VPAnnotated (VPMetaVar "V") (TName "defined-values")])) env - stepTermTo (TApp "give" [TVar "V",TVar "Y"]) env + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TApp "thrown" [TVar "V''"])) env (premise (TVar "X") [PMetaVar "X'"] env)) + env <- receiveSignalPatt __varabrupted (Just (PADT "thrown" [VPAnnotated (VPMetaVar "V''") (TName "values")])) env + stepTermTo (TApp "give" [TVar "V''",TVar "Y"]) env step3 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X",PMetaVar "Y"] env env <- getControlPatt "abrupted" (Just (VPMetaVar "V'")) env - (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V'")) env (premise (TVar "X") (PMetaVar "X'") env)) + (env,[__varabrupted]) <- receiveSignals ["abrupted"] (withControlTerm "abrupted" (Just (TVar "V'")) env (premise (TVar "X") [PMetaVar "X'"] env)) env <- receiveSignalPatt __varabrupted (Just (VPAnnotated (VPMetaVar "V'") (TSortComplement (TName "throwing")))) env raiseTerm "abrupted" (TVar "V'") env stepTermTo (TApp "handle-thrown" [TVar "X'",TVar "Y"]) env @@ -82,7 +82,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PAnnotated (PMetaVar "P") (TName "defined-values"),PMetaVar "Y"] env + env <- fsMatch fargs [PAnnotated (PMetaVar "P") (TName "values"),PMetaVar "Y"] env rewriteTermTo (TApp "else" [TApp "case-match" [TVar "P",TVar "Y"],TApp "throw" [TName "given"]]) env throwing_ = FName "throwing" 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 @@ -5,22 +5,21 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList - [("identifiers",DataTypeMemberss "identifiers" [] [DataTypeInclusionn (TName "strings"),DataTypeMemberConstructor "identifier-tagged" [TName "identifiers",TName "defined-values"] (Just [])]),("ids",DataTypeMemberss "ids" [] [DataTypeInclusionn (TName "strings"),DataTypeMemberConstructor "identifier-tagged" [TName "identifiers",TName "defined-values"] (Just [])])] + [("identifiers",DataTypeMemberss "identifiers" [] [DataTypeInclusionn (TName "strings"),DataTypeMemberConstructor "identifier-tagged" [TName "identifiers",TName "values"] (Just [])]),("ids",DataTypeMemberss "ids" [] [DataTypeInclusionn (TName "strings"),DataTypeMemberConstructor "identifier-tagged" [TName "identifiers",TName "values"] (Just [])])] funcons = libFromList - [("environments",NullaryFuncon stepEnvironments),("env",NullaryFuncon stepEnvironments),("envs",NullaryFuncon stepEnvironments),("identifier-tagged",StrictFuncon stepIdentifier_tagged),("id-tagged",StrictFuncon stepIdentifier_tagged),("fresh-identifier",NullaryFuncon stepFresh_identifier),("initialise-binding",NonStrictFuncon stepInitialise_binding),("bind-value",StrictFuncon stepBind_value),("bind",StrictFuncon stepBind_value),("unbind",StrictFuncon stepUnbind),("bound-directly",StrictFuncon stepBound_directly),("bound-value",StrictFuncon stepBound_value),("bound",StrictFuncon stepBound_value),("closed",NonStrictFuncon stepClosed),("scope",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepScope),("accumulate",NonStrictFuncon stepAccumulate),("collateral",StrictFuncon stepCollateral),("bind-recursively",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepBind_recursively),("recursive",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepRecursive),("re-close",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepRe_close),("bind-to-forward-links",StrictFuncon stepBind_to_forward_links),("set-forward-links",StrictFuncon stepSet_forward_links),("identifiers",NullaryFuncon stepIdentifiers),("ids",NullaryFuncon stepIdentifiers)] + [("environments",NullaryFuncon stepEnvironments),("envs",NullaryFuncon stepEnvironments),("identifier-tagged",StrictFuncon stepIdentifier_tagged),("id-tagged",StrictFuncon stepIdentifier_tagged),("fresh-identifier",NullaryFuncon stepFresh_identifier),("initialise-binding",NonStrictFuncon stepInitialise_binding),("bind-value",StrictFuncon stepBind_value),("bind",StrictFuncon stepBind_value),("unbind",StrictFuncon stepUnbind),("bound-directly",StrictFuncon stepBound_directly),("bound-value",StrictFuncon stepBound_value),("bound",StrictFuncon stepBound_value),("closed",NonStrictFuncon stepClosed),("scope",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepScope),("accumulate",NonStrictFuncon stepAccumulate),("collateral",StrictFuncon stepCollateral),("bind-recursively",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepBind_recursively),("recursive",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepRecursive),("re-close",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepRe_close),("bind-to-forward-links",StrictFuncon stepBind_to_forward_links),("set-forward-links",StrictFuncon stepSet_forward_links),("identifiers",NullaryFuncon stepIdentifiers),("ids",NullaryFuncon stepIdentifiers)] environments_ = FName "environments" -env_ = FName "environments" envs_ = FName "environments" stepEnvironments = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "maps" [TName "identifiers",TName "values"]) env + rewriteTermTo (TApp "maps" [TName "identifiers",TSortSeq (TName "values") QuestionMarkOp]) env identifier_tagged_ fargs = FApp "identifier-tagged" (fargs) id_tagged_ fargs = FApp "identifier-tagged" (fargs) @@ -29,8 +28,8 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1",VPMetaVar "_X2"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) env - env <- sideCondition (SCIsInSort (TVar "_X2") (TName "values")) 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 fresh_identifier_ = FName "fresh-identifier" @@ -53,8 +52,8 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "I") (TName "identifiers"),VPAnnotated (VPMetaVar "V") (TName "defined-values")] env - rewriteTermTo (TMap [TVar "I",TVar "V"]) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "I") (TName "identifiers"),VPAnnotated (VPMetaVar "V") (TName "values")] env + rewriteTermTo (TMap [TBinding (TVar "I") (TVar "V")]) env unbind_ fargs = FApp "unbind" (fargs) stepUnbind fargs = @@ -62,7 +61,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPAnnotated (VPMetaVar "I") (TName "identifiers")] env - rewriteTermTo (TMap [TVar "I",TName "none"]) env + rewriteTermTo (TMap [TBinding (TVar "I") (TSeq [])]) env bound_directly_ fargs = FApp "bound-directly" (fargs) stepBound_directly fargs = @@ -70,14 +69,14 @@ where step1 = do let env = emptyEnv env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "I") (TName "identifiers")] env - env <- getInhPatt "environment" (VPMetaVar "Rho") env - env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "Rho",TVar "I"]) (VPAnnotated (VPMetaVar "V") (TName "defined-values"))) env + env <- getInhPatt "environment" [VPMetaVar "Rho"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "Rho",TVar "I"]) [VPAnnotated (VPMetaVar "V") (TName "values")]) env stepTermTo (TVar "V") env step2 = do let env = emptyEnv env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "I") (TName "identifiers")] env - env <- getInhPatt "environment" (VPMetaVar "Rho") env - env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "Rho",TVar "I"]) (PADT "none" [])) env + env <- getInhPatt "environment" [VPMetaVar "Rho"] env + env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "Rho",TVar "I"]) []) env stepTermTo (TName "fail") env bound_value_ fargs = FApp "bound-value" (fargs) @@ -99,8 +98,8 @@ step1 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X"] env - env <- getInhPatt "environment" (VPWildCard) env - env <- withInhTerm "environment" (TApp "map" []) env (premise (TVar "X") (PMetaVar "X'") env) + env <- getInhPatt "environment" [VPWildCard] env + env <- withInhTerm "environment" (TApp "map" []) env (premise (TVar "X") [PMetaVar "X'"] env) stepTermTo (TApp "closed" [TVar "X'"]) env scope_ fargs = FApp "scope" (fargs) @@ -113,8 +112,8 @@ step1 = do let env = emptyEnv env <- lifted_fsMatch fargs [PAnnotated (PMetaVar "Rho1") (TName "environments"),PMetaVar "X"] env - env <- getInhPatt "environment" (VPMetaVar "Rho0") env - env <- withInhTerm "environment" (TApp "map-override" [TVar "Rho1",TVar "Rho0"]) env (premise (TVar "X") (PMetaVar "X'") env) + env <- getInhPatt "environment" [VPMetaVar "Rho0"] env + env <- withInhTerm "environment" (TApp "map-override" [TVar "Rho1",TVar "Rho0"]) env (premise (TVar "X") [PMetaVar "X'"] env) stepTermTo (TApp "scope" [TVar "Rho1",TVar "X'"]) env accumulate_ fargs = FApp "accumulate" (fargs) @@ -139,7 +138,7 @@ step1 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "D1",PMetaVar "D2"] env - env <- premise (TVar "D1") (PMetaVar "D1'") env + env <- premise (TVar "D1") [PMetaVar "D1'"] env stepTermTo (TApp "accumulate" [TVar "D1'",TVar "D2"]) env collateral_ fargs = FApp "collateral" (fargs) @@ -148,7 +147,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPAnnotated (VPSeqVar "Rho*" StarOp) (TSortSeq (TName "environments") StarOp)] env - rewriteTermTo (TApp "def" [TApp "map-unite" [TVar "Rho*"]]) env + rewriteTermTo (TApp "checked" [TApp "map-unite" [TVar "Rho*"]]) env bind_recursively_ fargs = FApp "bind-recursively" (fargs) stepBind_recursively fargs = @@ -180,7 +179,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPAnnotated (VPMetaVar "SI") (TApp "sets" [TName "identifiers"])] env - rewriteTermTo (TApp "map-unite" [TApp "interleave-map" [TApp "bind-value" [TName "given",TApp "fresh-link" [TName "defined-values"]],TApp "set-elements" [TVar "SI"]]]) env + rewriteTermTo (TApp "map-unite" [TApp "interleave-map" [TApp "bind-value" [TName "given",TApp "fresh-link" [TName "values"]],TApp "set-elements" [TVar "SI"]]]) env set_forward_links_ fargs = FApp "set-forward-links" (fargs) stepSet_forward_links fargs = @@ -188,7 +187,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPAnnotated (VPMetaVar "M") (TApp "maps" [TName "identifiers",TName "links"])] env - rewriteTermTo (TApp "effect" [TApp "interleave-map" [TApp "set-link" [TApp "lookup" [TVar "M",TName "given"],TApp "bound-value" [TName "given"]],TApp "set-elements" [TApp "map-domain" [TVar "M"]]]]) env + rewriteTermTo (TApp "effect" [TApp "interleave-map" [TApp "set-link" [TApp "map-lookup" [TVar "M",TName "given"],TApp "bound-value" [TName "given"]],TApp "set-elements" [TApp "map-domain" [TVar "M"]]]]) env identifiers_ = FName "identifiers" stepIdentifiers = rewriteType "identifiers" [] 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 @@ -5,70 +5,14 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList [("yielding",DataTypeMemberss "yielding" [] [DataTypeMemberConstructor "signal" [] (Just [])])] funcons = libFromList - [("interleave",StrictFuncon stepInterleave),("signal",NullaryFuncon stepSignal),("yield",NullaryFuncon stepYield),("yield-on-value",StrictFuncon stepYield_on_value),("yield-on-abrupt",NonStrictFuncon stepYield_on_abrupt),("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),("yielding",NullaryFuncon stepYielding)] - -interleave_ fargs = FApp "interleave" (fargs) -stepInterleave fargs = - evalRules [rewrite1] [] - where rewrite1 = do - let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - rewriteTermTo (TVar "V*") env - -signal_ = FName "signal" -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 - -yield_ = FName "yield" -stepYield = evalRules [rewrite1] [] - where rewrite1 = do - let env = emptyEnv - rewriteTermTo (TApp "yield-on-value" [TName "none"]) env - -yield_on_value_ fargs = FApp "yield-on-value" (fargs) -stepYield_on_value fargs = - evalRules [] [step1] - where step1 = do - let env = emptyEnv - env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values")] env - env <- getControlPatt "yielded" (Just (PADT "signal" [])) env - raiseTerm "yielded" (TName "signal") env - stepTermTo (TVar "V") env - -yield_on_abrupt_ fargs = FApp "yield-on-abrupt" (fargs) -stepYield_on_abrupt fargs = - evalRules [rewrite1] [step1,step2] - 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 "abrupt" (Just (VPMetaVar "V")) env - env <- getControlPatt "yielded" (Just (PADT "signal" [])) env - (env,[__varabrupt,__varyielded]) <- receiveSignals ["abrupt","yielded"] (withControlTerm "abrupt" (Just (TVar "V")) env (withControlTerm "yielded" (Just (TVar "___")) env (premise (TVar "X") (PMetaVar "X'") env))) - env <- receiveSignalPatt __varabrupt (Just (VPAnnotated (VPMetaVar "V") (TName "values"))) env - env <- receiveSignalPatt __varyielded (Just (VPSeqVar "___" QuestionMarkOp)) env - raiseTerm "abrupt" (TVar "V") env - raiseTerm "yielded" (TName "signal") env - stepTermTo (TApp "yield-on-abrupt" [TVar "X'"]) env - step2 = do - let env = emptyEnv - env <- lifted_fsMatch fargs [PMetaVar "X"] env - env <- getControlPatt "abrupt" (Nothing) env - (env,[__varabrupt]) <- receiveSignals ["abrupt"] (withControlTerm "abrupt" (Nothing) env (premise (TVar "X") (PMetaVar "X'") env)) - env <- receiveSignalPatt __varabrupt (Nothing) env - stepTermTo (TApp "yield-on-abrupt" [TVar "X'"]) env + [("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_ fargs = FApp "left-to-right" (fargs) l_to_r_ fargs = FApp "left-to-right" (fargs) @@ -81,30 +25,16 @@ step1 = do let env = emptyEnv env <- lifted_fsMatch fargs [PAnnotated (PSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp),PMetaVar "Y",PSeqVar "Z*" StarOp] env - env <- premise (TVar "Y") (PMetaVar "Y'") env + 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 = evalRules [rewrite1,rewrite2] [step1] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PValue (PADT "none" []),PSeqVar "Y+" PlusOp] env + env <- fsMatch fargs [PValue (PADT "null-value" []),PSeqVar "Y+" PlusOp] env rewriteTermTo (TApp "sequential" [TVar "Y+"]) env rewrite2 = do let env = emptyEnv @@ -113,7 +43,7 @@ step1 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X",PSeqVar "Y+" PlusOp] env - env <- premise (TVar "X") (PMetaVar "X'") env + env <- premise (TVar "X") [PMetaVar "X'"] env stepTermTo (TApp "sequential" [TVar "X'",TVar "Y+"]) env effect_ fargs = FApp "effect" (fargs) @@ -122,7 +52,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - rewriteTermTo (TName "none") env + rewriteTermTo (TName "null-value") env choice_ fargs = FApp "choice" (fargs) stepChoice fargs = @@ -152,7 +82,7 @@ where rewrite1 = do let env = emptyEnv env <- fsMatch fargs [PMetaVar "B",PMetaVar "X"] env - rewriteTermTo (TApp "if-true-else" [TVar "B",TApp "sequential" [TVar "X",TApp "while-true" [TVar "B",TVar "X"]],TName "none"]) env + rewriteTermTo (TApp "if-true-else" [TVar "B",TApp "sequential" [TVar "X",TApp "while-true" [TVar "B",TVar "X"]],TName "null-value"]) env do_while_true_ fargs = FApp "do-while-true" (fargs) do_while_ fargs = FApp "do-while-true" (fargs) @@ -161,7 +91,63 @@ where rewrite1 = do let env = emptyEnv env <- fsMatch fargs [PMetaVar "X",PMetaVar "B"] env - rewriteTermTo (TApp "sequential" [TVar "X",TApp "if-true-else" [TVar "B",TApp "do-while-true" [TVar "X",TVar "B"],TName "none"]]) env + rewriteTermTo (TApp "sequential" [TVar "X",TApp "if-true-else" [TVar "B",TApp "do-while-true" [TVar "X",TVar "B"],TName "null-value"]]) env + +interleave_ fargs = FApp "interleave" (fargs) +stepInterleave fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env + rewriteTermTo (TVar "V*") env + +signal_ = FName "signal" +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 + +yield_ = FName "yield" +stepYield = evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + rewriteTermTo (TApp "yield-on-value" [TName "null-value"]) env + +yield_on_value_ fargs = FApp "yield-on-value" (fargs) +stepYield_on_value fargs = + evalRules [] [step1] + where step1 = do + let env = emptyEnv + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values")] env + env <- getControlPatt "yielded" (Just (PADT "signal" [])) env + raiseTerm "yielded" (TName "signal") env + stepTermTo (TVar "V") env + +yield_on_abrupt_ fargs = FApp "yield-on-abrupt" (fargs) +stepYield_on_abrupt fargs = + evalRules [rewrite1] [step1,step2] + 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 "abrupt" (Just (VPMetaVar "V")) env + env <- getControlPatt "yielded" (Just (PADT "signal" [])) env + (env,[__varabrupt,__varyielded]) <- receiveSignals ["abrupt","yielded"] (withControlTerm "abrupt" (Just (TVar "V")) env (withControlTerm "yielded" (Just (TVar "___")) env (premise (TVar "X") [PMetaVar "X'"] env))) + env <- receiveSignalPatt __varabrupt (Just (VPAnnotated (VPMetaVar "V") (TName "values"))) env + env <- receiveSignalPatt __varyielded (Just (VPSeqVar "___" QuestionMarkOp)) env + raiseTerm "abrupt" (TVar "V") env + raiseTerm "yielded" (TName "signal") env + stepTermTo (TApp "yield-on-abrupt" [TVar "X'"]) env + step2 = do + let env = emptyEnv + env <- lifted_fsMatch fargs [PMetaVar "X"] env + env <- getControlPatt "abrupt" (Nothing) env + (env,[__varabrupt]) <- receiveSignals ["abrupt"] (withControlTerm "abrupt" (Nothing) env (premise (TVar "X") [PMetaVar "X'"] env)) + env <- receiveSignalPatt __varabrupt (Nothing) env + stepTermTo (TApp "yield-on-abrupt" [TVar "X'"]) env yielding_ = FName "yielding" stepYielding = rewriteType "yielding" [] diff --git a/cbs/Funcons/Core/Computations/Normal/Generating/Generating.hs b/cbs/Funcons/Core/Computations/Normal/Generating/Generating.hs --- a/cbs/Funcons/Core/Computations/Normal/Generating/Generating.hs +++ b/cbs/Funcons/Core/Computations/Normal/Generating/Generating.hs @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -19,7 +19,7 @@ where step1 = do let env = emptyEnv env <- getMutPatt "used-atom-set" (VPMetaVar "SA") env - env <- lifted_sideCondition (SCPatternMatch (TApp "element-not-in" [TName "atoms",TVar "SA"]) (VPMetaVar "A")) env + env <- lifted_sideCondition (SCPatternMatch (TApp "element-not-in" [TName "atoms",TVar "SA"]) [VPMetaVar "A"]) env putMutTerm "used-atom-set" (TApp "set-insert" [TVar "A",TVar "SA"]) env stepTermTo (TVar "A") env @@ -30,6 +30,6 @@ let env = emptyEnv env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "SA") (TApp "sets" [TName "atoms"])] env env <- getMutPatt "used-atom-set" (VPMetaVar "SA'") env - env <- lifted_sideCondition (SCPatternMatch (TApp "element-not-in" [TName "atoms",TVar "SA"]) (VPMetaVar "A")) env + env <- lifted_sideCondition (SCPatternMatch (TApp "element-not-in" [TName "atoms",TVar "SA"]) [VPMetaVar "A"]) env putMutTerm "used-atom-set" (TApp "set-insert" [TVar "A",TVar "SA'"]) env stepTermTo (TVar "A") env diff --git a/cbs/Funcons/Core/Computations/Normal/Giving/Giving.hs b/cbs/Funcons/Core/Computations/Normal/Giving/Giving.hs --- a/cbs/Funcons/Core/Computations/Normal/Giving/Giving.hs +++ b/cbs/Funcons/Core/Computations/Normal/Giving/Giving.hs @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -27,24 +27,24 @@ evalRules [rewrite1] [step1] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PAnnotated (PMetaVar "V") (TName "defined-values"),PAnnotated (PMetaVar "W") (TName "values")] env + env <- fsMatch fargs [PAnnotated PWildCard (TName "values"),PAnnotated (PMetaVar "W") (TName "values")] env rewriteTermTo (TVar "W") env step1 = do let env = emptyEnv - env <- lifted_fsMatch fargs [PAnnotated (PMetaVar "V") (TName "defined-values"),PMetaVar "Y"] env - env <- getInhPatt "given-value" (VPWildCard) env - env <- withInhTerm "given-value" (TVar "V") env (premise (TVar "Y") (PMetaVar "Y'") env) + env <- lifted_fsMatch fargs [PAnnotated (PMetaVar "V") (TName "values"),PMetaVar "Y"] env + env <- getInhPatt "given-value" [VPSeqVar "___" QuestionMarkOp] env + env <- withInhTerm "given-value" (TVar "V") env (premise (TVar "Y") [PMetaVar "Y'"] env) stepTermTo (TApp "give" [TVar "V",TVar "Y'"]) env given_ = FName "given" stepGiven = evalRules [] [step1,step2] where step1 = do let env = emptyEnv - env <- getInhPatt "given-value" (VPAnnotated (VPMetaVar "V") (TName "defined-values")) env + env <- getInhPatt "given-value" [VPAnnotated (VPMetaVar "V") (TName "values")] env stepTermTo (TVar "V") env step2 = do let env = emptyEnv - env <- getInhPatt "given-value" (PADT "none" []) env + env <- getInhPatt "given-value" [] env stepTermTo (TName "fail") env no_given_ fargs = FApp "no-given" (fargs) @@ -57,8 +57,8 @@ step1 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X"] env - env <- getInhPatt "given-value" (VPWildCard) env - env <- withInhTerm "given-value" (TName "none") env (premise (TVar "X") (PMetaVar "X'") env) + env <- getInhPatt "given-value" [VPSeqVar "___" QuestionMarkOp] env + env <- withInhTerm "given-value" (TSeq []) env (premise (TVar "X") [PMetaVar "X'"] env) stepTermTo (TApp "no-given" [TVar "X'"]) env left_to_right_map_ fargs = FApp "left-to-right-map" (fargs) @@ -66,11 +66,11 @@ evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "F",PAnnotated (PMetaVar "V") (TName "defined-values"),PAnnotated (PSeqVar "V*" StarOp) (TSortSeq (TName "defined-values") StarOp)] env + env <- fsMatch fargs [PMetaVar "F",PAnnotated (PMetaVar "V") (TName "values"),PAnnotated (PSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env rewriteTermTo (TApp "left-to-right" [TApp "give" [TVar "V",TVar "F"],TApp "left-to-right-map" [TVar "F",TVar "V*"]]) env rewrite2 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "F"] env + env <- fsMatch fargs [PWildCard] env rewriteTermTo (TSeq []) env interleave_map_ fargs = FApp "interleave-map" (fargs) @@ -78,11 +78,11 @@ evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "F",PAnnotated (PMetaVar "V") (TName "defined-values"),PAnnotated (PSeqVar "V*" StarOp) (TSortSeq (TName "defined-values") StarOp)] env + env <- fsMatch fargs [PMetaVar "F",PAnnotated (PMetaVar "V") (TName "values"),PAnnotated (PSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env rewriteTermTo (TApp "interleave" [TApp "give" [TVar "V",TVar "F"],TApp "interleave-map" [TVar "F",TVar "V*"]]) env rewrite2 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "F"] env + env <- fsMatch fargs [PWildCard] env rewriteTermTo (TSeq []) env left_to_right_repeat_ fargs = FApp "left-to-right-repeat" (fargs) @@ -90,12 +90,12 @@ evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "F",PAnnotated (PMetaVar "M") (TName "ints"),PAnnotated (PMetaVar "N") (TName "ints")] env + env <- fsMatch fargs [PMetaVar "F",PAnnotated (PMetaVar "M") (TName "integers"),PAnnotated (PMetaVar "N") (TName "integers")] env env <- sideCondition (SCEquality (TApp "is-less-or-equal" [TVar "M",TVar "N"]) (TName "true")) env rewriteTermTo (TApp "left-to-right" [TApp "give" [TVar "M",TVar "F"],TApp "left-to-right-repeat" [TVar "F",TApp "int-add" [TVar "M",TFuncon (FValue (Nat 1))],TVar "N"]]) env rewrite2 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "F",PAnnotated (PMetaVar "M") (TName "ints"),PAnnotated (PMetaVar "N") (TName "ints")] env + env <- fsMatch fargs [PWildCard,PAnnotated (PMetaVar "M") (TName "integers"),PAnnotated (PMetaVar "N") (TName "integers")] env env <- sideCondition (SCEquality (TApp "is-less-or-equal" [TVar "M",TVar "N"]) (TName "false")) env rewriteTermTo (TSeq []) env @@ -104,37 +104,45 @@ evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "F",PAnnotated (PMetaVar "M") (TName "ints"),PAnnotated (PMetaVar "N") (TName "ints")] env + env <- fsMatch fargs [PMetaVar "F",PAnnotated (PMetaVar "M") (TName "integers"),PAnnotated (PMetaVar "N") (TName "integers")] env env <- sideCondition (SCEquality (TApp "is-less-or-equal" [TVar "M",TVar "N"]) (TName "true")) env rewriteTermTo (TApp "interleave" [TApp "give" [TVar "M",TVar "F"],TApp "interleave-repeat" [TVar "F",TApp "int-add" [TVar "M",TFuncon (FValue (Nat 1))],TVar "N"]]) env rewrite2 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "F",PAnnotated (PMetaVar "M") (TName "ints"),PAnnotated (PMetaVar "N") (TName "ints")] env + env <- fsMatch fargs [PWildCard,PAnnotated (PMetaVar "M") (TName "integers"),PAnnotated (PMetaVar "N") (TName "integers")] env env <- sideCondition (SCEquality (TApp "is-less-or-equal" [TVar "M",TVar "N"]) (TName "false")) env rewriteTermTo (TSeq []) env left_to_right_filter_ fargs = FApp "left-to-right-filter" (fargs) stepLeft_to_right_filter fargs = - evalRules [rewrite1] [] + evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "P",PAnnotated (PSeqVar "V*" StarOp) (TSortSeq (TName "defined-values") StarOp)] env - rewriteTermTo (TApp "filter-defined" [TApp "left-to-right-map" [TApp "if-true-else" [TVar "P",TName "given",TName "none"],TVar "V*"]]) env + env <- fsMatch fargs [PMetaVar "P",PAnnotated (PMetaVar "V") (TName "values"),PAnnotated (PSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env + rewriteTermTo (TApp "left-to-right" [TApp "when-true" [TApp "give" [TVar "V",TVar "P"],TVar "V"],TApp "left-to-right-filter" [TVar "P",TVar "V*"]]) env + rewrite2 = do + let env = emptyEnv + env <- fsMatch fargs [PWildCard] env + rewriteTermTo (TSeq []) env interleave_filter_ fargs = FApp "interleave-filter" (fargs) stepInterleave_filter fargs = - evalRules [rewrite1] [] + evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "P",PAnnotated (PSeqVar "V*" StarOp) (TSortSeq (TName "defined-values") StarOp)] env - rewriteTermTo (TApp "filter-defined" [TApp "interleave-map" [TApp "if-true-else" [TVar "P",TName "given",TName "none"],TVar "V*"]]) env + env <- fsMatch fargs [PMetaVar "P",PAnnotated (PMetaVar "V") (TName "values"),PAnnotated (PSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env + rewriteTermTo (TApp "interleave" [TApp "when-true" [TApp "give" [TVar "V",TVar "P"],TVar "V"],TApp "interleave-filter" [TVar "P",TVar "V*"]]) env + rewrite2 = do + let env = emptyEnv + env <- fsMatch fargs [PWildCard] env + rewriteTermTo (TSeq []) env fold_left_ fargs = FApp "fold-left" (fargs) stepFold_left fargs = evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "F",PAnnotated (PMetaVar "A") (TName "values")] env + env <- fsMatch fargs [PWildCard,PAnnotated (PMetaVar "A") (TName "values")] env rewriteTermTo (TVar "A") env rewrite2 = do let env = emptyEnv diff --git a/cbs/Funcons/Core/Computations/Normal/Interacting/Interacting.hs b/cbs/Funcons/Core/Computations/Normal/Interacting/Interacting.hs --- a/cbs/Funcons/Core/Computations/Normal/Interacting/Interacting.hs +++ b/cbs/Funcons/Core/Computations/Normal/Interacting/Interacting.hs @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -19,17 +19,17 @@ evalRules [] [step1] where step1 = do let env = emptyEnv - env <- lifted_vsMatch fargs [VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "defined-values") StarOp)] env + env <- lifted_vsMatch fargs [VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env writeOutTerm "standard-out" (TVar "V*") env - stepTermTo (TName "none") env + stepTermTo (TName "null-value") env read_ = FName "read" stepRead = evalRules [] [step1,step2] where step1 = do let env = emptyEnv - env <- matchInput "standard-in" (VPAnnotated (VPMetaVar "V") (TName "defined-values")) env + env <- matchInput "standard-in" (VPAnnotated (VPMetaVar "V") (TSortComplement (TName "null-type"))) env stepTermTo (TVar "V") env step2 = do let env = emptyEnv - env <- matchInput "standard-in" (PADT "none" []) env + env <- matchInput "standard-in" (PADT "null-value" []) env stepTermTo (TName "fail") env 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 @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -20,7 +20,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) 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 initialise_linking_ fargs = FApp "initialise-linking" (fargs) @@ -36,8 +36,8 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "VT"] env - rewriteTermTo (TApp "link" [TApp "allocate-variable" [TVar "VT"]]) env + env <- fsMatch fargs [PMetaVar "T"] env + rewriteTermTo (TApp "link" [TApp "allocate-variable" [TVar "T"]]) env fresh_initialised_link_ fargs = FApp "fresh-initialised-link" (fargs) fresh_init_link_ fargs = FApp "fresh-initialised-link" (fargs) @@ -45,15 +45,15 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "VT",PAnnotated (PMetaVar "V") (TVar "VT")] env - rewriteTermTo (TApp "link" [TApp "allocate-initialised-variable" [TVar "VT",TVar "V"]]) env + env <- fsMatch fargs [PMetaVar "T",PAnnotated (PMetaVar "V") (TVar "T")] env + rewriteTermTo (TApp "link" [TApp "allocate-initialised-variable" [TVar "T",TVar "V"]]) env set_link_ fargs = FApp "set-link" (fargs) stepSet_link fargs = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "link" [VPAnnotated (VPMetaVar "Var") (TName "variables")],VPAnnotated (VPMetaVar "V") (TName "defined-values")] env + env <- vsMatch fargs [PADT "link" [VPAnnotated (VPMetaVar "Var") (TName "variables")],VPAnnotated (VPMetaVar "V") (TName "values")] env rewriteTermTo (TApp "initialise-variable" [TVar "Var",TVar "V"]) env follow_link_ fargs = FApp "follow-link" (fargs) @@ -73,8 +73,7 @@ rewriteTermTo (TApp "assigned" [TVar "Var"]) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [VPMetaVar "V"] env - env <- sideCondition (SCIsInSort (TVar "V") (TSortComplement (TSortUnion (TName "links") (TName "nothing")))) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TSortComplement (TName "links"))] env rewriteTermTo (TVar "V") env links_ = FName "links" 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 @@ -5,14 +5,14 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList [("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",NonStrictFuncon stepAllocate_variable),("alloc",NonStrictFuncon 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 stepCurrent_value),("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),("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_ = FName "locations" locs_ = FName "locations" @@ -25,7 +25,7 @@ stepStores = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TApp "maps" [TName "locations",TName "values"]) env + rewriteTermTo (TApp "maps" [TName "locations",TSortSeq (TName "values") QuestionMarkOp]) env store_clear_ = FName "store-clear" stepStore_clear = evalRules [] [step1] @@ -33,7 +33,7 @@ let env = emptyEnv env <- getMutPatt "store" (VPWildCard) env putMutTerm "store" (TApp "map" []) env - stepTermTo (TName "none") env + stepTermTo (TName "null-value") env initialise_storing_ fargs = FApp "initialise-storing" (fargs) init_storing_ fargs = FApp "initialise-storing" (fargs) @@ -51,8 +51,8 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1",VPMetaVar "_X2"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) env - env <- sideCondition (SCIsInSort (TVar "_X2") (TName "values")) 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 allocate_variable_ fargs = FApp "allocate-variable" (fargs) @@ -61,14 +61,14 @@ evalRules [] [step1] where step1 = do let env = emptyEnv - env <- lifted_fsMatch fargs [PAnnotated (PMetaVar "VT") (TName "types")] env + env <- lifted_vsMatch fargs [VPAnnotated (VPMetaVar "T") (TName "types")] env env <- getMutPatt "store" (VPMetaVar "Sigma") env putMutTerm "store" (TVar "Sigma") env - env <- premise (TApp "use-atom-not-in" [TApp "dom" [TVar "Sigma"]]) (PMetaVar "L") env + env <- premise (TApp "use-atom-not-in" [TApp "dom" [TVar "Sigma"]]) [PMetaVar "L"] env env <- getMutPatt "store" (VPMetaVar "Sigma'") env - env <- lifted_sideCondition (SCPatternMatch (TApp "map-override" [TMap [TVar "L",TName "none"],TVar "Sigma'"]) (VPMetaVar "Sigma''")) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-override" [TMap [TBinding (TVar "L") (TSeq [])],TVar "Sigma'"]) [VPMetaVar "Sigma''"]) env putMutTerm "store" (TVar "Sigma''") env - stepTermTo (TApp "variable" [TVar "L",TVar "VT"]) env + stepTermTo (TApp "variable" [TVar "L",TVar "T"]) env recycle_variables_ fargs = FApp "recycle-variables" (fargs) recycle_ fargs = FApp "recycle-variables" (fargs) @@ -80,14 +80,14 @@ rewriteTermTo (TApp "sequential" [TApp "recycle-variables" [TVar "Var"],TApp "recycle-variables" [TVar "Var+"]]) env step1 = do let env = emptyEnv - env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env + env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env env <- getMutPatt "store" (VPMetaVar "Sigma") env env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "true")) env putMutTerm "store" (TApp "map-delete" [TVar "Sigma",TSet [TVar "L"]]) env - stepTermTo (TName "none") env + stepTermTo (TName "null-value") env step2 = do let env = emptyEnv - env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env + env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env env <- getMutPatt "store" (VPMetaVar "Sigma") env env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "false")) env putMutTerm "store" (TVar "Sigma") env @@ -99,16 +99,16 @@ evalRules [] [step1,step2] where step1 = do let env = emptyEnv - env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "defined-values")] env + env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "values")] env env <- getMutPatt "store" (VPMetaVar "Sigma") env - env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "not" [TApp "is-defined" [TApp "lookup" [TVar "Sigma",TVar "L"]]],TApp "is-in-type" [TVar "Val",TVar "VT"]]) (TName "true")) env - putMutTerm "store" (TApp "map-override" [TMap [TVar "L",TVar "Val"],TVar "Sigma"]) env - stepTermTo (TName "none") env + env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "not" [TApp "is-value" [TApp "map-lookup" [TVar "Sigma",TVar "L"]]],TApp "is-in-type" [TVar "Val",TVar "T"]]) (TName "true")) env + putMutTerm "store" (TApp "map-override" [TMap [TBinding (TVar "L") (TVar "Val")],TVar "Sigma"]) env + stepTermTo (TName "null-value") env step2 = do let env = emptyEnv - env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "defined-values")] env + env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "values")] env env <- getMutPatt "store" (VPMetaVar "Sigma") env - env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "not" [TApp "is-defined" [TApp "lookup" [TVar "Sigma",TVar "L"]]],TApp "is-in-type" [TVar "Val",TVar "VT"]]) (TName "false")) env + env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "not" [TApp "is-value" [TApp "map-lookup" [TVar "Sigma",TVar "L"]]],TApp "is-in-type" [TVar "Val",TVar "T"]]) (TName "false")) env putMutTerm "store" (TVar "Sigma") env stepTermTo (TName "fail") env @@ -118,24 +118,24 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "VT",PAnnotated (PMetaVar "Val") (TVar "VT")] env - rewriteTermTo (TApp "give" [TApp "allocate-variable" [TVar "VT"],TApp "sequential" [TApp "initialise-variable" [TName "given",TVar "Val"],TName "given"]]) env + env <- fsMatch fargs [PMetaVar "T",PAnnotated (PMetaVar "Val") (TVar "T")] env + rewriteTermTo (TApp "give" [TApp "allocate-variable" [TVar "T"],TApp "sequential" [TApp "initialise-variable" [TName "given",TVar "Val"],TName "given"]]) env assign_ fargs = FApp "assign" (fargs) stepAssign fargs = evalRules [] [step1,step2] where step1 = do let env = emptyEnv - env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "defined-values")] env + env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "values")] env env <- getMutPatt "store" (VPMetaVar "Sigma") env - env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "is-in-type" [TVar "Val",TVar "VT"]]) (TName "true")) env - putMutTerm "store" (TApp "map-override" [TMap [TVar "L",TVar "Val"],TVar "Sigma"]) env - stepTermTo (TName "none") env + env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "is-in-type" [TVar "Val",TVar "T"]]) (TName "true")) env + putMutTerm "store" (TApp "map-override" [TMap [TBinding (TVar "L") (TVar "Val")],TVar "Sigma"]) env + stepTermTo (TName "null-value") env step2 = do let env = emptyEnv - env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "defined-values")] env + env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")],VPAnnotated (VPMetaVar "Val") (TName "values")] env env <- getMutPatt "store" (VPMetaVar "Sigma") env - env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "is-in-type" [TVar "Val",TVar "VT"]]) (TName "false")) env + env <- lifted_sideCondition (SCEquality (TApp "and" [TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]],TApp "is-in-type" [TVar "Val",TVar "T"]]) (TName "false")) env putMutTerm "store" (TVar "Sigma") env stepTermTo (TName "fail") env @@ -144,16 +144,16 @@ evalRules [] [step1,step2] where step1 = do let env = emptyEnv - env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env + env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env env <- getMutPatt "store" (VPMetaVar "Sigma") env - env <- lifted_sideCondition (SCPatternMatch (TApp "lookup" [TVar "Sigma",TVar "L"]) (VPAnnotated (VPMetaVar "Val") (TName "defined-values"))) env + env <- lifted_sideCondition (SCPatternMatch (TApp "map-lookup" [TVar "Sigma",TVar "L"]) [VPAnnotated (VPMetaVar "Val") (TName "values")]) env putMutTerm "store" (TVar "Sigma") env stepTermTo (TVar "Val") env step2 = do let env = emptyEnv - env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env + env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env env <- getMutPatt "store" (VPMetaVar "Sigma") env - env <- lifted_sideCondition (SCEquality (TApp "lookup" [TVar "Sigma",TVar "L"]) (TName "none")) env + env <- lifted_sideCondition (SCEquality (TApp "map-lookup" [TVar "Sigma",TVar "L"]) (TSeq [])) env putMutTerm "store" (TVar "Sigma") env stepTermTo (TName "fail") env @@ -162,14 +162,14 @@ evalRules [] [step1,step2] where step1 = do let env = emptyEnv - env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env + env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env env <- getMutPatt "store" (VPMetaVar "Sigma") env env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "true")) env - putMutTerm "store" (TApp "map-override" [TMap [TVar "L",TName "none"],TVar "Sigma"]) env - stepTermTo (TName "none") env + putMutTerm "store" (TApp "map-override" [TMap [TBinding (TVar "L") (TSeq [])],TVar "Sigma"]) env + stepTermTo (TName "null-value") env step2 = do let env = emptyEnv - env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "VT") (TName "types")]] env + env <- lifted_vsMatch fargs [PADT "variable" [VPAnnotated (VPMetaVar "L") (TName "locations"),VPAnnotated (VPMetaVar "T") (TName "types")]] env env <- getMutPatt "store" (VPMetaVar "Sigma") env env <- lifted_sideCondition (SCEquality (TApp "is-in-set" [TVar "L",TApp "dom" [TVar "Sigma"]]) (TName "false")) env putMutTerm "store" (TVar "Sigma") env @@ -180,30 +180,31 @@ evalRules [rewrite1,rewrite2,rewrite3,rewrite4,rewrite5] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "variables"),VPAnnotated (VPMetaVar "V2") (TName "defined-values")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "variables"),VPAnnotated (VPMetaVar "V2") (TName "values")] env rewriteTermTo (TApp "assign" [TVar "V1",TVar "V2"]) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I1") (TName "ids"),VPAnnotated (VPSeqVar "V1*" StarOp) (TSortSeq (TName "defined-values") StarOp)],PADT "datatype-value" [VPAnnotated (VPMetaVar "I2") (TName "ids"),VPAnnotated (VPSeqVar "V2*" StarOp) (TSortSeq (TName "defined-values") StarOp)]] env + 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 - 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 "none"]) 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 - env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TName "values",TName "values"]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TName "values",TName "values"])] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])] env env <- sideCondition (SCEquality (TApp "dom" [TVar "M1"]) (TSet [])) env rewriteTermTo (TApp "check-true" [TApp "is-equal" [TApp "dom" [TVar "M2"],TSet []]]) env rewrite4 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TName "values",TName "values"]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TName "values",TName "values"])] env - env <- sideCondition (SCPatternMatch (TApp "some-element" [TApp "dom" [TVar "M1"]]) (VPMetaVar "K")) env - rewriteTermTo (TApp "sequential" [TApp "check-true" [TApp "is-in-set" [TVar "K",TApp "dom" [TVar "M2"]]],TApp "structural-assign" [TApp "lookup" [TVar "M1",TVar "K"],TApp "lookup" [TVar "M2",TVar "K"]],TApp "structural-assign" [TApp "map-delete" [TVar "M1",TSet [TVar "K"]],TApp "map-delete" [TVar "M2",TSet [TVar "K"]]]]) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])] env + env <- sideCondition (SCPatternMatch (TApp "some-element" [TApp "dom" [TVar "M1"]]) [VPMetaVar "K"]) env + rewriteTermTo (TApp "sequential" [TApp "check-true" [TApp "is-in-set" [TVar "K",TApp "dom" [TVar "M2"]]],TApp "structural-assign" [TApp "map-lookup" [TVar "M1",TVar "K"],TApp "map-lookup" [TVar "M2",TVar "K"]],TApp "structural-assign" [TApp "map-delete" [TVar "M1",TSet [TVar "K"]],TApp "map-delete" [TVar "M2",TSet [TVar "K"]]]]) env rewrite5 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "defined-values"),VPAnnotated (VPMetaVar "V2") (TName "defined-values")] env - env <- sideCondition (SCIsInSort (TVar "V1") (TSortComplement (TSortUnion (TName "variables") (TApp "maps" [TName "values",TName "values"])))) env + 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 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 @@ -212,26 +213,18 @@ rewriteTermTo (TApp "assigned" [TVar "Var"]) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I") (TName "ids"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "defined-values") StarOp)]] env + 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 rewriteTermTo (TApp "datatype-value" [TVar "I",TApp "interleave-map" [TApp "structural-assigned" [TName "given"],TVar "V*"]]) env rewrite3 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "M") (TApp "maps" [TName "values",TName "values"])] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "M") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])] env rewriteTermTo (TApp "map" [TApp "interleave-map" [TApp "structural-assigned" [TName "given"],TApp "map-elements" [TVar "M"]]]) env 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" [TName "values",TName "values"])))) env + env <- sideCondition (SCIsInSort (TVar "U") (TSortComplement (TSortUnion (TName "variables") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])))) env rewriteTermTo (TVar "U") env - -current_value_ fargs = FApp "current-value" (fargs) -stepCurrent_value fargs = - evalRules [rewrite1] [] - where rewrite1 = do - let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "defined-values")] env - rewriteTermTo (TApp "def" [TApp "structural-assigned" [TVar "V"]]) env variables_ = FName "variables" stepVariables = rewriteType "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 @@ -9,37 +9,38 @@ module Funcons.Core.Computations.Normal.Binding.Binding, module Funcons.Core.Computations.Abnormal.Abrupting.Abrupting, module Funcons.Core.Computations.Abnormal.Returning.Returning, + module Funcons.Core.Computations.Abnormal.Controlling.Controlling, module Funcons.Core.Computations.Abnormal.Throwing.Throwing, module Funcons.Core.Computations.Abnormal.Failing.Failing, module Funcons.Core.Computations.Abnormal.Sticking, module Funcons.Core.Computations.Abnormal.Breaking.Breaking, module Funcons.Core.Computations.Abnormal.Continuing.Continuing, - module Funcons.Core.Computations.Abnormal.Controlling.Controlling, - module Funcons.Core.Values.ValueTypes.ValueTypes, --- module Funcons.Core.Values.Composite.Sets, - module Funcons.Core.Values.Composite.Bits.Bits, - module Funcons.Core.Values.Composite.Strings.Strings, - module Funcons.Core.Values.Composite.Datatypes.Datatypes, - module Funcons.Core.Values.Composite.Lists.Lists, --- module Funcons.Core.Values.Composite.Multisets, - module Funcons.Core.Values.Composite.Sequences.Sequences, - module Funcons.Core.Values.Composite.Variants.Variants, + module Funcons.Core.Values.Composite.Maps.Maps, module Funcons.Core.Values.Composite.Records.Records, --- module Funcons.Core.Values.Composite.Maps, - module Funcons.Core.Values.Composite.Vectors.Vectors, - module Funcons.Core.Values.Composite.Tuples.Tuples, + module Funcons.Core.Values.Composite.Strings.Strings, module Funcons.Core.Values.Composite.References.References, module Funcons.Core.Values.Composite.Graphs.Graphs, + module Funcons.Core.Values.Composite.Vectors.Vectors, + module Funcons.Core.Values.Composite.Variants.Variants, + module Funcons.Core.Values.Composite.Trees.Trees, + module Funcons.Core.Values.Composite.Sequences.Sequences, + module Funcons.Core.Values.Composite.Lists.Lists, + module Funcons.Core.Values.Composite.Classes.Classes, + module Funcons.Core.Values.Composite.Objects.Objects, + module Funcons.Core.Values.Composite.Datatypes.Datatypes, + module Funcons.Core.Values.Composite.Tuples.Tuples, + module Funcons.Core.Values.Composite.Bits.Bits, module Funcons.Core.Values.Primitive.Floats.Floats, - module Funcons.Core.Values.Primitive.Integers.Integers, - module Funcons.Core.Values.Primitive.Unit.Unit, module Funcons.Core.Values.Primitive.Booleans.Booleans, + module Funcons.Core.Values.Primitive.Null.Null, module Funcons.Core.Values.Primitive.Characters.Characters, - module Funcons.Core.Values.Abstraction.Functions.Functions, + module Funcons.Core.Values.Primitive.Integers.Integers, + module Funcons.Core.Values.ValueTypes.ValueTypes, + module Funcons.Core.Values.Abstraction.Thunks.Thunks, module Funcons.Core.Values.Abstraction.Patterns.Patterns, + module Funcons.Core.Values.Abstraction.Functions.Functions, module Funcons.Core.Values.Abstraction.Generic.Generic, - module Funcons.Core.Values.Abstraction.Thunks.Thunks, - ) where + ) where import Funcons.EDSL import Funcons.Core.Computations.Normal.Interacting.Interacting hiding (funcons,types,entities) import qualified Funcons.Core.Computations.Normal.Interacting.Interacting @@ -59,6 +60,8 @@ import qualified Funcons.Core.Computations.Abnormal.Abrupting.Abrupting import Funcons.Core.Computations.Abnormal.Returning.Returning hiding (funcons,types,entities) import qualified Funcons.Core.Computations.Abnormal.Returning.Returning +import Funcons.Core.Computations.Abnormal.Controlling.Controlling hiding (funcons,types,entities) +import qualified Funcons.Core.Computations.Abnormal.Controlling.Controlling import Funcons.Core.Computations.Abnormal.Throwing.Throwing hiding (funcons,types,entities) import qualified Funcons.Core.Computations.Abnormal.Throwing.Throwing import Funcons.Core.Computations.Abnormal.Failing.Failing hiding (funcons,types,entities) @@ -69,56 +72,56 @@ 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.Computations.Abnormal.Controlling.Controlling hiding (funcons,types,entities) -import qualified Funcons.Core.Computations.Abnormal.Controlling.Controlling -import Funcons.Core.Values.ValueTypes.ValueTypes hiding (funcons,types,entities) -import qualified Funcons.Core.Values.ValueTypes.ValueTypes ---import Funcons.Core.Values.Composite.Sets hiding (funcons,types,entities) ---import qualified Funcons.Core.Values.Composite.Sets -import Funcons.Core.Values.Composite.Bits.Bits hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Bits.Bits -import Funcons.Core.Values.Composite.Strings.Strings hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Strings.Strings -import Funcons.Core.Values.Composite.Datatypes.Datatypes hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Datatypes.Datatypes -import Funcons.Core.Values.Composite.Lists.Lists hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Lists.Lists ---import Funcons.Core.Values.Composite.Multisets hiding (funcons,types,entities) ---import qualified Funcons.Core.Values.Composite.Multisets ---import Funcons.Core.Values.Composite.Sequences.Sequences hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Sequences.Sequences -import Funcons.Core.Values.Composite.Variants.Variants hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Variants.Variants +import Funcons.Core.Values.Composite.Maps.Maps hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Maps.Maps import Funcons.Core.Values.Composite.Records.Records hiding (funcons,types,entities) import qualified Funcons.Core.Values.Composite.Records.Records ---import Funcons.Core.Values.Composite.Maps hiding (funcons,types,entities) ---import qualified Funcons.Core.Values.Composite.Maps -import Funcons.Core.Values.Composite.Vectors.Vectors hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Vectors.Vectors -import Funcons.Core.Values.Composite.Tuples.Tuples hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Composite.Tuples.Tuples +import Funcons.Core.Values.Composite.Strings.Strings hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Strings.Strings import Funcons.Core.Values.Composite.References.References hiding (funcons,types,entities) import qualified Funcons.Core.Values.Composite.References.References import Funcons.Core.Values.Composite.Graphs.Graphs hiding (funcons,types,entities) import qualified Funcons.Core.Values.Composite.Graphs.Graphs +import Funcons.Core.Values.Composite.Vectors.Vectors hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Vectors.Vectors +import Funcons.Core.Values.Composite.Variants.Variants hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Variants.Variants +import Funcons.Core.Values.Composite.Trees.Trees hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Trees.Trees +import Funcons.Core.Values.Composite.Sequences.Sequences hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Sequences.Sequences +import Funcons.Core.Values.Composite.Lists.Lists hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Lists.Lists +import Funcons.Core.Values.Composite.Classes.Classes hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Classes.Classes +import Funcons.Core.Values.Composite.Objects.Objects hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Objects.Objects +import Funcons.Core.Values.Composite.Datatypes.Datatypes hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Datatypes.Datatypes +import Funcons.Core.Values.Composite.Tuples.Tuples hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Tuples.Tuples +import Funcons.Core.Values.Composite.Bits.Bits hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Composite.Bits.Bits import Funcons.Core.Values.Primitive.Floats.Floats hiding (funcons,types,entities) import qualified Funcons.Core.Values.Primitive.Floats.Floats -import Funcons.Core.Values.Primitive.Integers.Integers hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Primitive.Integers.Integers -import Funcons.Core.Values.Primitive.Unit.Unit hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Primitive.Unit.Unit import Funcons.Core.Values.Primitive.Booleans.Booleans hiding (funcons,types,entities) import qualified Funcons.Core.Values.Primitive.Booleans.Booleans +import Funcons.Core.Values.Primitive.Null.Null hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Primitive.Null.Null import Funcons.Core.Values.Primitive.Characters.Characters hiding (funcons,types,entities) import qualified Funcons.Core.Values.Primitive.Characters.Characters -import Funcons.Core.Values.Abstraction.Functions.Functions hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Abstraction.Functions.Functions +import Funcons.Core.Values.Primitive.Integers.Integers hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Primitive.Integers.Integers +import Funcons.Core.Values.ValueTypes.ValueTypes hiding (funcons,types,entities) +import qualified Funcons.Core.Values.ValueTypes.ValueTypes +import Funcons.Core.Values.Abstraction.Thunks.Thunks hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Abstraction.Thunks.Thunks import Funcons.Core.Values.Abstraction.Patterns.Patterns hiding (funcons,types,entities) import qualified Funcons.Core.Values.Abstraction.Patterns.Patterns +import Funcons.Core.Values.Abstraction.Functions.Functions hiding (funcons,types,entities) +import qualified Funcons.Core.Values.Abstraction.Functions.Functions import Funcons.Core.Values.Abstraction.Generic.Generic hiding (funcons,types,entities) import qualified Funcons.Core.Values.Abstraction.Generic.Generic -import Funcons.Core.Values.Abstraction.Thunks.Thunks hiding (funcons,types,entities) -import qualified Funcons.Core.Values.Abstraction.Thunks.Thunks funcons = libUnions [ Funcons.Core.Computations.Normal.Interacting.Interacting.funcons @@ -130,38 +133,39 @@ , Funcons.Core.Computations.Normal.Binding.Binding.funcons , Funcons.Core.Computations.Abnormal.Abrupting.Abrupting.funcons , Funcons.Core.Computations.Abnormal.Returning.Returning.funcons + , Funcons.Core.Computations.Abnormal.Controlling.Controlling.funcons , Funcons.Core.Computations.Abnormal.Throwing.Throwing.funcons , Funcons.Core.Computations.Abnormal.Failing.Failing.funcons , Funcons.Core.Computations.Abnormal.Sticking.funcons , Funcons.Core.Computations.Abnormal.Breaking.Breaking.funcons , Funcons.Core.Computations.Abnormal.Continuing.Continuing.funcons - , Funcons.Core.Computations.Abnormal.Controlling.Controlling.funcons - , Funcons.Core.Values.ValueTypes.ValueTypes.funcons --- , Funcons.Core.Values.Composite.Sets.funcons - , Funcons.Core.Values.Composite.Bits.Bits.funcons - , Funcons.Core.Values.Composite.Strings.Strings.funcons - , Funcons.Core.Values.Composite.Datatypes.Datatypes.funcons - , Funcons.Core.Values.Composite.Lists.Lists.funcons --- , Funcons.Core.Values.Composite.Multisets.funcons - , Funcons.Core.Values.Composite.Sequences.Sequences.funcons - , Funcons.Core.Values.Composite.Variants.Variants.funcons + , Funcons.Core.Values.Composite.Maps.Maps.funcons , Funcons.Core.Values.Composite.Records.Records.funcons --- , Funcons.Core.Values.Composite.Maps.funcons - , Funcons.Core.Values.Composite.Vectors.Vectors.funcons - , Funcons.Core.Values.Composite.Tuples.Tuples.funcons + , Funcons.Core.Values.Composite.Strings.Strings.funcons , Funcons.Core.Values.Composite.References.References.funcons , Funcons.Core.Values.Composite.Graphs.Graphs.funcons + , Funcons.Core.Values.Composite.Vectors.Vectors.funcons + , Funcons.Core.Values.Composite.Variants.Variants.funcons + , Funcons.Core.Values.Composite.Trees.Trees.funcons + , Funcons.Core.Values.Composite.Sequences.Sequences.funcons + , Funcons.Core.Values.Composite.Lists.Lists.funcons + , Funcons.Core.Values.Composite.Classes.Classes.funcons + , Funcons.Core.Values.Composite.Objects.Objects.funcons + , Funcons.Core.Values.Composite.Datatypes.Datatypes.funcons + , Funcons.Core.Values.Composite.Tuples.Tuples.funcons + , Funcons.Core.Values.Composite.Bits.Bits.funcons , Funcons.Core.Values.Primitive.Floats.Floats.funcons - , Funcons.Core.Values.Primitive.Integers.Integers.funcons - , Funcons.Core.Values.Primitive.Unit.Unit.funcons , Funcons.Core.Values.Primitive.Booleans.Booleans.funcons + , Funcons.Core.Values.Primitive.Null.Null.funcons , Funcons.Core.Values.Primitive.Characters.Characters.funcons - , Funcons.Core.Values.Abstraction.Functions.Functions.funcons + , Funcons.Core.Values.Primitive.Integers.Integers.funcons + , Funcons.Core.Values.ValueTypes.ValueTypes.funcons + , Funcons.Core.Values.Abstraction.Thunks.Thunks.funcons , Funcons.Core.Values.Abstraction.Patterns.Patterns.funcons + , Funcons.Core.Values.Abstraction.Functions.Functions.funcons , Funcons.Core.Values.Abstraction.Generic.Generic.funcons - , Funcons.Core.Values.Abstraction.Thunks.Thunks.funcons ] -entities = concat +entities = concat [ Funcons.Core.Computations.Normal.Interacting.Interacting.entities , Funcons.Core.Computations.Normal.Flowing.Flowing.entities @@ -172,38 +176,39 @@ , Funcons.Core.Computations.Normal.Binding.Binding.entities , Funcons.Core.Computations.Abnormal.Abrupting.Abrupting.entities , Funcons.Core.Computations.Abnormal.Returning.Returning.entities + , Funcons.Core.Computations.Abnormal.Controlling.Controlling.entities , Funcons.Core.Computations.Abnormal.Throwing.Throwing.entities , Funcons.Core.Computations.Abnormal.Failing.Failing.entities , Funcons.Core.Computations.Abnormal.Sticking.entities , Funcons.Core.Computations.Abnormal.Breaking.Breaking.entities , Funcons.Core.Computations.Abnormal.Continuing.Continuing.entities - , Funcons.Core.Computations.Abnormal.Controlling.Controlling.entities - , Funcons.Core.Values.ValueTypes.ValueTypes.entities --- , Funcons.Core.Values.Composite.Sets.entities - , Funcons.Core.Values.Composite.Bits.Bits.entities - , Funcons.Core.Values.Composite.Strings.Strings.entities - , Funcons.Core.Values.Composite.Datatypes.Datatypes.entities - , Funcons.Core.Values.Composite.Lists.Lists.entities --- , Funcons.Core.Values.Composite.Multisets.entities - , Funcons.Core.Values.Composite.Sequences.Sequences.entities - , Funcons.Core.Values.Composite.Variants.Variants.entities + , Funcons.Core.Values.Composite.Maps.Maps.entities , Funcons.Core.Values.Composite.Records.Records.entities --- , Funcons.Core.Values.Composite.Maps.entities - , Funcons.Core.Values.Composite.Vectors.Vectors.entities - , Funcons.Core.Values.Composite.Tuples.Tuples.entities + , Funcons.Core.Values.Composite.Strings.Strings.entities , Funcons.Core.Values.Composite.References.References.entities , Funcons.Core.Values.Composite.Graphs.Graphs.entities + , Funcons.Core.Values.Composite.Vectors.Vectors.entities + , Funcons.Core.Values.Composite.Variants.Variants.entities + , Funcons.Core.Values.Composite.Trees.Trees.entities + , Funcons.Core.Values.Composite.Sequences.Sequences.entities + , Funcons.Core.Values.Composite.Lists.Lists.entities + , Funcons.Core.Values.Composite.Classes.Classes.entities + , Funcons.Core.Values.Composite.Objects.Objects.entities + , Funcons.Core.Values.Composite.Datatypes.Datatypes.entities + , Funcons.Core.Values.Composite.Tuples.Tuples.entities + , Funcons.Core.Values.Composite.Bits.Bits.entities , Funcons.Core.Values.Primitive.Floats.Floats.entities - , Funcons.Core.Values.Primitive.Integers.Integers.entities - , Funcons.Core.Values.Primitive.Unit.Unit.entities , Funcons.Core.Values.Primitive.Booleans.Booleans.entities + , Funcons.Core.Values.Primitive.Null.Null.entities , Funcons.Core.Values.Primitive.Characters.Characters.entities - , Funcons.Core.Values.Abstraction.Functions.Functions.entities + , Funcons.Core.Values.Primitive.Integers.Integers.entities + , Funcons.Core.Values.ValueTypes.ValueTypes.entities + , Funcons.Core.Values.Abstraction.Thunks.Thunks.entities , Funcons.Core.Values.Abstraction.Patterns.Patterns.entities + , Funcons.Core.Values.Abstraction.Functions.Functions.entities , Funcons.Core.Values.Abstraction.Generic.Generic.entities - , Funcons.Core.Values.Abstraction.Thunks.Thunks.entities ] -types = typeEnvUnions +types = typeEnvUnions [ Funcons.Core.Computations.Normal.Interacting.Interacting.types , Funcons.Core.Computations.Normal.Flowing.Flowing.types @@ -214,34 +219,35 @@ , Funcons.Core.Computations.Normal.Binding.Binding.types , Funcons.Core.Computations.Abnormal.Abrupting.Abrupting.types , Funcons.Core.Computations.Abnormal.Returning.Returning.types + , Funcons.Core.Computations.Abnormal.Controlling.Controlling.types , Funcons.Core.Computations.Abnormal.Throwing.Throwing.types , Funcons.Core.Computations.Abnormal.Failing.Failing.types , Funcons.Core.Computations.Abnormal.Sticking.types , Funcons.Core.Computations.Abnormal.Breaking.Breaking.types , Funcons.Core.Computations.Abnormal.Continuing.Continuing.types - , Funcons.Core.Computations.Abnormal.Controlling.Controlling.types - , Funcons.Core.Values.ValueTypes.ValueTypes.types --- , Funcons.Core.Values.Composite.Sets.types - , Funcons.Core.Values.Composite.Bits.Bits.types - , Funcons.Core.Values.Composite.Strings.Strings.types - , Funcons.Core.Values.Composite.Datatypes.Datatypes.types - , Funcons.Core.Values.Composite.Lists.Lists.types --- , Funcons.Core.Values.Composite.Multisets.types - , Funcons.Core.Values.Composite.Sequences.Sequences.types - , Funcons.Core.Values.Composite.Variants.Variants.types + , Funcons.Core.Values.Composite.Maps.Maps.types , Funcons.Core.Values.Composite.Records.Records.types --- , Funcons.Core.Values.Composite.Maps.types - , Funcons.Core.Values.Composite.Vectors.Vectors.types - , Funcons.Core.Values.Composite.Tuples.Tuples.types + , Funcons.Core.Values.Composite.Strings.Strings.types , Funcons.Core.Values.Composite.References.References.types , Funcons.Core.Values.Composite.Graphs.Graphs.types + , Funcons.Core.Values.Composite.Vectors.Vectors.types + , Funcons.Core.Values.Composite.Variants.Variants.types + , Funcons.Core.Values.Composite.Trees.Trees.types + , Funcons.Core.Values.Composite.Sequences.Sequences.types + , Funcons.Core.Values.Composite.Lists.Lists.types + , Funcons.Core.Values.Composite.Classes.Classes.types + , Funcons.Core.Values.Composite.Objects.Objects.types + , Funcons.Core.Values.Composite.Datatypes.Datatypes.types + , Funcons.Core.Values.Composite.Tuples.Tuples.types + , Funcons.Core.Values.Composite.Bits.Bits.types , Funcons.Core.Values.Primitive.Floats.Floats.types - , Funcons.Core.Values.Primitive.Integers.Integers.types - , Funcons.Core.Values.Primitive.Unit.Unit.types , Funcons.Core.Values.Primitive.Booleans.Booleans.types + , Funcons.Core.Values.Primitive.Null.Null.types , Funcons.Core.Values.Primitive.Characters.Characters.types - , Funcons.Core.Values.Abstraction.Functions.Functions.types + , Funcons.Core.Values.Primitive.Integers.Integers.types + , Funcons.Core.Values.ValueTypes.ValueTypes.types + , Funcons.Core.Values.Abstraction.Thunks.Thunks.types , Funcons.Core.Values.Abstraction.Patterns.Patterns.types + , Funcons.Core.Values.Abstraction.Functions.Functions.types , Funcons.Core.Values.Abstraction.Generic.Generic.types - , Funcons.Core.Values.Abstraction.Thunks.Thunks.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 @@ -5,11 +5,11 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList - [("functions",DataTypeMemberss "functions" [TPVar "DT",TPVar "T"] [DataTypeMemberConstructor "function" [TApp "abstractions" [TSortComputesFrom (TVar "DT") (TVar "T")]] (Just [TPVar "DT",TPVar "T"])])] + [("functions",DataTypeMemberss "functions" [TPVar "T",TPVar "T'"] [DataTypeMemberConstructor "function" [TApp "abstractions" [TSortComputesFrom (TVar "T") (TVar "T'")]] (Just [TPVar "T",TPVar "T'"])])] funcons = libFromList [("function",StrictFuncon stepFunction),("apply",StrictFuncon stepApply),("supply",StrictFuncon stepSupply),("compose",StrictFuncon stepCompose),("uncurry",StrictFuncon stepUncurry),("curry",StrictFuncon stepCurry),("partial-apply",StrictFuncon stepPartial_apply),("functions",StrictFuncon stepFunctions)] @@ -20,7 +20,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) 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 apply_ fargs = FApp "apply" (fargs) @@ -28,7 +28,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "function" [PADT "abstraction" [VPMetaVar "X"]],VPAnnotated (VPMetaVar "V") (TName "defined-values")] env + env <- vsMatch fargs [PADT "function" [PADT "abstraction" [VPMetaVar "X"]],VPAnnotated (VPMetaVar "V") (TName "values")] env rewriteTermTo (TApp "give" [TVar "V",TVar "X"]) env supply_ fargs = FApp "supply" (fargs) @@ -36,7 +36,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "function" [PADT "abstraction" [VPMetaVar "X"]],VPAnnotated (VPMetaVar "V") (TName "defined-values")] env + env <- vsMatch fargs [PADT "function" [PADT "abstraction" [VPMetaVar "X"]],VPAnnotated (VPMetaVar "V") (TName "values")] env rewriteTermTo (TApp "thunk" [TApp "abstraction" [TApp "give" [TVar "V",TVar "X"]]]) env compose_ fargs = FApp "compose" (fargs) @@ -52,15 +52,15 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "F") (TApp "functions" [TName "defined-values",TApp "functions" [TName "defined-values",TName "values"]])] env - rewriteTermTo (TApp "function" [TApp "abstraction" [TApp "apply" [TApp "apply" [TVar "F",TApp "def" [TApp "index" [TFuncon (FValue (Nat 1)),TApp "tuple-elements" [TName "given"]]]],TApp "def" [TApp "index" [TFuncon (FValue (Nat 2)),TApp "tuple-elements" [TName "given"]]]]]]) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "F") (TApp "functions" [TName "values",TApp "functions" [TName "values",TName "values"]])] env + rewriteTermTo (TApp "function" [TApp "abstraction" [TApp "apply" [TApp "apply" [TVar "F",TApp "checked" [TApp "index" [TFuncon (FValue (Nat 1)),TApp "tuple-elements" [TName "given"]]]],TApp "checked" [TApp "index" [TFuncon (FValue (Nat 2)),TApp "tuple-elements" [TName "given"]]]]]]) env curry_ fargs = FApp "curry" (fargs) stepCurry fargs = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "F") (TApp "functions" [TApp "tuples" [TName "defined-values",TName "defined-values"],TName "values"])] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "F") (TApp "functions" [TApp "tuples" [TName "values",TName "values"],TName "values"])] env rewriteTermTo (TApp "function" [TApp "abstraction" [TApp "partial-apply" [TVar "F",TName "given"]]]) env partial_apply_ fargs = FApp "partial-apply" (fargs) @@ -68,7 +68,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "F") (TApp "functions" [TApp "tuples" [TName "defined-values",TName "defined-values"],TName "values"]),VPAnnotated (VPMetaVar "V") (TName "defined-values")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "F") (TApp "functions" [TApp "tuples" [TName "values",TName "values"],TName "values"]),VPAnnotated (VPMetaVar "V") (TName "values")] env rewriteTermTo (TApp "function" [TApp "abstraction" [TApp "apply" [TVar "F",TApp "tuple" [TVar "V",TName "given"]]]]) env functions_ = FApp "functions" 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 @@ -5,11 +5,11 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList - [("abstractions",DataTypeMemberss "abstractions" [TPWildCard] [DataTypeMemberConstructor "abstraction" [TSortComputesFrom (TVar "DT") (TVar "T")] (Just [TPComputesFrom (TPVar "DT") (TPVar "T")])])] + [("abstractions",DataTypeMemberss "abstractions" [TPWildCard] [DataTypeMemberConstructor "abstraction" [TSortComputesFrom (TVar "T?") (TVar "T")] (Just [TPComputesFrom (TPVar "T?") (TPVar "T")])])] funcons = libFromList [("abstraction",NonStrictFuncon stepAbstraction),("closure",NonStrictFuncon stepClosure),("enact",StrictFuncon stepEnact),("abstractions",StrictFuncon stepAbstractions)] @@ -28,7 +28,7 @@ where step1 = do let env = emptyEnv env <- lifted_fsMatch fargs [PMetaVar "X"] env - env <- getInhPatt "environment" (VPMetaVar "Rho") env + env <- getInhPatt "environment" [VPMetaVar "Rho"] env stepTermTo (TApp "abstraction" [TApp "closed" [TApp "scope" [TVar "Rho",TVar "X"]]]) env enact_ fargs = FApp "enact" (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 @@ -5,11 +5,11 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList - [("patterns",DataTypeMemberss "patterns" [] [DataTypeMemberConstructor "pattern" [TApp "abstractions" [TSortComputesFrom (TName "defined-values") (TName "environments")]] (Just [])])] + [("patterns",DataTypeMemberss "patterns" [] [DataTypeMemberConstructor "pattern" [TApp "abstractions" [TSortComputesFrom (TName "values") (TName "environments")]] (Just [])])] funcons = libFromList [("pattern",StrictFuncon stepPattern),("pattern-any",NullaryFuncon stepPattern_any),("pattern-bind",StrictFuncon stepPattern_bind),("pattern-type",NonStrictFuncon stepPattern_type),("pattern-else",StrictFuncon stepPattern_else),("pattern-unite",StrictFuncon stepPattern_unite),("match",StrictFuncon stepMatch),("match-loosely",StrictFuncon stepMatch_loosely),("case-match",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepCase_match),("case-match-loosely",PartiallyStrictFuncon [Strict,NonStrict] NonStrict stepCase_match_loosely),("case-variant-value",StrictFuncon stepCase_variant_value),("patterns",NullaryFuncon stepPatterns)] @@ -20,7 +20,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) 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 pattern_any_ = FName "pattern-any" @@ -34,23 +34,23 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "I") (TName "ids")] env - rewriteTermTo (TApp "pattern" [TApp "abstraction" [TApp "bind" [TVar "I",TName "given"]]]) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "I") (TName "identifiers")] env + rewriteTermTo (TApp "pattern" [TApp "abstraction" [TApp "bind-value" [TVar "I",TName "given"]]]) env pattern_type_ fargs = FApp "pattern-type" (fargs) stepPattern_type fargs = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "DT"] env - rewriteTermTo (TApp "pattern" [TApp "abstraction" [TApp "if-true-else" [TApp "is-in-type" [TName "given",TVar "DT"],TApp "map" [],TName "fail"]]]) env + env <- fsMatch fargs [PMetaVar "T"] env + rewriteTermTo (TApp "pattern" [TApp "abstraction" [TApp "if-true-else" [TApp "is-in-type" [TName "given",TVar "T"],TApp "map" [],TName "fail"]]]) env pattern_else_ fargs = FApp "pattern-else" (fargs) stepPattern_else fargs = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "P1") (TName "defined-values"),VPAnnotated (VPMetaVar "P2") (TName "defined-values")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "P1") (TName "values"),VPAnnotated (VPMetaVar "P2") (TName "values")] env rewriteTermTo (TApp "pattern" [TApp "abstraction" [TApp "else" [TApp "match" [TName "given",TVar "P1"],TApp "match" [TName "given",TVar "P2"]]]]) env pattern_unite_ fargs = FApp "pattern-unite" (fargs) @@ -58,7 +58,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "P1") (TName "defined-values"),VPAnnotated (VPMetaVar "P2") (TName "defined-values")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "P1") (TName "values"),VPAnnotated (VPMetaVar "P2") (TName "values")] env rewriteTermTo (TApp "pattern" [TApp "abstraction" [TApp "collateral" [TApp "match" [TName "given",TVar "P1"],TApp "match" [TName "given",TVar "P2"]]]]) env match_ fargs = FApp "match" (fargs) @@ -66,57 +66,57 @@ evalRules [rewrite1,rewrite2,rewrite3,rewrite4,rewrite5] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "DV") (TName "defined-values"),PADT "pattern" [PADT "abstraction" [VPMetaVar "X"]]] env - rewriteTermTo (TApp "give" [TVar "DV",TVar "X"]) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),PADT "pattern" [PADT "abstraction" [VPMetaVar "X"]]] env + rewriteTermTo (TApp "give" [TVar "V",TVar "X"]) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I1") (TName "ids"),VPAnnotated (VPSeqVar "V1*" StarOp) (TSortSeq (TName "values") StarOp)],PADT "datatype-value" [VPAnnotated (VPMetaVar "I2") (TName "ids"),VPAnnotated (VPSeqVar "V2*" StarOp) (TSortSeq (TName "values") StarOp)]] env + 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 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 - env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TName "values",TName "values"]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TName "values",TName "values"])] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])] env env <- sideCondition (SCEquality (TApp "dom" [TVar "M2"]) (TSet [])) env rewriteTermTo (TApp "if-true-else" [TApp "is-equal" [TApp "dom" [TVar "M1"],TSet []],TApp "map" [],TName "fail"]) env rewrite4 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TName "values",TName "values"]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TName "values",TName "values"])] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])] env env <- sideCondition (SCInequality (TApp "dom" [TVar "M2"]) (TSet [])) env - env <- sideCondition (SCPatternMatch (TApp "some-element" [TApp "dom" [TVar "M2"]]) (VPMetaVar "K")) env - rewriteTermTo (TApp "if-true-else" [TApp "is-in-set" [TVar "K",TApp "dom" [TVar "M1"]],TApp "collateral" [TApp "match" [TApp "lookup" [TVar "M1",TVar "K"],TApp "lookup" [TVar "M2",TVar "K"]],TApp "match" [TApp "map-delete" [TVar "M1",TSet [TVar "K"]],TApp "map-delete" [TVar "M2",TSet [TVar "K"]]]],TName "fail"]) env + env <- sideCondition (SCPatternMatch (TApp "some-element" [TApp "dom" [TVar "M2"]]) [VPMetaVar "K"]) env + rewriteTermTo (TApp "if-true-else" [TApp "is-in-set" [TVar "K",TApp "dom" [TVar "M1"]],TApp "collateral" [TApp "match" [TApp "map-lookup" [TVar "M1",TVar "K"],TApp "map-lookup" [TVar "M2",TVar "K"]],TApp "match" [TApp "map-delete" [TVar "M1",TSet [TVar "K"]],TApp "map-delete" [TVar "M2",TSet [TVar "K"]]]],TName "fail"]) env rewrite5 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "DV") (TName "defined-values"),VPAnnotated (VPMetaVar "P") (TName "defined-values")] env - env <- sideCondition (SCIsInSort (TVar "P") (TSortComplement (TSortUnion (TName "datatype-values") (TApp "maps" [TName "values",TName "values"])))) env - rewriteTermTo (TApp "if-true-else" [TApp "is-equal" [TVar "DV",TVar "P"],TApp "map" [],TName "fail"]) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "P") (TName "values")] env + env <- sideCondition (SCIsInSort (TVar "P") (TSortComplement (TSortUnion (TName "datatype-values") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])))) env + rewriteTermTo (TApp "if-true-else" [TApp "is-equal" [TVar "V",TVar "P"],TApp "map" [],TName "fail"]) env match_loosely_ fargs = FApp "match-loosely" (fargs) stepMatch_loosely fargs = evalRules [rewrite1,rewrite2,rewrite3,rewrite4,rewrite5] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "DV") (TName "defined-values"),PADT "pattern" [PADT "abstraction" [VPMetaVar "X"]]] env - rewriteTermTo (TApp "give" [TVar "DV",TVar "X"]) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),PADT "pattern" [PADT "abstraction" [VPMetaVar "X"]]] env + rewriteTermTo (TApp "give" [TVar "V",TVar "X"]) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I1") (TName "ids"),VPAnnotated (VPSeqVar "V1*" StarOp) (TSortSeq (TName "values") StarOp)],PADT "datatype-value" [VPAnnotated (VPMetaVar "I2") (TName "ids"),VPAnnotated (VPSeqVar "V2*" StarOp) (TSortSeq (TName "values") StarOp)]] env + 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 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 - env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TName "values",TName "values"]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TName "values",TName "values"])] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])] env env <- sideCondition (SCEquality (TApp "dom" [TVar "M2"]) (TSet [])) env rewriteTermTo (TApp "map" []) env rewrite4 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TName "values",TName "values"]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TName "values",TName "values"])] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "M1") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPMetaVar "M2") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])] env env <- sideCondition (SCInequality (TApp "dom" [TVar "M2"]) (TSet [])) env - env <- sideCondition (SCPatternMatch (TApp "some-element" [TApp "dom" [TVar "M2"]]) (VPMetaVar "K")) env - rewriteTermTo (TApp "if-true-else" [TApp "is-in-set" [TVar "K",TApp "dom" [TVar "M1"]],TApp "collateral" [TApp "match-loosely" [TApp "lookup" [TVar "M1",TVar "K"],TApp "lookup" [TVar "M2",TVar "K"]],TApp "match-loosely" [TApp "map-delete" [TVar "M1",TSet [TVar "K"]],TApp "map-delete" [TVar "M2",TSet [TVar "K"]]]],TName "fail"]) env + env <- sideCondition (SCPatternMatch (TApp "some-element" [TApp "dom" [TVar "M2"]]) [VPMetaVar "K"]) env + rewriteTermTo (TApp "if-true-else" [TApp "is-in-set" [TVar "K",TApp "dom" [TVar "M1"]],TApp "collateral" [TApp "match-loosely" [TApp "map-lookup" [TVar "M1",TVar "K"],TApp "map-lookup" [TVar "M2",TVar "K"]],TApp "match-loosely" [TApp "map-delete" [TVar "M1",TSet [TVar "K"]],TApp "map-delete" [TVar "M2",TSet [TVar "K"]]]],TName "fail"]) env rewrite5 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "DV") (TName "defined-values"),VPAnnotated (VPMetaVar "P") (TName "defined-values")] env - env <- sideCondition (SCIsInSort (TVar "P") (TSortComplement (TSortUnion (TName "datatype-values") (TApp "maps" [TName "values",TName "values"])))) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "DV") (TName "values"),VPAnnotated (VPMetaVar "P") (TName "values")] env + env <- sideCondition (SCIsInSort (TVar "P") (TSortComplement (TSortUnion (TName "datatype-values") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])))) env rewriteTermTo (TApp "if-true-else" [TApp "is-equal" [TVar "DV",TVar "P"],TApp "map" [],TName "fail"]) env case_match_ fargs = FApp "case-match" (fargs) @@ -124,7 +124,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PAnnotated (PMetaVar "P") (TName "defined-values"),PMetaVar "X"] env + env <- fsMatch fargs [PAnnotated (PMetaVar "P") (TName "values"),PMetaVar "X"] env rewriteTermTo (TApp "scope" [TApp "match" [TName "given",TVar "P"],TVar "X"]) env case_match_loosely_ fargs = FApp "case-match-loosely" (fargs) @@ -132,7 +132,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PAnnotated (PMetaVar "P") (TName "defined-values"),PMetaVar "X"] env + env <- fsMatch fargs [PAnnotated (PMetaVar "P") (TName "values"),PMetaVar "X"] env rewriteTermTo (TApp "scope" [TApp "match-loosely" [TName "given",TVar "P"],TVar "X"]) env case_variant_value_ fargs = FApp "case-variant-value" (fargs) @@ -140,7 +140,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "I") (TName "ids")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "I") (TName "identifiers")] env rewriteTermTo (TApp "case-match" [TApp "variant" [TVar "I",TName "pattern-any"],TApp "variant-value" [TName "given"]]) env patterns_ = FName "patterns" 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 @@ -5,11 +5,11 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList - [("thunks",DataTypeMemberss "thunks" [TPVar "T"] [DataTypeMemberConstructor "thunk" [TApp "abstractions" [TSortComputesFrom (TName "nothing") (TVar "T")]] (Just [TPVar "T"])])] + [("thunks",DataTypeMemberss "thunks" [TPVar "T"] [DataTypeMemberConstructor "thunk" [TApp "abstractions" [TSortComputesFrom (TName "null-type") (TVar "T")]] (Just [TPVar "T"])])] funcons = libFromList [("thunk",StrictFuncon stepThunk),("force",StrictFuncon stepForce),("thunks",StrictFuncon stepThunks)] @@ -20,7 +20,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) 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 force_ fargs = FApp "force" (fargs) @@ -29,7 +29,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [PADT "thunk" [PADT "abstraction" [VPMetaVar "X"]]] env - rewriteTermTo (TVar "X") env + rewriteTermTo (TApp "no-given" [TVar "X"]) env thunks_ = FApp "thunks" stepThunks ts = rewriteType "thunks" ts 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 @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -18,7 +18,7 @@ stepBits = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - rewriteTermTo (TName "bools") env + rewriteTermTo (TName "booleans") env bit_vector_ fargs = FApp "bit-vector" (fargs) stepBit_vector fargs = @@ -26,7 +26,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPSeqVar "_X1*" StarOp] env - env <- sideCondition (SCIsInSort (TVar "_X1*") (TSortSeq (TName "values") 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 bytes_ = FName "bytes" @@ -41,7 +41,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "nats")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "natural-numbers")] env rewriteTermTo (TApp "integer-subtract" [TApp "integer-power" [TFuncon (FValue (Nat 2)),TVar "N"],TFuncon (FValue (Nat 1))]) env signed_bit_vector_maximum_ fargs = FApp "signed-bit-vector-maximum" (fargs) @@ -49,7 +49,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "nats")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "natural-numbers")] env rewriteTermTo (TApp "integer-subtract" [TApp "integer-power" [TFuncon (FValue (Nat 2)),TApp "integer-subtract" [TVar "N",TFuncon (FValue (Nat 1))]],TFuncon (FValue (Nat 1))]) env signed_bit_vector_minimum_ fargs = FApp "signed-bit-vector-minimum" (fargs) @@ -57,7 +57,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "nats")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "natural-numbers")] env rewriteTermTo (TApp "integer-negate" [TApp "integer-power" [TFuncon (FValue (Nat 2)),TApp "integer-subtract" [TVar "N",TFuncon (FValue (Nat 1))]]]) env is_in_signed_bit_vector_ fargs = FApp "is-in-signed-bit-vector" (fargs) @@ -65,7 +65,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "M") (TName "integers"),VPAnnotated (VPMetaVar "N") (TName "nats")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "M") (TName "integers"),VPAnnotated (VPMetaVar "N") (TName "natural-numbers")] env rewriteTermTo (TApp "and" [TApp "integer-is-less-or-equal" [TVar "M",TApp "signed-bit-vector-maximum" [TVar "N"]],TApp "integer-is-greater-or-equal" [TVar "M",TApp "signed-bit-vector-minimum" [TVar "N"]]]) env is_in_unsigned_bit_vector_ fargs = FApp "is-in-unsigned-bit-vector" (fargs) @@ -73,7 +73,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "M") (TName "integers"),VPAnnotated (VPMetaVar "N") (TName "nats")] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "M") (TName "integers"),VPAnnotated (VPMetaVar "N") (TName "natural-numbers")] env rewriteTermTo (TApp "and" [TApp "integer-is-less-or-equal" [TVar "M",TApp "unsigned-bit-vector-maximum" [TVar "N"]],TApp "integer-is-greater-or-equal" [TVar "M",TFuncon (FValue (Nat 0))]]) env bit_vectors_ = FApp "bit-vectors" diff --git a/cbs/Funcons/Core/Values/Composite/Classes/Classes.hs b/cbs/Funcons/Core/Values/Composite/Classes/Classes.hs new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Values/Composite/Classes/Classes.hs @@ -0,0 +1,77 @@ +-- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Classes/Classes.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Values.Composite.Classes.Classes where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) +entities = [] + +types = typeEnvFromList + [("classes",DataTypeMemberss "classes" [] [DataTypeMemberConstructor "class" [TApp "thunks" [TApp "references" [TName "objects"]],TName "environments",TSortSeq (TName "identifiers") StarOp] (Just [])])] + +funcons = libFromList + [("class",StrictFuncon stepClass),("class-instantiator",StrictFuncon stepClass_instantiator),("class-feature-map",StrictFuncon stepClass_feature_map),("class-superclass-name-sequence",StrictFuncon stepClass_superclass_name_sequence),("class-name-tree",StrictFuncon stepClass_name_tree),("is-subclass-name",StrictFuncon stepIs_subclass_name),("class-name-single-inheritance-feature-map",StrictFuncon stepClass_name_single_inheritance_feature_map),("classes",NullaryFuncon stepClasses)] + +class_ fargs = FApp "class" (fargs) +stepClass fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPMetaVar "_X1",VPMetaVar "_X2",VPSeqVar "_X3*" StarOp] env + 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 + +class_instantiator_ fargs = FApp "class-instantiator" (fargs) +stepClass_instantiator fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "class" [VPAnnotated (VPMetaVar "Thunk") (TApp "thunks" [TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPMetaVar "Envs") (TName "environments"),VPAnnotated (VPSeqVar "C*" StarOp) (TSortSeq (TName "identifiers") StarOp)]] env + rewriteTermTo (TVar "Thunk") env + +class_feature_map_ fargs = FApp "class-feature-map" (fargs) +stepClass_feature_map fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "class" [VPAnnotated (VPMetaVar "Thunk") (TApp "thunks" [TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPMetaVar "Env") (TName "environments"),VPAnnotated (VPSeqVar "C*" StarOp) (TSortSeq (TName "identifiers") StarOp)]] env + rewriteTermTo (TVar "Env") env + +class_superclass_name_sequence_ fargs = FApp "class-superclass-name-sequence" (fargs) +stepClass_superclass_name_sequence fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "class" [VPAnnotated (VPMetaVar "Thunk") (TApp "thunks" [TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPMetaVar "Env") (TName "environments"),VPAnnotated (VPSeqVar "C*" StarOp) (TSortSeq (TName "identifiers") StarOp)]] env + rewriteTermTo (TVar "C*") env + +class_name_tree_ fargs = FApp "class-name-tree" (fargs) +stepClass_name_tree fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "C") (TName "identifiers")] env + rewriteTermTo (TApp "tree" [TVar "C",TApp "interleave-map" [TApp "class-name-tree" [TName "given"],TApp "class-superclass-name-sequence" [TApp "bound-value" [TVar "C"]]]]) env + +is_subclass_name_ fargs = FApp "is-subclass-name" (fargs) +stepIs_subclass_name fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "C") (TName "identifiers"),VPAnnotated (VPMetaVar "C'") (TName "identifiers")] env + rewriteTermTo (TApp "is-in-set" [TVar "C",TSet [TApp "forest-value-sequence" [TApp "class-name-tree" [TVar "C'"]]]]) env + +class_name_single_inheritance_feature_map_ fargs = FApp "class-name-single-inheritance-feature-map" (fargs) +stepClass_name_single_inheritance_feature_map fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "C") (TName "identifiers")] env + rewriteTermTo (TApp "map-override" [TApp "interleave-map" [TApp "class-feature-map" [TApp "bound-value" [TName "given"]],TApp "single-branching-sequence" [TApp "class-name-tree" [TVar "C"]]]]) env + +classes_ = FName "classes" +stepClasses = rewriteType "classes" [] diff --git a/cbs/Funcons/Core/Values/Composite/Datatypes/Datatypes.hs b/cbs/Funcons/Core/Values/Composite/Datatypes/Datatypes.hs --- a/cbs/Funcons/Core/Values/Composite/Datatypes/Datatypes.hs +++ b/cbs/Funcons/Core/Values/Composite/Datatypes/Datatypes.hs @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -19,7 +19,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I") (TName "ids"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env + env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I") (TName "identifiers"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)]] env rewriteTermTo (TVar "I") env datatype_value_elements_ fargs = FApp "datatype-value-elements" (fargs) @@ -27,5 +27,5 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated (VPMetaVar "I") (TName "ids"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env + env <- vsMatch fargs [PADT "datatype-value" [VPAnnotated VPWildCard (TName "identifiers"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env rewriteTermTo (TVar "V*") env diff --git a/cbs/Funcons/Core/Values/Composite/Graphs/Graphs.hs b/cbs/Funcons/Core/Values/Composite/Graphs/Graphs.hs --- a/cbs/Funcons/Core/Values/Composite/Graphs/Graphs.hs +++ b/cbs/Funcons/Core/Values/Composite/Graphs/Graphs.hs @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -19,5 +19,5 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "GVT"] env - rewriteTermTo (TApp "maps" [TVar "GVT",TApp "sets" [TVar "GVT"]]) env + env <- fsMatch fargs [PMetaVar "GT"] env + rewriteTermTo (TApp "maps" [TVar "GT",TApp "sets" [TVar "GT"]]) env 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 @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -20,7 +20,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPSeqVar "_X1*" StarOp] env - env <- sideCondition (SCIsInSort (TVar "_X1*") (TSortSeq (TName "values") 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 list_elements_ fargs = FApp "list-elements" (fargs) @@ -53,12 +53,12 @@ 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 "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env + 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 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 - rewriteTermTo (TName "none") env + rewriteTermTo (TSeq []) env list_tail_ fargs = FApp "list-tail" (fargs) tail_ fargs = FApp "list-tail" (fargs) @@ -66,12 +66,12 @@ 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 "V*" StarOp) (TSortSeq (TName "values") StarOp)]] env + 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 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 - rewriteTermTo (TName "none") env + rewriteTermTo (TSeq []) env list_length_ fargs = FApp "list-length" (fargs) stepList_length fargs = @@ -90,7 +90,7 @@ rewriteTermTo (TApp "list" [TVar "V1*",TVar "V2*"]) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "L1") (TApp "lists" [TName "values"]),VPAnnotated (VPMetaVar "L2") (TApp "lists" [TName "values"]),VPAnnotated (VPMetaVar "L3") (TApp "lists" [TName "values"]),VPAnnotated (VPSeqVar "L*" StarOp) (TSortSeq (TApp "lists" [TName "values"]) StarOp)] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "L1") (TApp "lists" [TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPMetaVar "L2") (TApp "lists" [TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPMetaVar "L3") (TApp "lists" [TSortSeq (TName "values") QuestionMarkOp]),VPAnnotated (VPSeqVar "L*" StarOp) (TSortSeq (TApp "lists" [TSortSeq (TName "values") QuestionMarkOp]) StarOp)] env rewriteTermTo (TApp "list-append" [TVar "L1",TApp "list-append" [TVar "L2",TVar "L3",TVar "L*"]]) env rewrite3 = do let env = emptyEnv @@ -98,7 +98,7 @@ rewriteTermTo (TApp "list" []) env rewrite4 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "L") (TApp "lists" [TName "values"])] env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "L") (TApp "lists" [TSortSeq (TName "values") QuestionMarkOp])] env rewriteTermTo (TVar "L") env lists_ = FApp "lists" diff --git a/cbs/Funcons/Core/Values/Composite/Maps/Maps.hs b/cbs/Funcons/Core/Values/Composite/Maps/Maps.hs new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Values/Composite/Maps/Maps.hs @@ -0,0 +1,24 @@ +-- 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 new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Values/Composite/Objects/Objects.hs @@ -0,0 +1,78 @@ +-- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Objects/Objects.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Values.Composite.Objects.Objects where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) +entities = [] + +types = typeEnvFromList + [("objects",DataTypeMemberss "objects" [] [DataTypeMemberConstructor "object" [TName "atoms",TName "identifiers",TName "environments",TSortSeq (TName "objects") StarOp] (Just [])])] + +funcons = libFromList + [("object",StrictFuncon stepObject),("object-identity",StrictFuncon stepObject_identity),("object-class-name",StrictFuncon stepObject_class_name),("object-feature-map",StrictFuncon stepObject_feature_map),("object-subobject-sequence",StrictFuncon stepObject_subobject_sequence),("object-tree",StrictFuncon stepObject_tree),("object-single-inheritance-feature-map",StrictFuncon stepObject_single_inheritance_feature_map),("objects",NullaryFuncon stepObjects)] + +object_ fargs = FApp "object" (fargs) +stepObject fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPMetaVar "_X1",VPMetaVar "_X2",VPMetaVar "_X3",VPSeqVar "_X4*" StarOp] env + 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 (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 + +object_identity_ fargs = FApp "object-identity" (fargs) +stepObject_identity fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "object" [VPAnnotated (VPMetaVar "A") (TName "atoms"),VPAnnotated VPWildCard (TName "identifiers"),VPAnnotated VPWildCard (TName "environments"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "objects") StarOp)]] env + rewriteTermTo (TVar "A") env + +object_class_name_ fargs = FApp "object-class-name" (fargs) +stepObject_class_name fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "object" [VPAnnotated VPWildCard (TName "atoms"),VPAnnotated (VPMetaVar "C") (TName "identifiers"),VPAnnotated VPWildCard (TName "environments"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "objects") StarOp)]] env + rewriteTermTo (TVar "C") env + +object_feature_map_ fargs = FApp "object-feature-map" (fargs) +stepObject_feature_map fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "object" [VPAnnotated VPWildCard (TName "atoms"),VPAnnotated VPWildCard (TName "identifiers"),VPAnnotated (VPMetaVar "Env") (TName "environments"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "objects") StarOp)]] env + rewriteTermTo (TVar "Env") env + +object_subobject_sequence_ fargs = FApp "object-subobject-sequence" (fargs) +stepObject_subobject_sequence fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "object" [VPAnnotated VPWildCard (TName "atoms"),VPAnnotated VPWildCard (TName "identifiers"),VPAnnotated VPWildCard (TName "environments"),VPAnnotated (VPSeqVar "O*" StarOp) (TSortSeq (TName "objects") StarOp)]] env + rewriteTermTo (TVar "O*") env + +object_tree_ fargs = FApp "object-tree" (fargs) +stepObject_tree fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "O") (TName "objects")] env + rewriteTermTo (TApp "tree" [TVar "O",TApp "interleave-map" [TApp "object-tree" [TName "given"],TApp "object-subobject-sequence" [TVar "O"]]]) env + +object_single_inheritance_feature_map_ fargs = FApp "object-single-inheritance-feature-map" (fargs) +stepObject_single_inheritance_feature_map fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "O") (TName "objects")] env + rewriteTermTo (TApp "map-override" [TApp "left-to-right-map" [TApp "object-feature-map" [TName "given"],TApp "single-branching-sequence" [TApp "object-tree" [TVar "O"]]]]) env + +objects_ = FName "objects" +stepObjects = rewriteType "objects" [] 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 @@ -5,14 +5,14 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList - [("records",DataTypeMemberss "records" [TPVar "MIT"] [DataTypeMemberConstructor "record" [TApp "maps" [TName "ids",TName "values"]] (Just [TPVar "MIT"])])] + [("records",DataTypeMemberss "records" [TPVar "T"] [DataTypeMemberConstructor "record" [TApp "maps" [TName "identifiers",TVar "T"]] (Just [TPVar "T"])])] funcons = libFromList - [("record",StrictFuncon stepRecord),("record-select",StrictFuncon stepRecord_select),("records",StrictFuncon stepRecords)] + [("record",StrictFuncon stepRecord),("record-map",StrictFuncon stepRecord_map),("record-select",StrictFuncon stepRecord_select),("records",StrictFuncon stepRecords)] record_ fargs = FApp "record" (fargs) stepRecord fargs = @@ -20,16 +20,24 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) 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 +record_map_ fargs = FApp "record-map" (fargs) +stepRecord_map fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "record" [VPAnnotated (VPMetaVar "M") (TApp "maps" [TSortSeq (TName "values") QuestionMarkOp,TSortSeq (TName "values") QuestionMarkOp])]] env + rewriteTermTo (TVar "M") env + record_select_ fargs = FApp "record-select" (fargs) stepRecord_select fargs = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "record" [VPAnnotated (VPMetaVar "MIV") (TApp "maps" [TName "ids",TName "values"])],VPAnnotated (VPMetaVar "I") (TName "ids")] env - rewriteTermTo (TApp "lookup" [TVar "MIV",TVar "I"]) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "R") (TApp "records" [TName "values"]),VPAnnotated (VPMetaVar "I") (TName "identifiers")] env + rewriteTermTo (TApp "map-lookup" [TApp "record-map" [TVar "R"],TVar "I"]) env records_ = FApp "records" stepRecords ts = rewriteType "records" ts 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 @@ -5,14 +5,14 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList - [("references",DataTypeMemberss "references" [TPVar "VT"] [DataTypeMemberConstructor "reference" [TVar "VT"] (Just [TPVar "VT"])])] + [("references",DataTypeMemberss "references" [TPVar "T"] [DataTypeMemberConstructor "reference" [TVar "T"] (Just [TPVar "T"])]),("pointers",DataTypeMemberss "pointers" [TPVar "T"] [DataTypeInclusionn (TApp "references" [TVar "T"]),DataTypeMemberConstructor "pointer-null" [] (Just [TPVar "T"])])] funcons = libFromList - [("reference",StrictFuncon stepReference),("pointers",NonStrictFuncon stepPointers),("dereference",StrictFuncon stepDereference),("references",StrictFuncon stepReferences)] + [("reference",StrictFuncon stepReference),("pointer-null",NullaryFuncon stepPointer_null),("dereference",StrictFuncon stepDereference),("references",StrictFuncon stepReferences),("pointers",StrictFuncon stepPointers)] reference_ fargs = FApp "reference" (fargs) stepReference fargs = @@ -20,28 +20,29 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) 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 -pointers_ fargs = FApp "pointers" (fargs) -stepPointers fargs = - evalRules [rewrite1] [] +pointer_null_ = FName "pointer-null" +stepPointer_null = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- fsMatch fargs [PMetaVar "VT"] env - rewriteTermTo (TSortUnion (TName "unit-type") (TApp "references" [TVar "VT"])) env + 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 dereference_ fargs = FApp "dereference" (fargs) stepDereference fargs = evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "reference" [VPAnnotated (VPMetaVar "DV") (TName "defined-values")]] env - rewriteTermTo (TVar "DV") env + env <- vsMatch fargs [PADT "reference" [VPAnnotated (VPMetaVar "V") (TName "values")]] env + rewriteTermTo (TVar "V") env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "null-value" []] env - rewriteTermTo (TName "none") env + env <- vsMatch fargs [PADT "pointer-null" []] env + rewriteTermTo (TSeq []) env references_ = FApp "references" stepReferences ts = rewriteType "references" ts + +pointers_ = FApp "pointers" +stepPointers ts = rewriteType "pointers" ts 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 @@ -5,14 +5,14 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList [] funcons = libFromList - [("length",StrictFuncon stepLength),("index",StrictFuncon stepIndex),("first",StrictFuncon stepFirst),("second",StrictFuncon stepSecond),("third",StrictFuncon stepThird),("is-in",StrictFuncon stepIs_in),("first-n",StrictFuncon stepFirst_n),("drop-first-n",StrictFuncon stepDrop_first_n),("reverse",StrictFuncon stepReverse),("n-of",StrictFuncon stepN_of),("intersperse",StrictFuncon stepIntersperse),("filter-defined",StrictFuncon stepFilter_defined)] + [("length",StrictFuncon stepLength),("is-in",StrictFuncon stepIs_in),("index",StrictFuncon stepIndex),("first",StrictFuncon stepFirst),("second",StrictFuncon stepSecond),("third",StrictFuncon stepThird),("first-n",StrictFuncon stepFirst_n),("drop-first-n",StrictFuncon stepDrop_first_n),("reverse",StrictFuncon stepReverse),("n-of",StrictFuncon stepN_of),("intersperse",StrictFuncon stepIntersperse)] length_ fargs = FApp "length" (fargs) stepLength fargs = @@ -24,81 +24,81 @@ rewrite2 = do let env = emptyEnv env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - rewriteTermTo (TApp "nat-succ" [TApp "length" [TVar "V*"]]) env + rewriteTermTo (TApp "natural-successor" [TApp "length" [TVar "V*"]]) env +is_in_ fargs = FApp "is-in" (fargs) +stepIs_in fargs = + evalRules [rewrite1,rewrite2] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "V'") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env + rewriteTermTo (TApp "or" [TApp "is-equal" [TVar "V",TVar "V'"],TApp "is-in" [TVar "V",TVar "V*"]]) env + rewrite2 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values")] env + rewriteTermTo (TName "false") env + index_ fargs = FApp "index" (fargs) stepIndex fargs = evalRules [rewrite1,rewrite2,rewrite3,rewrite4] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPLit (Nat 1),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env + env <- vsMatch fargs [VPLit (Nat 1),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 [VPAnnotated (VPMetaVar "N") (TName "pos-ints"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - env <- sideCondition (SCPatternMatch (TApp "nat-pred" [TVar "N"]) (VPMetaVar "N'")) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "positive-integers"),VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env + env <- sideCondition (SCPatternMatch (TApp "natural-predecessor" [TVar "N"]) [VPMetaVar "N'"]) env rewriteTermTo (TApp "index" [TVar "N'",TVar "V*"]) env rewrite3 = do let env = emptyEnv - env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - rewriteTermTo (TName "none") env + env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)] env + rewriteTermTo (TSeq []) env rewrite4 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "P") (TName "pos-ints")] env - rewriteTermTo (TName "none") env + env <- vsMatch fargs [VPAnnotated VPWildCard (TName "positive-integers")] env + rewriteTermTo (TSeq []) env first_ fargs = FApp "first" (fargs) stepFirst fargs = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - rewriteTermTo (TVar "V1") env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)] env + rewriteTermTo (TVar "V") env second_ fargs = FApp "second" (fargs) stepSecond fargs = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "values"),VPAnnotated (VPMetaVar "V2") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - rewriteTermTo (TVar "V2") env + env <- vsMatch fargs [VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)] env + rewriteTermTo (TVar "V") env third_ fargs = FApp "third" (fargs) stepThird fargs = evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "values"),VPAnnotated (VPMetaVar "V2") (TName "values"),VPAnnotated (VPMetaVar "V3") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - rewriteTermTo (TVar "V3") env - -is_in_ fargs = FApp "is-in" (fargs) -stepIs_in fargs = - evalRules [rewrite1,rewrite2] [] - where rewrite1 = do - let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "V'") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - rewriteTermTo (TApp "or" [TApp "is-equal" [TVar "V",TVar "V'"],TApp "is-in" [TVar "V",TVar "V*"]]) env - rewrite2 = do - let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values")] env - rewriteTermTo (TName "false") env + env <- vsMatch fargs [VPAnnotated VPWildCard (TName "values"),VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)] env + rewriteTermTo (TVar "V") env first_n_ fargs = FApp "first-n" (fargs) stepFirst_n fargs = evalRules [rewrite1,rewrite2,rewrite3] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env + env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "values") StarOp)] env rewriteTermTo (TSeq []) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - env <- sideCondition (SCPatternMatch (TApp "nat-pred" [TVar "N"]) (VPMetaVar "N'")) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "positive-integers"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp),VPAnnotated VPWildCard (TName "values")] env + env <- sideCondition (SCPatternMatch (TApp "natural-predecessor" [TVar "N"]) [VPMetaVar "N'"]) env rewriteTermTo (TApp "first-n" [TVar "N'",TVar "V*"]) env rewrite3 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints")] env - rewriteTermTo (TName "none") env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "positive-integers")] env + rewriteTermTo (TSeq []) env drop_first_n_ fargs = FApp "drop-first-n" (fargs) stepDrop_first_n fargs = @@ -109,13 +109,13 @@ rewriteTermTo (TVar "V*") env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - env <- sideCondition (SCPatternMatch (TApp "nat-pred" [TVar "N"]) (VPMetaVar "N'")) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "positive-integers"),VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env + env <- sideCondition (SCPatternMatch (TApp "natural-predecessor" [TVar "N"]) [VPMetaVar "N'"]) env rewriteTermTo (TApp "drop-first-n" [TVar "N'",TVar "V*"]) env rewrite3 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints")] env - rewriteTermTo (TName "none") env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "positive-integers")] env + rewriteTermTo (TSeq []) env reverse_ fargs = FApp "reverse" (fargs) stepReverse fargs = @@ -134,12 +134,12 @@ evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPLit (Nat 0),VPMetaVar "V"] env + env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated VPWildCard (TName "values")] env rewriteTermTo (TSeq []) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints"),VPAnnotated (VPMetaVar "V") (TName "values")] env - env <- sideCondition (SCPatternMatch (TApp "nat-pred" [TVar "N"]) (VPMetaVar "N'")) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "positive-integers"),VPAnnotated (VPMetaVar "V") (TName "values")] env + env <- sideCondition (SCPatternMatch (TApp "natural-predecessor" [TVar "N"]) [VPMetaVar "N'"]) env rewriteTermTo (TSeq [TVar "V",TApp "n-of" [TVar "N'",TVar "V"]]) env intersperse_ fargs = FApp "intersperse" (fargs) @@ -147,29 +147,13 @@ evalRules [rewrite1,rewrite2,rewrite3] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V'") (TName "values")] env + env <- vsMatch fargs [VPAnnotated VPWildCard (TName "values")] env rewriteTermTo (TSeq []) env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V'") (TName "values"),VPMetaVar "V"] env + env <- vsMatch fargs [VPAnnotated VPWildCard (TName "values"),VPMetaVar "V"] env rewriteTermTo (TVar "V") env rewrite3 = do let env = emptyEnv env <- vsMatch fargs [VPAnnotated (VPMetaVar "V'") (TName "values"),VPAnnotated (VPMetaVar "V1") (TName "values"),VPAnnotated (VPMetaVar "V2") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env rewriteTermTo (TSeq [TVar "V1",TVar "V'",TApp "intersperse" [TVar "V'",TVar "V2",TVar "V*"]]) env - -filter_defined_ fargs = FApp "filter-defined" (fargs) -stepFilter_defined fargs = - evalRules [rewrite1,rewrite2,rewrite3] [] - where rewrite1 = do - let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "defined-values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - rewriteTermTo (TSeq [TVar "V",TApp "filter-defined" [TVar "V*"]]) env - rewrite2 = do - let env = emptyEnv - env <- vsMatch fargs [PADT "none" [],VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env - rewriteTermTo (TApp "filter-defined" [TVar "V*"]) env - rewrite3 = do - let env = emptyEnv - env <- vsMatch fargs [] env - rewriteTermTo (TSeq []) env diff --git a/cbs/Funcons/Core/Values/Composite/Strings/Strings.hs b/cbs/Funcons/Core/Values/Composite/Strings/Strings.hs --- a/cbs/Funcons/Core/Values/Composite/Strings/Strings.hs +++ b/cbs/Funcons/Core/Values/Composite/Strings/Strings.hs @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList diff --git a/cbs/Funcons/Core/Values/Composite/Trees/Trees.hs b/cbs/Funcons/Core/Values/Composite/Trees/Trees.hs new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Values/Composite/Trees/Trees.hs @@ -0,0 +1,96 @@ +-- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Trees/Trees.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Values.Composite.Trees.Trees where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) +entities = [] + +types = typeEnvFromList + [("trees",DataTypeMemberss "trees" [TPVar "T"] [DataTypeMemberConstructor "tree" [TVar "T",TSortSeq (TApp "trees" [TVar "T"]) StarOp] (Just [TPVar "T"])])] + +funcons = libFromList + [("tree",StrictFuncon stepTree),("tree-root-value",StrictFuncon stepTree_root_value),("tree-branch-sequence",StrictFuncon stepTree_branch_sequence),("single-branching-sequence",StrictFuncon stepSingle_branching_sequence),("forest-root-value-sequence",StrictFuncon stepForest_root_value_sequence),("forest-branch-sequence",StrictFuncon stepForest_branch_sequence),("forest-value-sequence",StrictFuncon stepForest_value_sequence),("trees",StrictFuncon stepTrees)] + +tree_ fargs = FApp "tree" (fargs) +stepTree 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 (Ascii 't'),FValue (Ascii 'r'),FValue (Ascii 'e'),FValue (Ascii 'e')])),TVar "_X1",TVar "_X2*"]) env + +tree_root_value_ fargs = FApp "tree-root-value" (fargs) +stepTree_root_value fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "tree" [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TApp "trees" [TName "values"]) StarOp)]] env + rewriteTermTo (TVar "V") env + +tree_branch_sequence_ fargs = FApp "tree-branch-sequence" (fargs) +stepTree_branch_sequence fargs = + evalRules [rewrite1] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "tree" [VPAnnotated VPWildCard (TName "values"),VPAnnotated (VPSeqVar "B*" StarOp) (TSortSeq (TApp "trees" [TName "values"]) StarOp)]] env + rewriteTermTo (TVar "B*") env + +single_branching_sequence_ fargs = FApp "single-branching-sequence" (fargs) +stepSingle_branching_sequence fargs = + evalRules [rewrite1,rewrite2,rewrite3] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "tree" [VPAnnotated (VPMetaVar "V") (TName "values")]] env + rewriteTermTo (TVar "V") env + rewrite2 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "tree" [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "B") (TApp "trees" [TName "values"])]] env + rewriteTermTo (TApp "left-to-right" [TVar "V",TApp "single-branching-sequence" [TVar "B"]]) env + rewrite3 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "tree" [VPAnnotated VPWildCard (TName "values"),VPAnnotated VPWildCard (TApp "trees" [TName "values"]),VPAnnotated (VPSeqVar "___" PlusOp) (TSortSeq (TApp "trees" [TName "values"]) PlusOp)]] env + rewriteTermTo (TName "fail") env + +forest_root_value_sequence_ fargs = FApp "forest-root-value-sequence" (fargs) +stepForest_root_value_sequence fargs = + evalRules [rewrite1,rewrite2] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "B") (TApp "trees" [TName "values"]),VPAnnotated (VPSeqVar "B*" StarOp) (TSortSeq (TApp "trees" [TName "values"]) StarOp)] env + rewriteTermTo (TSeq [TApp "tree-root-value" [TVar "B"],TApp "forest-root-value-sequence" [TVar "B*"]]) env + rewrite2 = do + let env = emptyEnv + env <- vsMatch fargs [] env + rewriteTermTo (TSeq []) env + +forest_branch_sequence_ fargs = FApp "forest-branch-sequence" (fargs) +stepForest_branch_sequence fargs = + evalRules [rewrite1,rewrite2] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [VPAnnotated (VPMetaVar "B") (TApp "trees" [TName "values"]),VPAnnotated (VPSeqVar "B*" StarOp) (TSortSeq (TApp "trees" [TName "values"]) StarOp)] env + rewriteTermTo (TSeq [TApp "tree-branch-sequence" [TVar "B"],TApp "forest-branch-sequence" [TVar "B*"]]) env + rewrite2 = do + let env = emptyEnv + env <- vsMatch fargs [] env + rewriteTermTo (TSeq []) env + +forest_value_sequence_ fargs = FApp "forest-value-sequence" (fargs) +stepForest_value_sequence fargs = + evalRules [rewrite1,rewrite2] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "tree" [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "B1*" StarOp) (TSortSeq (TApp "trees" [TName "values"]) StarOp)],VPAnnotated (VPSeqVar "B2*" StarOp) (TSortSeq (TApp "trees" [TName "values"]) StarOp)] env + rewriteTermTo (TSeq [TVar "V",TApp "forest-value-sequence" [TVar "B1*"],TApp "forest-value-sequence" [TVar "B2*"]]) env + rewrite2 = do + let env = emptyEnv + env <- vsMatch fargs [] env + rewriteTermTo (TSeq []) env + +trees_ = FApp "trees" +stepTrees ts = rewriteType "trees" ts 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 @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -20,7 +20,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPSeqVar "_X1*" StarOp] env - env <- sideCondition (SCIsInSort (TVar "_X1*") (TSortSeq (TName "values") 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 tuple_elements_ fargs = FApp "tuple-elements" (fargs) @@ -45,11 +45,11 @@ rewrite3 = do let env = emptyEnv env <- vsMatch fargs [PADT "tuple" [VPAnnotated (VPSeqVar "V1+" PlusOp) (TSortSeq (TName "values") PlusOp)],PADT "tuple" []] env - rewriteTermTo (TName "none") env + rewriteTermTo (TSeq []) env rewrite4 = do let env = emptyEnv env <- vsMatch fargs [PADT "tuple" [],PADT "tuple" [VPAnnotated (VPSeqVar "V2+" PlusOp) (TSortSeq (TName "values") PlusOp)]] env - rewriteTermTo (TName "none") env + rewriteTermTo (TSeq []) env tuples_ = FApp "tuples" stepTuples ts = rewriteType "tuples" ts 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 @@ -5,11 +5,11 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList - [("variants",DataTypeMemberss "variants" [TPVar "MIT"] [DataTypeMemberConstructor "variant" [TName "ids",TName "defined-values"] (Just [TPVar "MIT"])])] + [("variants",DataTypeMemberss "variants" [TPVar "T"] [DataTypeMemberConstructor "variant" [TName "identifiers",TVar "T"] (Just [TPVar "T"])])] funcons = libFromList [("variant",StrictFuncon stepVariant),("variant-id",StrictFuncon stepVariant_id),("variant-value",StrictFuncon stepVariant_value),("variants",StrictFuncon stepVariants)] @@ -20,8 +20,8 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPMetaVar "_X1",VPMetaVar "_X2"] env - env <- sideCondition (SCIsInSort (TVar "_X1") (TName "values")) env - env <- sideCondition (SCIsInSort (TVar "_X2") (TName "values")) 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 variant_id_ fargs = FApp "variant-id" (fargs) @@ -29,7 +29,7 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "variant" [VPAnnotated (VPMetaVar "I") (TName "ids"),VPAnnotated (VPMetaVar "DV") (TName "defined-values")]] env + env <- vsMatch fargs [PADT "variant" [VPAnnotated (VPMetaVar "I") (TName "identifiers"),VPAnnotated VPWildCard (TName "values")]] env rewriteTermTo (TVar "I") env variant_value_ fargs = FApp "variant-value" (fargs) @@ -37,8 +37,8 @@ evalRules [rewrite1] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [PADT "variant" [VPAnnotated (VPMetaVar "I") (TName "ids"),VPAnnotated (VPMetaVar "DV") (TName "defined-values")]] env - rewriteTermTo (TVar "DV") env + env <- vsMatch fargs [PADT "variant" [VPAnnotated VPWildCard (TName "identifiers"),VPAnnotated (VPMetaVar "V") (TName "values")]] env + rewriteTermTo (TVar "V") env variants_ = FApp "variants" stepVariants ts = rewriteType "variants" ts 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 @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -20,7 +20,7 @@ where rewrite1 = do let env = emptyEnv env <- vsMatch fargs [VPSeqVar "_X1*" StarOp] env - env <- sideCondition (SCIsInSort (TVar "_X1*") (TSortSeq (TName "values") 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 vector_elements_ fargs = FApp "vector-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 @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -67,7 +67,7 @@ rewriteTermTo (TName "true") env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "false" [],VPAnnotated (VPSeqVar "B*" StarOp) (TSortSeq (TName "booleans") StarOp)] env + env <- vsMatch fargs [PADT "false" [],VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "booleans") StarOp)] env rewriteTermTo (TName "false") env rewrite3 = do let env = emptyEnv @@ -83,7 +83,7 @@ rewriteTermTo (TName "false") env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "true" [],VPAnnotated (VPSeqVar "B*" StarOp) (TSortSeq (TName "booleans") StarOp)] env + env <- vsMatch fargs [PADT "true" [],VPAnnotated (VPSeqVar "___" StarOp) (TSortSeq (TName "booleans") StarOp)] env rewriteTermTo (TName "true") env rewrite3 = do let env = emptyEnv 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 @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList @@ -46,12 +46,12 @@ let env = emptyEnv env <- vsMatch fargs [PADT "datatype-value" [VPLit (ADTVal "list" [FValue (Ascii 'l'),FValue (Ascii 'i'),FValue (Ascii 's'),FValue (Ascii 't')]),VPAnnotated (VPMetaVar "C") (TName "characters")]] env env <- sideCondition (SCIsInSort (TVar "C") (TSortComplement (TName "ascii-characters"))) env - rewriteTermTo (TName "none") env + 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 <- sideCondition (SCInequality (TApp "length" [TVar "C*"]) (TFuncon (FValue (Nat 1)))) env - rewriteTermTo (TName "none") env + rewriteTermTo (TSeq []) env backspace_ = FName "backspace" stepBackspace = evalRules [rewrite1] [] 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 @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList diff --git a/cbs/Funcons/Core/Values/Primitive/Integers/Integers.hs b/cbs/Funcons/Core/Values/Primitive/Integers/Integers.hs --- a/cbs/Funcons/Core/Values/Primitive/Integers/Integers.hs +++ b/cbs/Funcons/Core/Values/Primitive/Integers/Integers.hs @@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList diff --git a/cbs/Funcons/Core/Values/Primitive/Null/Null.hs b/cbs/Funcons/Core/Values/Primitive/Null/Null.hs new file mode 100644 --- /dev/null +++ b/cbs/Funcons/Core/Values/Primitive/Null/Null.hs @@ -0,0 +1,25 @@ +-- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Primitive/Null/Null.cbs +{-# LANGUAGE OverloadedStrings #-} + +module Funcons.Core.Values.Primitive.Null.Null where + +import Funcons.EDSL + +import Funcons.Operations hiding (Values,libFromList) +entities = [] + +types = typeEnvFromList + [("null-type",DataTypeMemberss "null-type" [] [DataTypeMemberConstructor "null-value" [] (Just [])])] + +funcons = libFromList + [("null-value",NullaryFuncon stepNull_value),("null",NullaryFuncon stepNull_value),("null-type",NullaryFuncon stepNull_type)] + +null_value_ = FName "null-value" +null_ = FName "null-value" +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 + +null_type_ = FName "null-type" +stepNull_type = rewriteType "null-type" [] diff --git a/cbs/Funcons/Core/Values/Primitive/Unit/Unit.hs b/cbs/Funcons/Core/Values/Primitive/Unit/Unit.hs deleted file mode 100644 --- a/cbs/Funcons/Core/Values/Primitive/Unit/Unit.hs +++ /dev/null @@ -1,25 +0,0 @@ --- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Primitive/Unit/Unit.cbs -{-# LANGUAGE OverloadedStrings #-} - -module Funcons.Core.Values.Primitive.Unit.Unit where - -import Funcons.EDSL - -import Funcons.Operations hiding (Values) -entities = [] - -types = typeEnvFromList - [("unit-type",DataTypeMemberss "unit-type" [] [DataTypeMemberConstructor "null-value" [] (Just [])])] - -funcons = libFromList - [("null-value",NullaryFuncon stepNull_value),("null",NullaryFuncon stepNull_value),("unit-type",NullaryFuncon stepUnit_type)] - -null_value_ = FName "null-value" -null_ = FName "null-value" -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 - -unit_type_ = FName "unit-type" -stepUnit_type = rewriteType "unit-type" [] diff --git a/cbs/Funcons/Core/Values/ValueTypes/ValueTypes.hs b/cbs/Funcons/Core/Values/ValueTypes/ValueTypes.hs --- a/cbs/Funcons/Core/Values/ValueTypes/ValueTypes.hs +++ b/cbs/Funcons/Core/Values/ValueTypes/ValueTypes.hs @@ -5,14 +5,14 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList [] funcons = libFromList - [("is-in-type",StrictFuncon stepIs_in_type),("is",StrictFuncon stepIs_in_type),("cast-to-type",StrictFuncon stepCast_to_type),("cast",StrictFuncon stepCast_to_type),("is-defined",StrictFuncon stepIs_defined),("is-def",StrictFuncon stepIs_defined),("is-equal",StrictFuncon stepIs_equal),("is-eq",StrictFuncon stepIs_equal)] + [("is-in-type",StrictFuncon stepIs_in_type),("is",StrictFuncon stepIs_in_type),("is-value",StrictFuncon stepIs_value),("is-val",StrictFuncon stepIs_value),("when-true",StrictFuncon stepWhen_true),("when",StrictFuncon stepWhen_true),("cast-to-type",StrictFuncon stepCast_to_type),("cast",StrictFuncon stepCast_to_type),("is-equal",StrictFuncon stepIs_equal),("is-eq",StrictFuncon stepIs_equal)] is_in_type_ fargs = FApp "is-in-type" (fargs) is_ fargs = FApp "is-in-type" (fargs) @@ -20,42 +20,55 @@ evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "T'") (TName "types")] env - env <- sideCondition (SCIsInSort (TVar "V") (TVar "T'")) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "T") (TName "types")] env + env <- sideCondition (SCIsInSort (TVar "V") (TVar "T")) env rewriteTermTo (TName "true") env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "T'") (TName "types")] env - env <- sideCondition (SCIsInSort (TVar "V") (TSortComplement (TVar "T'"))) env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "T") (TName "types")] env + env <- sideCondition (SCIsInSort (TVar "V") (TSortComplement (TVar "T"))) env rewriteTermTo (TName "false") env -cast_to_type_ fargs = FApp "cast-to-type" (fargs) -cast_ fargs = FApp "cast-to-type" (fargs) -stepCast_to_type fargs = +is_value_ fargs = FApp "is-value" (fargs) +is_val_ fargs = FApp "is-value" (fargs) +stepIs_value fargs = evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "T'") (TName "types")] env - env <- sideCondition (SCIsInSort (TVar "V") (TVar "T'")) env + env <- vsMatch fargs [VPAnnotated VPWildCard (TName "values")] env + rewriteTermTo (TName "true") env + rewrite2 = do + let env = emptyEnv + env <- vsMatch fargs [] env + rewriteTermTo (TName "false") env + +when_true_ fargs = FApp "when-true" (fargs) +when_ fargs = FApp "when-true" (fargs) +stepWhen_true fargs = + evalRules [rewrite1,rewrite2] [] + where rewrite1 = do + let env = emptyEnv + env <- vsMatch fargs [PADT "true" [],VPAnnotated (VPMetaVar "V") (TName "values")] env rewriteTermTo (TVar "V") env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "T'") (TName "types")] env - env <- sideCondition (SCIsInSort (TVar "V") (TSortComplement (TVar "T'"))) env - rewriteTermTo (TName "none") env + env <- vsMatch fargs [PADT "false" [],VPAnnotated (VPMetaVar "V") (TName "values")] env + rewriteTermTo (TSeq []) env -is_defined_ fargs = FApp "is-defined" (fargs) -is_def_ fargs = FApp "is-defined" (fargs) -stepIs_defined fargs = +cast_to_type_ fargs = FApp "cast-to-type" (fargs) +cast_ fargs = FApp "cast-to-type" (fargs) +stepCast_to_type fargs = evalRules [rewrite1,rewrite2] [] where rewrite1 = do let env = emptyEnv - env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "defined-values")] env - rewriteTermTo (TName "true") env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "T") (TName "types")] env + env <- sideCondition (SCIsInSort (TVar "V") (TVar "T")) env + rewriteTermTo (TVar "V") env rewrite2 = do let env = emptyEnv - env <- vsMatch fargs [PADT "none" []] env - rewriteTermTo (TName "false") env + env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "T") (TName "types")] env + env <- sideCondition (SCIsInSort (TVar "V") (TSortComplement (TVar "T"))) env + rewriteTermTo (TSeq []) env is_equal_ fargs = FApp "is-equal" (fargs) is_eq_ fargs = FApp "is-equal" (fargs) diff --git a/funcons-tools.cabal b/funcons-tools.cabal --- a/funcons-tools.cabal +++ b/funcons-tools.cabal @@ -2,29 +2,24 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: funcons-tools -version: 0.2.0.1 +version: 0.2.0.3 synopsis: A modular interpreter for executing funcons description: - The PLanCompS project has developed a component-based approach to formal semantics. + The PLanCompS project () has developed a component-based approach to formal semantics. The semantics of a language is defined by translating its constructs to combinations of `fundamental constructs' called /funcons/. . - Read more about the project here: . - Read more about funcons and their specification in CBS here: . - . This package provides a collection of highly reusable funcons in "Funcons.Core", an interpreter for these funcons and means for defining new funcons. . The executable provided by this package is an interpreter for running terms constructed from the collection of funcons provided by "Funcons.Core". - How this executable is used is explained in "Funcons.Tools". + How this executable is used is explained in "Funcons.Tools". . - Additional funcons can be defined with the helper functions provided by - "Funcons.EDSL". The module "Funcons.Tools" provides functions for creating + Additional funcons can be defined with the helper functions provided by + "Funcons.EDSL". The module "Funcons.Tools" provides functions for creating executables by extending the main interpreter with additional funcons. . - Please contact any of the maintainers when unexpected behaviour is encountered - or exports appear to be missing. homepage: http://plancomps.org license: MIT @@ -34,17 +29,18 @@ copyright: Copyright (C) 2015 L. Thomas van Binsbergen and Neil Sculthorpe category: Compilers/Interpreters build-type: Simple -stability: unstable +stability: unstable -- extra-source-files: cabal-version: >=1.10 library exposed-modules: Funcons.EDSL , Funcons.Tools - Funcons.Core + , Funcons.Core , Funcons.ValueOperations , Funcons.Core.Manual - , Funcons.MetaProgramming + , Funcons.MetaProgramming + , Funcons.Parser , Funcons.GLLParser , Funcons.RunOptions build-depends: base >=4.3 && <= 5 @@ -60,21 +56,20 @@ ,TypeCompose>=0.9.10 ,regex-applicative ,random-strings - ,funcons-values + ,funcons-values >= 0.1.0.3 hs-source-dirs: src, cbs, manual default-language: Haskell2010 other-extensions: OverloadedStrings ghc-options: -fwarn-incomplete-patterns -fwarn-monomorphism-restriction -fwarn-unused-imports - other-modules: - Funcons.MSOS, + other-modules: + Funcons.MSOS, Funcons.TypeSubstitution, - Funcons.Substitution, - Funcons.Parser, - Funcons.Patterns, - Funcons.Entities, - Funcons.Simulation, - Funcons.Exceptions, - Funcons.Types, + Funcons.Substitution, + Funcons.Patterns, + Funcons.Entities, + Funcons.Simulation, + Funcons.Exceptions, + Funcons.Types, Funcons.Printer -- generated Funcons.Core.Library, @@ -96,6 +91,9 @@ Funcons.Core.Values.ValueTypes.ValueTypes, -- Funcons.Core.Values.Composite.Sets, Funcons.Core.Values.Composite.Bits.Bits, + Funcons.Core.Values.Composite.Classes.Classes, + Funcons.Core.Values.Composite.Objects.Objects, + Funcons.Core.Values.Composite.Trees.Trees, Funcons.Core.Values.Composite.Strings.Strings, Funcons.Core.Values.Composite.Datatypes.Datatypes, Funcons.Core.Values.Composite.Lists.Lists, @@ -103,16 +101,16 @@ Funcons.Core.Values.Composite.Sequences.Sequences, Funcons.Core.Values.Composite.Variants.Variants, Funcons.Core.Values.Composite.Records.Records, --- Funcons.Core.Values.Composite.Maps, + Funcons.Core.Values.Composite.Maps.Maps, Funcons.Core.Values.Composite.Vectors.Vectors, Funcons.Core.Values.Composite.Tuples.Tuples, Funcons.Core.Values.Composite.References.References, Funcons.Core.Values.Composite.Graphs.Graphs, Funcons.Core.Values.Primitive.Floats.Floats, Funcons.Core.Values.Primitive.Integers.Integers, - Funcons.Core.Values.Primitive.Unit.Unit, Funcons.Core.Values.Primitive.Booleans.Booleans, Funcons.Core.Values.Primitive.Characters.Characters, + Funcons.Core.Values.Primitive.Null.Null, Funcons.Core.Values.Abstraction.Functions.Functions, Funcons.Core.Values.Abstraction.Patterns.Patterns, Funcons.Core.Values.Abstraction.Generic.Generic, @@ -141,15 +139,15 @@ other-extensions: OverloadedStrings build-depends: base >=4.3 && <= 5 ,text - ,containers + ,containers ,vector ,bv >= 0.5 ,funcons-tools ,multiset ,split - ,directory + ,directory ,mtl >= 2.0 - ,gll >= 0.3.0.9 + ,gll >= 0.4.0.2 ,TypeCompose>=0.9.10 ,regex-applicative ,random-strings diff --git a/manual/Funcons/Core/Computations/Normal/GeneratingBuiltin.hs b/manual/Funcons/Core/Computations/Normal/GeneratingBuiltin.hs --- a/manual/Funcons/Core/Computations/Normal/GeneratingBuiltin.hs +++ b/manual/Funcons/Core/Computations/Normal/GeneratingBuiltin.hs @@ -3,7 +3,7 @@ module Funcons.Core.Computations.Normal.GeneratingBuiltin where import Funcons.EDSL -import Funcons.Operations hiding (Values,tobool) +import Funcons.Operations hiding (Values,tobool,libFromList) import Data.Set (fromList) diff --git a/manual/Funcons/Core/Values/Composite/MapsBuiltin.hs b/manual/Funcons/Core/Values/Composite/MapsBuiltin.hs --- a/manual/Funcons/Core/Values/Composite/MapsBuiltin.hs +++ b/manual/Funcons/Core/Values/Composite/MapsBuiltin.hs @@ -20,8 +20,8 @@ ("map-empty", fromNullaryValOp map_empty_ VAL.map_empty_) , ("is-map-empty", fromValOp is_map_empty_ VAL.is_map_empty_) , ("map-insert", fromValOp map_insert_ VAL.map_insert_) - , ("map-lookup", fromValOp map_lookup_ VAL.map_lookup_) - , ("lookup", fromValOp map_lookup_ VAL.map_lookup_) + , ("map-lookup", fromSeqValOp map_lookup_ VAL.map_lookup_) + , ("lookup", fromSeqValOp map_lookup_ VAL.map_lookup_) , ("map-domain", fromValOp map_domain_ VAL.domain_) , ("domain", fromValOp map_domain_ VAL.domain_) , ("dom", fromValOp map_domain_ VAL.domain_) @@ -32,7 +32,6 @@ , ("maps", fromValOp maps_ VAL.maps_) , ("map", fromValOp map_ VAL.map_) , ("map-elements", fromSeqValOp map_elements_ VAL.map_elements_) - , ("map-points", fromSeqValOp map_points_ VAL.map_points_) ] map_ = applyFuncon "map" @@ -53,4 +52,3 @@ dom_ = applyFuncon "domain" map_domain_ = applyFuncon "domain" map_elements_ = applyFuncon "map-elements" -map_points_ = applyFuncon "map-points" diff --git a/manual/Funcons/Core/Values/Composite/MultisetsBuiltin.hs b/manual/Funcons/Core/Values/Composite/MultisetsBuiltin.hs --- a/manual/Funcons/Core/Values/Composite/MultisetsBuiltin.hs +++ b/manual/Funcons/Core/Values/Composite/MultisetsBuiltin.hs @@ -3,7 +3,7 @@ module Funcons.Core.Values.Composite.MultisetsBuiltin where import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values,libFromList) import Funcons.Core.Values.Primitive.BoolBuiltin import qualified Data.MultiSet as MS diff --git a/manual/Funcons/Core/Values/Primitive/BoolBuiltin.hs b/manual/Funcons/Core/Values/Primitive/BoolBuiltin.hs --- a/manual/Funcons/Core/Values/Primitive/BoolBuiltin.hs +++ b/manual/Funcons/Core/Values/Primitive/BoolBuiltin.hs @@ -3,7 +3,7 @@ module Funcons.Core.Values.Primitive.BoolBuiltin where import Funcons.EDSL -import Funcons.Operations hiding (Values) +import Funcons.Operations hiding (Values, libFromList) library = libFromList [] diff --git a/manual/Funcons/Core/Values/Primitive/CharactersBuiltin.hs b/manual/Funcons/Core/Values/Primitive/CharactersBuiltin.hs --- a/manual/Funcons/Core/Values/Primitive/CharactersBuiltin.hs +++ b/manual/Funcons/Core/Values/Primitive/CharactersBuiltin.hs @@ -6,8 +6,8 @@ import qualified Funcons.Operations as VAL library = libFromList [ - ("ascii-characters", fromValOp ascii_characters_ VAL.ascii_characters_) - , ("ascii-characters", fromValOp ascii_character_ VAL.ascii_character_) + ("ascii-characters", fromNullaryValOp ascii_characters_ VAL.ascii_characters_) +-- , ("ascii-character", fromValOp ascii_character_ VAL.ascii_character_) , ("unicode", fromValOp unicode_ VAL.unicode_) , ("unicode-character-code", fromValOp unicode_character_code_ VAL.unicode_character_code_) , ("characters", fromNullaryValOp characters_ VAL.characters_) diff --git a/manual/Funcons/Core/Values/TypesBuiltin.hs b/manual/Funcons/Core/Values/TypesBuiltin.hs --- a/manual/Funcons/Core/Values/TypesBuiltin.hs +++ b/manual/Funcons/Core/Values/TypesBuiltin.hs @@ -9,17 +9,15 @@ ("datatype-values", fromNullaryValOp datatype_values_ VAL.datatype_values_) , ("ground-values", fromNullaryValOp ground_values_ VAL.ground_values_) , ("ground-vals", fromNullaryValOp ground_values_ VAL.ground_values_) - , ("none", fromNullaryValOp none_ VAL.none_) - , ("defined-values", fromNullaryValOp defined_values_ VAL.defined_values_) - , ("nothing", fromNullaryValOp nothing_ VAL.nothing_) +-- , ("null", fromNullaryValOp null_ VAL.null_) +-- , ("null-type", fromNullaryValOp nulltype_ VAL.nulltype_) , ("types", fromNullaryValOp types_ VAL.types_) , ("value-types", fromNullaryValOp value_types_ VAL.value_types_) ] types_ = applyFuncon "types" value_types_ = applyFuncon "value-types" -defined_values_ = applyFuncon "defined-values" -nothing_ = applyFuncon "nothing" +nulltype_ = applyFuncon "null-type" datatype_values_ = applyFuncon "datatype-values" -none_ = applyFuncon "none" +null_ = applyFuncon "null" ground_values_ = applyFuncon "ground-values" diff --git a/manual/Funcons/MetaProgramming.hs b/manual/Funcons/MetaProgramming.hs --- a/manual/Funcons/MetaProgramming.hs +++ b/manual/Funcons/MetaProgramming.hs @@ -14,6 +14,7 @@ import Data.Text (pack, unpack) import qualified Data.Map as M +import qualified Data.Set as S -- | This function implements the ==CT=> relation. -- Compiling programs to executable funcons terms, @@ -25,11 +26,11 @@ FApp "meta-down" [m] -> staticEval m FApp "meta-let" [FValue nm,m,n] | isString_ nm -> do v <- evalRel =<< ctRel m - menv <- getInh "env" + [menv] <- getInh env_entity let env' = case menv of - Map env -> Map (M.insert nm v env) - _ -> Map (M.singleton nm v) - withInh "env" env' (ctRel n) + Map env -> Map (M.insert nm [v] env) + _ -> Map (M.singleton nm [v]) + withInh env_entity [env'] (ctRel n) FApp nm arg -> FApp nm <$> mapM ctRel arg -- FList fs -> FList <$> mapM ctRel fs FSet fs -> FSet <$> mapM ctRel fs @@ -82,9 +83,13 @@ ((Right f, _, _), _) -> f where process = do env <- evalRel fenv - putMut "atom-gen" (Atom "0") - putMut "store" (Map M.empty) - withInh "env" env (ctRel f) + putMut atom_gen_entity (Set S.empty) + putMut store_entity (Map M.empty) + withInh env_entity [env] (ctRel f) + +env_entity = "environment" +store_entity = "store" +atom_gen_entity = "used-atom-set" translationStep :: ([Funcons] -> Funcons) -> StrictFuncon translationStep f vs = compstep $ do fs <- liftRewrite (mapM dlRel vs) 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 hiding (entities, funcons, types) -import Funcons.Core.Manual hiding (entities, funcons, types, unicode_, ascii_character_) +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 @@ -11,7 +11,7 @@ -- ** Smart construction of funcon terms app0_, app1_, app2_, app3_, -- *** Funcon terms - tuple_, list_, set_, map_, vec_, env_fromlist_, none__, + tuple_, list_, set_, map_, vec_, env_fromlist_, null__, -- *** Values int_, nat_, float_, ieee_float_32_, ieee_float_64_, string_, string__, atom_, -- *** Types @@ -160,7 +160,7 @@ mkBinary :: (Types -> Types -> Types) -> EvalFunction mkBinary cons = StrictFuncon sfuncon where sfuncon [ComputationType (Type x), ComputationType (Type y)] = - rewritten $ typeVal $ Maps x y + rewritten $ typeVal $ maps (injectT x) (injectT y) sfuncon _ = rewritten $ typeVal $ cons VAL.Values VAL.Values app0_ :: ([Funcons] -> Funcons) -> Funcons diff --git a/src/Funcons/Entities.hs b/src/Funcons/Entities.hs --- a/src/Funcons/Entities.hs +++ b/src/Funcons/Entities.hs @@ -52,8 +52,7 @@ _ -> liftRewrite $ exception f "default value requires steps to evaluate" setEntityDefaults ((DefInherited nm f):rest) msos = liftRewrite (rewriteFuncons f) >>= \case - ValTerm [v] -> withInh nm v (setEntityDefaults rest msos) - ValTerm vs -> liftRewrite $ exception f "default value evaluates to a sequence" + ValTerm vs -> withInh nm vs (setEntityDefaults rest msos) _ -> liftRewrite $ exception f "default value requires steps to evaluate" setEntityDefaults ((DefControl nm):rest) msos = withControl nm Nothing (setEntityDefaults rest msos) @@ -74,7 +73,7 @@ getMut :: Name -> MSOS Values getMut key = do rw <- giveMUT case M.lookup key rw of - Nothing -> return none__ + Nothing -> return null__ Just v -> return v -- | Variant of 'getMut' that performs pattern-matching. @@ -86,7 +85,7 @@ modifyMUT :: Name -> (Values -> Values) -> MSOS () modifyMUT key f = do rw <- giveMUT newMUT (M.alter up key rw) - where up Nothing = Just (f none__) + where up Nothing = Just (f null__) up (Just x) = Just (f x) -- | Set the value of some mutable entity. @@ -230,21 +229,21 @@ -- inherited -- | Get the value of an inherited entity. -getInh :: Name -> MSOS Values +getInh :: Name -> MSOS [Values] getInh key = do ro <- giveINH case M.lookup key ro of - Nothing -> return none__ - Just v -> return v + Nothing -> return [null__] + Just vs -> return vs -- | Version of 'getInh' that applies pattern-matching. -getInhPatt :: Name -> VPattern -> Env -> MSOS Env -getInhPatt nm pat env = do - val <- getInh nm - liftRewrite (vMatch val pat env) +getInhPatt :: Name -> [VPattern] -> Env -> MSOS Env +getInhPatt nm pats env = do + vals <- getInh nm + liftRewrite (vsMatch vals pats env) -- | Set the value of an inherited entity. -- The new value is /only/ set for 'MSOS' computation given as a third argument. -withInh :: Name -> Values -> MSOS a -> MSOS a +withInh :: Name -> [Values] -> MSOS a -> MSOS a withInh key v (MSOS f) = MSOS (\ctxt mut -> let ctxt' = ctxt { inh_entities = M.insert key v (inh_entities ctxt) } in f ctxt' mut) @@ -252,7 +251,7 @@ -- | Variant of 'withInh' that performs substitution. withInhTerm :: Name -> FTerm -> Env -> MSOS a -> MSOS a withInhTerm nm term env msos = do - v <- liftRewrite $ (subsAndRewritesToValue term env) + v <- liftRewrite $ (subsAndRewritesToValues term env) withInh nm v msos -- output diff --git a/src/Funcons/Exceptions.hs b/src/Funcons/Exceptions.hs --- a/src/Funcons/Exceptions.hs +++ b/src/Funcons/Exceptions.hs @@ -4,7 +4,8 @@ import Funcons.Types import Funcons.Printer -import Data.Text +import Data.List (intercalate) +import Data.Text (unpack) -- handling exception from the interpreter type IException = (Funcons, Funcons, IE) --global, local, exception @@ -12,8 +13,8 @@ | Err String --TODO when used? | PartialOp String | Internal String - | NoRule - | NoMoreBranches + | NoRule [IException] + | NoMoreBranches [IException] | SideCondFail String | InsufficientInput Name | InsufficientInputConsumed Name @@ -21,11 +22,15 @@ | StepOnValue [Values] showIException :: IException -> String -showIException (f0,f,ie) = "Internal Exception: " ++ show ie ++ " on \n" ++ showFuncons f0 +showIException (f0,f,ie@(NoRule _)) = show ie +showIException (f0,f,ie@(NoMoreBranches _)) = show ie +showIException (f0,f,ie) = "Internal Exception: " ++ show ie ++ " on \n" ++ showFuncons f instance Show IE where show (SortErr err) = "dynamic sort check (" ++ err ++ ")" - show NoRule = "no rule to execute" + show (NoRule []) = "no more rules to try" + show (NoRule errs) = mkRulesErr (zipWith mkRuleErr [1..] errs) f + where (_,f,_) = head errs show (Err err) = "exception (" ++ err ++ ")" show (Internal err) = "exception (" ++ err ++ ")" show (SideCondFail str) = str @@ -33,9 +38,14 @@ show (InsufficientInput nm) = "insufficient supply for " ++ unpack nm show (InsufficientInputConsumed nm) = "insufficient input consumed for entity " ++ unpack nm show (PartialOp str) = "partial operation" - show (NoMoreBranches) = "no more branches to try" + show (NoMoreBranches []) = "no more branches to try" + show (NoMoreBranches errs) = mkRulesErr (zipWith mkRuleErr [1..] errs) f + where (_,f,_) = head errs show (StepOnValue v) = "attempting to step a value: " ++ showValuesSeq v +mkRuleErr i (_,_,ie) = show ie +mkRulesErr strs f = " " ++ showFuncons f ++ ":\n" ++ intercalate "\n" (map (" " ++) strs) + -- which exceptions stop a rule from executing so that the next one can be attempted? failsRule :: IException -> Bool failsRule (_,_,SideCondFail _) = True @@ -43,8 +53,8 @@ failsRule (_,_,SortErr _) = True failsRule (_,_,PartialOp _) = True failsRule (_,_,StepOnValue _) = True -failsRule (_,_,NoMoreBranches) = True -failsRule (_,_,NoRule) = True +failsRule (_,_,NoMoreBranches _) = True +failsRule (_,_,NoRule _) = True failsRule _ = False diff --git a/src/Funcons/GLLParser.hs b/src/Funcons/GLLParser.hs --- a/src/Funcons/GLLParser.hs +++ b/src/Funcons/GLLParser.hs @@ -60,7 +60,7 @@ <:= FSet <$$> braces (multipleSepBy pFuncons (keychar ',')) -- <||> FTuple <$$> parens (multipleSepBy pFuncons (keychar ',')) <||> FApp "list" <$$> brackets (multipleSepBy pFuncons (keychar ',')) - <||> FMap . concat <$$> braces (multipleSepBy1 pKeyPair (keychar ',')) + <||> FMap <$$> braces (multipleSepBy1 pKeyPair (keychar ',')) <||> FSortComputes <$$ keyword "=>" <**> pFuncons <||> FSortComplement <$$ keychar '~' <**> pFuncons <||> suffix_select <$$> pFuncons <**> pFSuffix @@ -99,9 +99,10 @@ pFunconsSeq = "FUNCONS-SEQ" <:=> either (:[]) id <$$> pFunconss -pKeyPair :: Parser [Funcons] +pKeyPair :: Parser Funcons pKeyPair = "KEYPAIR" <:=> - (\x y -> [x,y]) <$$> pFuncons <** keyword "|->" <**> pFuncons + fBinding <$$> pFuncons <** keyword "|->" <**> pFunconss + where fBinding k ev = FBinding k (either (:[]) id ev) pOp :: Parser SeqSortOp pOp = "OP" <:=> diff --git a/src/Funcons/MSOS.hs b/src/Funcons/MSOS.hs --- a/src/Funcons/MSOS.hs +++ b/src/Funcons/MSOS.hs @@ -24,14 +24,14 @@ rewriteRules, stepRules, evalRules, MSOSState(..), emptyMSOSState, emptyRewriteState, MSOSReader(..),RewriteReader(..),showIException, MSOSWriter(..), RewriteWriterr(..), -- * Evaluation funcons TODO internal usage only (by Funcons.Tools) Rewritten(..), rewriteFuncons, rewriteFunconsWcount, evalFuncons - , stepTrans, rewritesToValue, rewritesToValues + , stepTrans, rewritesToValue, rewritesToValues, rewritesToType , emptyDCTRL, emptyINH, Interactive(..), SimIO(..) , rewriteToValErr, count_delegation, optRefocus , evalStrictSequence, rewriteStrictSequence, evalSequence, -- * Values showTypes, showSorts, showValues, showValuesSeq, showFuncons, showFunconsSeq,traceLib, -- * Funcon libraries - FunconLibrary, libUnions, libOverrides, libEmpty, libUnion, libOverride, libFromList, + FunconLibrary, libUnions, libOverrides, libEmpty, libUnion, libOverride, Funcons.MSOS.libFromList, evalctxt2exception, ctxt2exception, fromSeqValOp, fromNullaryValOp, fromValOp, -- * Counters displayCounters, counterKeys, ppCounters, @@ -78,11 +78,13 @@ report f seqRes res = case res of Error _ (VAL.SortErr str) -> sortErr f str - Error _ (DomErr str) -> rewritten none__ + Error _ (DomErr str) -> rewrittens [] Error _ (ArityErr str) -> sortErr f str 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, @@ -243,17 +245,17 @@ ctxt2exception ie ctxt = (global_fct (ereader ctxt), local_fct (ereader ctxt), ie) - -rewriteRules :: [Rewrite Rewritten] -> Rewrite Rewritten -rewriteRules [] = rewrite_throw NoMoreBranches -rewriteRules (t1:ts) = Rewrite $ \ctxt st -> +rewriteRules = rewriteRules' [] +rewriteRules' :: [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten +rewriteRules' errs [] = rewrite_throw (NoMoreBranches errs) +rewriteRules' errs (t1:ts) = Rewrite $ \ctxt st -> let (rw_res, st', rw_cs) = runRewrite t1 ctxt st in case rw_res of Left ie| failsRule ie -> -- resets state trace (showIException ie) $ runRewrite (do count_backtrack_in addToRCounter (counters rw_cs) - rewriteRules ts) ctxt st + rewriteRules' (ie:errs) ts) ctxt st _ -> (rw_res, st', rw_cs) --------------------------------------------------------------------------- @@ -324,16 +326,16 @@ stepRules = stepARules NoMoreBranches count_backtrack_in -stepARules :: IE -> Rewrite () -> [MSOS StepRes] -> MSOS StepRes -stepARules exc _ [] = msos_throw exc -stepARules exc counter (t1:ts) = MSOS $ \ctxt mut -> do +stepARules :: ([IException] -> IE) -> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes +stepARules fexc _ errs [] = msos_throw (fexc errs) +stepARules fexc counter errs (t1:ts) = MSOS $ \ctxt mut -> do (e_ie_a, mut', wr) <- runMSOS t1 ctxt mut case e_ie_a of Left ie | failsRule ie -> -- resets input & read/write entities trace (showIException ie) $ runMSOS (do liftRewrite counter addToCounter (counters (ewriter wr)) - stepARules exc counter ts) ctxt mut + stepARules fexc counter (errs++[ie]) ts) ctxt mut _ -> return (e_ie_a, mut', wr) -- | Function 'evalRules' implements a backtracking procedure. @@ -353,16 +355,17 @@ -- -- When no rules are successfully executed to completetion a -- 'no rule exception' is thrown. -evalRules :: [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten -evalRules [] msoss = buildStep (stepARules NoRule count_backtrack_out msoss) -evalRules ((Rewrite rw_rules):rest) msoss = Rewrite $ \ctxt st -> +evalRules = evalRules' [] +evalRules' :: [IException] -> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten +evalRules' errs [] msoss = buildStep (stepARules NoRule count_backtrack_out errs msoss) +evalRules' errs ((Rewrite rw_rules):rest) msoss = Rewrite $ \ctxt st -> let (rw_res, st', wo) = rw_rules ctxt st in case rw_res of Left ie | failsRule ie -> --resets counters and state trace (showIException ie) $ runRewrite (do count_backtrack_out addToRCounter (counters wo) - evalRules rest msoss) ctxt st + evalRules' (ie:errs) rest msoss) ctxt st _ -> (rw_res, st', wo) msos_throw :: IE -> MSOS b @@ -385,9 +388,13 @@ modifyRewriteCTXT :: (RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a modifyRewriteCTXT mod (Rewrite f) = Rewrite (f . mod) + +modifyRewriteReader :: (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a +modifyRewriteReader mod (MSOS f) = MSOS (f . mod') + where mod' ctxt = ctxt { ereader = mod (ereader ctxt) } ----------------- -- | a map storing the values of /inherited/ entities. -type Inherited = M.Map Name Values +type Inherited = M.Map Name [Values] emptyINH :: Inherited emptyINH = M.empty @@ -483,7 +490,7 @@ -- | Yields an error signaling that no rule is applicable. -- The funcon term argument may be used to provide a useful error message. norule :: Funcons -> Rewrite a -norule f = rewrite_throw NoRule +norule f = rewrite_throw (NoRule []) -- | Yields an error signaling that a sort error was encountered. -- These errors render a rule /inapplicable/ and a next rule is attempted @@ -536,7 +543,8 @@ stepRewritten :: Rewritten -> MSOS StepRes stepRewritten (ValTerm vs) = return (Right vs) -stepRewritten (CompTerm _ step) = count_step >> step +stepRewritten (CompTerm f step) = modifyRewriteReader mod (count_step >> step) + where mod ctxt = ctxt {local_fct = f} -- | Returns a value as a fully rewritten term. rewritten :: Values -> Rewrite Rewritten @@ -630,6 +638,12 @@ evalFuncons :: Funcons -> MSOS StepRes evalFuncons f = liftRewrite (rewriteFuncons f) >>= stepRewritten +rewritesToType :: Funcons -> Rewrite Types +rewritesToType f = do + rewriteFunconsWcount f >>= \case + ValTerm [v@(ComputationType _)] -> return (downcastValueType v) + _ -> rewriteToValErr + rewritesToValue :: Funcons -> Rewrite Values rewritesToValue f = do rewriteFunconsWcount f >>= \case @@ -663,6 +677,9 @@ -- rewriteFuncons' (FList fs) = evalStrictSequence fs (rewritten . List) FList rewriteFuncons' (FSet fs) = evalStrictSequence fs (rewritten . setval_) FSet rewriteFuncons' (FMap fs) = evalStrictSequence fs (rewritten . mapval_) FMap + rewriteFuncons' f@(FBinding fk fv) = evalStrictSequence (fk:fv) (rewritten . tuple) mkBinding + where mkBinding (k:fvs) = FBinding k fvs + mkBinding _ = error "invalid binding-notation" rewriteFuncons' f@(FSortPower s1 fn) = case (s1,fn) of (FValue mty@(ComputationType _), FValue v) | Nat n <- upcastNaturals v -> diff --git a/src/Funcons/Patterns.hs b/src/Funcons/Patterns.hs --- a/src/Funcons/Patterns.hs +++ b/src/Funcons/Patterns.hs @@ -31,7 +31,7 @@ | otherwise -> rewrite_rethrow ie Right env' -> return [(k+1,env')] -seqMatcher :: (a -> Maybe FTerm -> Env -> Rewrite Bool) -> ([a] -> Levelled) +seqMatcher :: (a -> Maybe FTerm -> Env -> Rewrite (Maybe [a])) -> ([a] -> Levelled) -> SeqVarInfo -> Matcher a seqMatcher p level (var, op, mty) str k env = case op of QuestionMarkOp -> makeResults ((<=1) . length) @@ -43,13 +43,13 @@ furthest <- takeWhileM (\a -> p a mty env) (drop k str) return (map ins (filter filter_op $ ordered_subsequences furthest)) where - ins fs = (k+length fs, envInsert var (level fs) env) + ins fs = (k+length fs, envInsert var (level (concat fs)) env) - takeWhileM :: (a -> Rewrite Bool) -> [a] -> Rewrite [a] + takeWhileM :: (a -> Rewrite (Maybe [a])) -> [a] -> Rewrite [[a]] takeWhileM _ [] = return [] takeWhileM p (x:xs) = eval_catch (p x) >>= \case - Right True -> (x:) <$> takeWhileM p xs - Right False -> return [] + Right (Just fs) -> (fs :) <$> takeWhileM p xs + Right Nothing -> return [] Left ie | failsRule ie -> return [] | otherwise -> rewrite_rethrow ie @@ -188,17 +188,17 @@ | otherwise = matching showValues str matchers env where matchers = map toMatcher pats toMatcher pat = case vpSeqVarInfo pat of - Just info -> seqMatcher isInMaybeTermType ValuesTerm info + Just info -> seqMatcher isInMaybeTermTypePreserve ValuesTerm info Nothing -> singleMatcher vMatch pat -- | Variant of 'premiseStep' that applies substitute and pattern-matching. -premise :: FTerm -> FPattern -> Env -> MSOS Env -premise x pat env = liftRewrite (subsAndRewritesInEnv x env) >>= \case +premise :: FTerm -> [FPattern] -> Env -> MSOS Env +premise x pats env = liftRewrite (subsAndRewritesInEnv x env) >>= \case (ValTerm v, env') -> msos_throw (StepOnValue v) (CompTerm f step,env') -> do ef' <- count_delegation >> optRefocus step - case ef' of Left f' -> liftRewrite $ fMatch f' pat env' - Right vs' -> liftRewrite $ fsMatch (map FValue vs') [pat] env' + case ef' of Left f' -> liftRewrite $ fsMatch [f'] pats env' + Right vs' -> liftRewrite $ fsMatch (map FValue vs') pats env' -- | Variant of 'fsMatch' that is lifted into the 'MSOS' monad. -- If all given terms are values, then 'vsMatch' is used instead. @@ -281,7 +281,7 @@ where matchers = map toMatcher pats toMatcher pat = case tpSeqVarInfo pat of Nothing -> singleMatcher tMatch pat - Just info -> seqMatcher (\_ _ _ -> return True) TypesTerm info + Just info -> seqMatcher isInMaybeTypeTypePreserve TypesTerm info tMatch :: ComputationTypes -> TPattern -> Env -> Rewrite Env tMatch t p env = case p of @@ -336,7 +336,7 @@ -- | /~(T1 : T2)/. Accepted only when /T2/ rewrites to a type and /T1/ rewrites to a value /not/ of that type. | SCNotInSort FTerm FTerm -- | /T = P/. Accepted only when /T/ rewrites to a value that matches the pattern /P/. (May produce new bindings in 'Env'). - | SCPatternMatch FTerm VPattern + | SCPatternMatch FTerm [VPattern] -- | Variant of 'sideCondition' that is lifted into the 'MSOS' monad. lifted_sideCondition sc env = liftRewrite $ sideCondition sc env @@ -352,17 +352,18 @@ SCIsInSort term1 term2 -> prop "sort annotation" isInTuple term1 term2 env SCNotInSort term1 term2 -> prop "neg. sort annotation" (\a b -> isInTuple a b >>= return . not) term1 term2 env - SCPatternMatch term vpat -> + SCPatternMatch term vpats -> eval_catch (subsAndRewritesInEnv term env) >>= \case -- env' binds term to step or value, if possible -- courtesy of subsAndRewritesInEnv - Right (ValTerm vs, env') -> vsMatch vs [vpat] env' - Right (CompTerm lf step, env') -> case vpat of - VPMetaVar v -> return (envInsert v (FunconTerm lf (Just step)) env') - _ -> fMatch lf pat env' - Left (_,lf,PartialOp _) -> fMatch lf pat env + Right (ValTerm vs, env') -> vsMatch vs vpats env' + Right (CompTerm lf step, env') -> case vpats of + [VPMetaVar v] -> return (envInsert v (FunconTerm lf (Just step)) env') + _ -> fsMatch [lf] pats env' + Left (_,lf,PartialOp _) -> fsMatch [lf] pats env Left ie -> rewrite_rethrow ie - where pat = case vpat of + where pats = map toFPat vpats + where toFPat vpat = case vpat of VPMetaVar var -> PMetaVar var value_pat -> PValue value_pat where prop :: String -> ([Values] -> [Values] -> Rewrite Bool) -> FTerm -> FTerm -> Env -> Rewrite Env @@ -387,13 +388,26 @@ alwaysAccept :: Funcons -> Maybe FTerm -> Env -> Rewrite Bool alwaysAccept _ _ _ = return True -rewritesToAnnotatedType :: Funcons -> Maybe FTerm -> Env -> Rewrite Bool -rewritesToAnnotatedType f Nothing _ = return True +rewritesToAnnotatedType :: Funcons -> Maybe FTerm -> Env -> Rewrite (Maybe [Funcons]) +rewritesToAnnotatedType f Nothing _ = return (Just [f]) rewritesToAnnotatedType f (Just term) env = rewriteFunconsWcount f >>= \case - ValTerm [v] -> isInMaybeTermType v (Just term) env - ValTerm vs -> isInMaybeTupleType vs term env - CompTerm _ _ -> return False + ValTerm [v] -> isInMaybeTermType v (Just term) env >>= \case + True -> return (Just [FValue v]) + _ -> return Nothing + ValTerm vs -> isInMaybeTupleType vs term env >>= \case + True -> return (Just (map FValue vs)) + _ -> return Nothing + CompTerm _ _ -> return Nothing +-- to be used by seqMatcher +isInMaybeTermTypePreserve :: Values -> Maybe FTerm -> Env -> Rewrite (Maybe [Values]) +isInMaybeTermTypePreserve v mty env = isInMaybeTermType v mty env >>= \case + True -> return (Just [v]) + _ -> return Nothing + +isInMaybeTypeTypePreserve :: ComputationTypes -> Maybe FTerm -> Env -> Rewrite (Maybe [ComputationTypes]) +isInMaybeTypeTypePreserve ty _ _ = return (Just [ty]) + -- type checking isInMaybeTermType :: Values -> (Maybe FTerm) -> Env -> Rewrite Bool isInMaybeTermType v Nothing _ = return True @@ -420,6 +434,24 @@ Just ty -> Funcons.Patterns.isInType v ty isInType :: Values -> Types -> Rewrite Bool +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)] + _ -> return False +isInType v (ADT "multisets" [ty']) = case v of + Multiset ls -> do + ty <- rewritesToType ty' + and <$> mapM (flip Funcons.Patterns.isInType ty) (toList ls) + _ -> return False +isInType v (ADT "sets" [ty']) = case v of + Set ls -> do + ty <- rewritesToType ty' + and <$> mapM (flip Funcons.Patterns.isInType ty) (toList ls) + _ -> return False isInType v (ADT nm tys) = do DataTypeMemberss _ tpats alts <- typeEnvLookup nm or <$> mapM (isInAlt tpats) alts @@ -439,15 +471,6 @@ _ -> return True -- imprecision isInAlt _ _ = return False isInType v (AnnotatedType ty op) = Funcons.Patterns.isInTupleType [v] [(ty, Just op)] -isInType (Map m) (Maps kt vt) = - and <$> sequence [and <$> mapM (flip Funcons.Patterns.isInType kt) (M.keys m) - ,and <$> mapM (flip Funcons.Patterns.isInType vt) (M.elems m)] -isInType (Multiset ls) (Multisets ty) = - and <$> mapM (flip Funcons.Patterns.isInType ty) (toList ls) -isInType (Set ls) (Sets ty) = - and <$> mapM (flip Funcons.Patterns.isInType ty) (toList ls) -isInType (Vector ls) (Vectors ty) = - and <$> mapM (flip Funcons.Patterns.isInType ty) (toList ls) isInType v (Union ty1 ty2) = (||) <$> Funcons.Patterns.isInType v ty1 <*> Funcons.Patterns.isInType v ty2 isInType v (Intersection ty1 ty2) = @@ -470,7 +493,7 @@ typeEnvLookup :: Name -> Rewrite DataTypeMembers typeEnvLookup con = Rewrite $ \ctxt st -> case typeLookup con (ty_env ctxt) of - Nothing -> (Left (evalctxt2exception(Internal "type lookup failed") ctxt) + Nothing -> (Left (evalctxt2exception(Internal ("type lookup failed: " ++ unpack con)) ctxt) , st, mempty) Just members -> (Right members, st, mempty) diff --git a/src/Funcons/Printer.hs b/src/Funcons/Printer.hs --- a/src/Funcons/Printer.hs +++ b/src/Funcons/Printer.hs @@ -53,8 +53,9 @@ --ppFuncons opts (FTuple fs) = "(" ++ showArgs opts False fs ++ ")" ppFuncons opts (FSet fs) = "{" ++ showArgs opts False fs ++ "}" ppFuncons opts (FMap fs) = - "{" ++ intercalate "," (map toKeyFValue $ mkPairs fs) ++ "}" - where toKeyFValue (k,v) = ppFuncons opts k ++ " |-> " ++ ppFuncons opts v + "{" ++ intercalate "," (map (ppFuncons opts) fs) ++ "}" +ppFuncons opts (FBinding fk fvs) = + ppFuncons opts fk ++ " |-> " ++ ppFunconsSeq opts fvs ppFuncons opts (FValue v) = ppValues (ppFuncons opts) v ppFuncons opts (FName nm) = unpack nm ppFuncons opts (FSortSeq f o) = ppFuncons opts f ++ ppOp o @@ -92,7 +93,8 @@ ppTerms opts (TVar var) = var ppTerms opts (TSeq ts) = "(" ++ intercalate "," (map (ppTerms opts) ts) ++ ")" ppTerms opts (TSet ts) = "{" ++ intercalate "," (map (ppTerms opts) ts) ++ "}" -ppTerms opts (TMap ts) = "map" ++ ("(" ++ intercalate "," (map (ppTerms opts) ts) ++ ")") +ppTerms opts (TMap ts) = "map" ++ "(" ++ intercalate "," (map (ppTerms opts) ts) ++ ")" +ppTerms opts (TBinding fk fv) = ppTerms opts fk ++ " |-> " ++ ppTerms opts fv ppTerms opts (TSortSeq term op) = ppTerms opts term ++ ppOp op ppTerms opts (TSortPower t1 t2) = ppTerms opts t1 ++ "^" ++ ppTerms opts t2 ppTerms opts (TSortUnion t1 t2) = ppTerms opts t1 ++ "|" ++ show t2 diff --git a/src/Funcons/RunOptions.hs b/src/Funcons/RunOptions.hs --- a/src/Funcons/RunOptions.hs +++ b/src/Funcons/RunOptions.hs @@ -55,7 +55,7 @@ bool_opt nm m = bool_opt_default False nm m do_refocus :: RunOptions -> Bool -do_refocus opts = bool_opt "refocus" (general_opts opts) +do_refocus opts = bool_opt_default True "refocus" (general_opts opts) max_restarts :: RunOptions -> Maybe Int max_restarts = fmap read . M.lookup "max-restarts" . general_opts @@ -262,4 +262,4 @@ where insertInputs list = defaultRunOptions { given_inputs = M.fromList list } toPair nm fs = case sequence (map recursiveFunconValue fs) of Just vs -> (pack nm, vs) - _ -> error ("inputs for " ++ nm ++ " not a list") + _ -> error ("inputs for " ++ nm ++ " not a sequence of values") diff --git a/src/Funcons/Simulation.hs b/src/Funcons/Simulation.hs --- a/src/Funcons/Simulation.hs +++ b/src/Funcons/Simulation.hs @@ -44,7 +44,7 @@ return v where mLookup m = case M.lookup nm m of Just (v:_) -> FValue v - _ -> FValue none__ + _ -> FValue null_value__ mTail [] = [] mTail (_:vs) = vs diff --git a/src/Funcons/Substitution.hs b/src/Funcons/Substitution.hs --- a/src/Funcons/Substitution.hs +++ b/src/Funcons/Substitution.hs @@ -111,6 +111,7 @@ -- TList ts -> List <$> subs_flatten ts env TSet ts -> setval_ <$> subs_flatten ts env TMap ts -> mapval_ <$> subs_flatten ts env + TBinding x y -> tuple <$> subs_flatten [x,y] env TFuncon (FValue v) -> return v TAny -> return VAny _ -> internal "missing case in substitute_signal" @@ -135,6 +136,7 @@ --substitute (TList terms) env = FList <$> subsFlatten terms env substitute (TSet terms) env = FSet <$> subsFlatten terms env substitute (TMap terms) env = FMap <$> subsFlatten terms env +substitute (TBinding x y) env = FBinding <$> substitute x env <*> subsFlatten [y] env substitute (TFuncon f) env = return f substitute (TSortUnion t1 t2) env = FSortUnion <$> substitute t1 env <*> substitute t2 env substitute (TSortInter t1 t2) env = FSortInter <$> substitute t1 env <*> substitute t2 env @@ -150,7 +152,7 @@ subsFlatten :: [FTerm] -> Env -> Rewrite [Funcons] subsFlatten terms env = concat <$> (forM terms $ \case TVar k -> envLookup env k >>= fsLevel - TSeq ts -> mapM (flip substitute env) ts + TSeq ts -> subsFlatten ts env term -> (:[]) <$> substitute term env) -- Version of subsAndRewritesToValue that 'caches' computational steps: diff --git a/src/Funcons/Tools.hs b/src/Funcons/Tools.hs --- a/src/Funcons/Tools.hs +++ b/src/Funcons/Tools.hs @@ -27,6 +27,7 @@ import Funcons.Core.Library import Funcons.Core.Manual import Funcons.Printer +import Funcons.Parser import System.Environment (getArgs) @@ -226,12 +227,13 @@ displayValues vs = intercalate "," (map displayValue vs) displayValue (Map m) = intercalate "\n" - [ displayValue key ++ " |-> " ++ displayValue val + [ displayValue key ++ " |-> " ++ displayValues val | (key, val) <- M.assocs m ] displayValue (ADTVal "variable" [FValue (Atom a) ,FValue (ComputationType (Type t))]) = "variable(" ++ displayValue (Atom a) ++ ", " ++ ppTypes (ppFuncons opts) t ++ ")" - displayValue (Atom a) = "@" ++ a + displayValue (Atom a) = a + displayValue val | isString_ val = show (unString val) displayValue val = ppValues (ppFuncons opts) val printTestResults :: [Funcons] -> EntityDefaults -> MSOSReader m -> @@ -286,7 +288,7 @@ Nothing -> return () Just expected -> unless (map (localEval name) expected == [val]) - (reportError name (show $ map showFuncons expected) (showValues val)) + (reportError name (showL $ map showFuncons expected) (showValues val)) -- set default values of output and control entities ctrl :: M.Map Name (Maybe Values) @@ -309,7 +311,7 @@ display name Nothing = case M.lookup name opts of Nothing -> return () Just vals -> putStrLn ("expected "++unpack name++": " - ++ show (map (showValues . localEval name) vals)) + ++ showL (map (showValues . localEval name) vals)) -- test whether control signal is expected when there is one -- shows that the emitted signal was unexpected -- if a signal was expected, shows if actual and expected are unequal @@ -317,19 +319,22 @@ Nothing -> putStrLn ("unexpected " ++ unpack name ++ ": " ++ showValues val) Just expected -> unless (map (localEval name) expected == [val]) - (reportError name (show $ map showFuncons expected) (showValues val)) + (reportError name (showL $ map showFuncons expected) (showValues val)) printInputOutput remaining = forM_ (M.assocs remaining) (uncurry display) where -- no test-error if the input/output is empty -- (and no input/output was specified) display name [] | Nothing <- M.lookup name opts = return () display name vals = case M.lookup name opts of - Nothing -> putStrLn ("unexpected " ++ unpack name ++ ": " ++ show (map showValues vals)) + Nothing -> putStrLn ("unexpected " ++ unpack name ++ ": " ++ showL (map showValues vals)) Just expected -> case map (localEval name) expected of - [ADTVal "list" exps] -> unless (exps == map FValue vals) (reportError name (show $ map showFuncons exps) (show $ map showValues vals)) + [ADTVal "list" exps] -> unless (exps == map FValue vals) (reportError name (showL $ map showFuncons exps) (showL $ map showValues vals)) val -> error ("non-list given as expected output entity ("++ - unpack name ++ "): " ++ show (map showValues val)) + unpack name ++ "): " ++ showL (map showValues val)) +showL :: [String] -> String +showL elems = "[" ++ intercalate "," elems ++ "]" + -- $moduledoc -- This module exports functions for creating executables for funcon interpeters. diff --git a/src/Funcons/TypeSubstitution.hs b/src/Funcons/TypeSubstitution.hs --- a/src/Funcons/TypeSubstitution.hs +++ b/src/Funcons/TypeSubstitution.hs @@ -48,6 +48,7 @@ -- TList ts -> TList (map (subsTypeVarWildcard mt env) ts) TSet ts -> TSet (map (subsTypeVarWildcard mt env) ts) TMap ts -> TMap (map (subsTypeVarWildcard mt env) ts) + TBinding x y -> TBinding (subsTypeVarWildcard mt env x) (subsTypeVarWildcard mt env y) TFuncon f -> TFuncon f TSortSeq t op -> TSortSeq (subsTypeVarWildcard mt env t) op TSortPower t1 t2 -> TSortPower (subsTypeVarWildcard mt env t1) (subsTypeVarWildcard mt env t2) 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, isNoValue, isSet, map_empty_, isEnv, isDefinedVal, isString_, isChar, isVec, isType, isList, isNat, isInt, atoms_, integers_, values_, set_, list_, tuple_, atom_, nothing_, defined_values_, types_, value_types_, toList, isList) +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 qualified Data.Char as C import qualified Data.Map as M @@ -30,6 +30,7 @@ -- | FList [Funcons] | FSet [Funcons] | FMap [Funcons] + | FBinding Funcons [Funcons] -- required for map-notation | FValue Values | FSortSeq Funcons VAL.SeqSortOp | FSortPower Funcons Funcons {- evals to natural number -} @@ -56,7 +57,7 @@ | otherwise = FApp str args tuple_ :: [Funcons] -> Funcons -tuple_ = FValue . ADTVal "list" +tuple_ = applyFuncon "tuple" -- | Creates a list of funcon terms. list_ :: [Funcons] -> Funcons @@ -75,6 +76,7 @@ -- | TList [FTerm] | TSet [FTerm] | TMap [FTerm] + | TBinding FTerm FTerm -- latter can be a sequence | TFuncon Funcons | TSortSeq FTerm VAL.SeqSortOp | TSortPower FTerm FTerm {- should eval to a natural number -} @@ -135,7 +137,7 @@ unaryTypes :: [(Name,Types->Types)] unaryTypes = - [ ("multisets", Multisets) + [ ("multisets", multisets) -- , ("lists", Lists) -- , ("vectors", Vectors) ] @@ -232,8 +234,17 @@ mapval = FValue . mapval_ mapval_ :: [Values] -> Values -mapval_ = Map . M.fromList . mkPairs +mapval_ mvs = case mapM fromBinding mvs of + Just vs -> Map $ M.fromListWith const vs + _ -> error "mapval: invalid map-notation" +fromBinding :: Values -> Maybe (Values, [Values]) +fromBinding (ADTVal "tuple" (k':vs')) = do + k <- project k' + vs <- mapM project vs' + return (k,vs) +fromBinding k = Just (k,[]) + -- subtyping rationals {- @@ -279,7 +290,10 @@ recursiveFunconValue (FValue v) = Just v --recursiveFunconValue (FList fs) = List <$> mapM recursiveFunconValue fs recursiveFunconValue (FSet fs) = Set . S.fromList <$> mapM recursiveFunconValue fs -recursiveFunconValue (FMap fs) = Map . M.fromList . mkPairs <$> mapM recursiveFunconValue fs +recursiveFunconValue (FMap fs) = do + vs <- mapM recursiveFunconValue fs + assocs <- mapM fromBinding vs + return (Map $ M.fromList assocs) recursiveFunconValue _ = Nothing allEqual :: [Values] -> [Values] -> Bool @@ -288,15 +302,15 @@ allUnEqual :: [Values] -> [Values] -> Bool allUnEqual xs ys = length xs /= length ys || or (zipWith (=/=) xs ys) -isNoValue :: Funcons -> Bool -isNoValue (FValue n) = n == none__ -isNoValue _ = False +isNull :: Funcons -> Bool +isNull (FValue n) = n == null__ +isNull _ = False hasStep (FValue _) = False hasStep _ = True isVal (FValue _) = True isVal _ = False -isDefinedVal f = isVal f && not (isNoValue f) +isDefinedVal f = isVal f && not (isNull f) -- functions that check simple properties of funcons -- TODO: Some of these are used, and all are exported by Funcons.EDSL @@ -339,10 +353,9 @@ integers_ = type_ Integers unicode_characters_ = type_ UnicodeCharacters values_ = type_ VAL.Values -defined_values_ = type_ DefinedValues -nothing_ = type_ Nothings +nulltype_ = type_ NullType vectors_ :: Types -> Funcons -vectors_ = type_ . Vectors +vectors_ = type_ . vectors atoms_ = type_ Atoms -- type environment