funcons-tools 0.2.0.1 → 0.2.0.3
raw patch · 63 files changed
+1082/−738 lines, 63 filesdep ~funcons-valuesdep ~gll
Dependency ranges changed: funcons-values, gll
Files
- cbs/Funcons/Core/Computations/Abnormal/Abrupting/Abrupting.hs +9/−9
- cbs/Funcons/Core/Computations/Abnormal/Breaking/Breaking.hs +7/−7
- cbs/Funcons/Core/Computations/Abnormal/Continuing/Continuing.hs +7/−7
- cbs/Funcons/Core/Computations/Abnormal/Controlling/Controlling.hs +15/−14
- cbs/Funcons/Core/Computations/Abnormal/Failing/Failing.hs +10/−11
- cbs/Funcons/Core/Computations/Abnormal/Returning/Returning.hs +7/−7
- cbs/Funcons/Core/Computations/Abnormal/Throwing/Throwing.hs +10/−10
- cbs/Funcons/Core/Computations/Normal/Binding/Binding.hs +21/−22
- cbs/Funcons/Core/Computations/Normal/Flowing/Flowing.hs +64/−78
- cbs/Funcons/Core/Computations/Normal/Generating/Generating.hs +3/−3
- cbs/Funcons/Core/Computations/Normal/Giving/Giving.hs +32/−24
- cbs/Funcons/Core/Computations/Normal/Interacting/Interacting.hs +5/−5
- cbs/Funcons/Core/Computations/Normal/Linking/Linking.hs +8/−9
- cbs/Funcons/Core/Computations/Normal/Storing/Storing.hs +48/−55
- cbs/Funcons/Core/Library.hs +111/−105
- cbs/Funcons/Core/Values/Abstraction/Functions/Functions.hs +9/−9
- cbs/Funcons/Core/Values/Abstraction/Generic/Generic.hs +3/−3
- cbs/Funcons/Core/Values/Abstraction/Patterns/Patterns.hs +31/−31
- cbs/Funcons/Core/Values/Abstraction/Thunks/Thunks.hs +4/−4
- cbs/Funcons/Core/Values/Composite/Bits/Bits.hs +8/−8
- cbs/Funcons/Core/Values/Composite/Classes/Classes.hs +77/−0
- cbs/Funcons/Core/Values/Composite/Datatypes/Datatypes.hs +3/−3
- cbs/Funcons/Core/Values/Composite/Graphs/Graphs.hs +3/−3
- cbs/Funcons/Core/Values/Composite/Lists/Lists.hs +8/−8
- cbs/Funcons/Core/Values/Composite/Maps/Maps.hs +24/−0
- cbs/Funcons/Core/Values/Composite/Objects/Objects.hs +78/−0
- cbs/Funcons/Core/Values/Composite/Records/Records.hs +14/−6
- cbs/Funcons/Core/Values/Composite/References/References.hs +14/−13
- cbs/Funcons/Core/Values/Composite/Sequences/Sequences.hs +42/−58
- cbs/Funcons/Core/Values/Composite/Strings/Strings.hs +1/−1
- cbs/Funcons/Core/Values/Composite/Trees/Trees.hs +96/−0
- cbs/Funcons/Core/Values/Composite/Tuples/Tuples.hs +4/−4
- cbs/Funcons/Core/Values/Composite/Variants/Variants.hs +7/−7
- cbs/Funcons/Core/Values/Composite/Vectors/Vectors.hs +2/−2
- cbs/Funcons/Core/Values/Primitive/Booleans/Booleans.hs +3/−3
- cbs/Funcons/Core/Values/Primitive/Characters/Characters.hs +3/−3
- cbs/Funcons/Core/Values/Primitive/Floats/Floats.hs +1/−1
- cbs/Funcons/Core/Values/Primitive/Integers/Integers.hs +1/−1
- cbs/Funcons/Core/Values/Primitive/Null/Null.hs +25/−0
- cbs/Funcons/Core/Values/Primitive/Unit/Unit.hs +0/−25
- cbs/Funcons/Core/Values/ValueTypes/ValueTypes.hs +34/−21
- funcons-tools.cabal +26/−28
- manual/Funcons/Core/Computations/Normal/GeneratingBuiltin.hs +1/−1
- manual/Funcons/Core/Values/Composite/MapsBuiltin.hs +2/−4
- manual/Funcons/Core/Values/Composite/MultisetsBuiltin.hs +1/−1
- manual/Funcons/Core/Values/Primitive/BoolBuiltin.hs +1/−1
- manual/Funcons/Core/Values/Primitive/CharactersBuiltin.hs +2/−2
- manual/Funcons/Core/Values/TypesBuiltin.hs +4/−6
- manual/Funcons/MetaProgramming.hs +12/−7
- src/Funcons/Core.hs +2/−2
- src/Funcons/EDSL.hs +2/−2
- src/Funcons/Entities.hs +12/−13
- src/Funcons/Exceptions.hs +18/−8
- src/Funcons/GLLParser.hs +4/−3
- src/Funcons/MSOS.hs +36/−19
- src/Funcons/Patterns.hs +57/−34
- src/Funcons/Printer.hs +5/−3
- src/Funcons/RunOptions.hs +2/−2
- src/Funcons/Simulation.hs +1/−1
- src/Funcons/Substitution.hs +3/−1
- src/Funcons/Tools.hs +13/−8
- src/Funcons/TypeSubstitution.hs +1/−0
- src/Funcons/Types.hs +25/−12
cbs/Funcons/Core/Computations/Abnormal/Abrupting/Abrupting.hs view
@@ -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
cbs/Funcons/Core/Computations/Abnormal/Breaking/Breaking.hs view
@@ -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
cbs/Funcons/Core/Computations/Abnormal/Continuing/Continuing.hs view
@@ -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
cbs/Funcons/Core/Computations/Abnormal/Controlling/Controlling.hs view
@@ -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
cbs/Funcons/Core/Computations/Abnormal/Failing/Failing.hs view
@@ -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"
cbs/Funcons/Core/Computations/Abnormal/Returning/Returning.hs view
@@ -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
cbs/Funcons/Core/Computations/Abnormal/Throwing/Throwing.hs view
@@ -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"
cbs/Funcons/Core/Computations/Normal/Binding/Binding.hs view
@@ -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" []
cbs/Funcons/Core/Computations/Normal/Flowing/Flowing.hs view
@@ -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" []
cbs/Funcons/Core/Computations/Normal/Generating/Generating.hs view
@@ -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
cbs/Funcons/Core/Computations/Normal/Giving/Giving.hs view
@@ -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
cbs/Funcons/Core/Computations/Normal/Interacting/Interacting.hs view
@@ -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
cbs/Funcons/Core/Computations/Normal/Linking/Linking.hs view
@@ -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"
cbs/Funcons/Core/Computations/Normal/Storing/Storing.hs view
@@ -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" []
cbs/Funcons/Core/Library.hs view
@@ -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 ]
cbs/Funcons/Core/Values/Abstraction/Functions/Functions.hs view
@@ -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"
cbs/Funcons/Core/Values/Abstraction/Generic/Generic.hs view
@@ -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)
cbs/Funcons/Core/Values/Abstraction/Patterns/Patterns.hs view
@@ -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"
cbs/Funcons/Core/Values/Abstraction/Thunks/Thunks.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Bits/Bits.hs view
@@ -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"
+ cbs/Funcons/Core/Values/Composite/Classes/Classes.hs view
@@ -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" []
cbs/Funcons/Core/Values/Composite/Datatypes/Datatypes.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Graphs/Graphs.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Lists/Lists.hs view
@@ -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"
+ cbs/Funcons/Core/Values/Composite/Maps/Maps.hs view
@@ -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" []
+ cbs/Funcons/Core/Values/Composite/Objects/Objects.hs view
@@ -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" []
cbs/Funcons/Core/Values/Composite/Records/Records.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/References/References.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Sequences/Sequences.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Strings/Strings.hs view
@@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values)+import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList
+ cbs/Funcons/Core/Values/Composite/Trees/Trees.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Tuples/Tuples.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Variants/Variants.hs view
@@ -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
cbs/Funcons/Core/Values/Composite/Vectors/Vectors.hs view
@@ -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)
cbs/Funcons/Core/Values/Primitive/Booleans/Booleans.hs view
@@ -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
cbs/Funcons/Core/Values/Primitive/Characters/Characters.hs view
@@ -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] []
cbs/Funcons/Core/Values/Primitive/Floats/Floats.hs view
@@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values)+import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList
cbs/Funcons/Core/Values/Primitive/Integers/Integers.hs view
@@ -5,7 +5,7 @@ import Funcons.EDSL -import Funcons.Operations hiding (Values)+import Funcons.Operations hiding (Values,libFromList) entities = [] types = typeEnvFromList
+ cbs/Funcons/Core/Values/Primitive/Null/Null.hs view
@@ -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" []
− cbs/Funcons/Core/Values/Primitive/Unit/Unit.hs
@@ -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" []
cbs/Funcons/Core/Values/ValueTypes/ValueTypes.hs view
@@ -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)
funcons-tools.cabal view
@@ -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 (<http://plancomps.org>) 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: <http://plancomps.org>.- Read more about funcons and their specification in CBS here: <http://plancomps.dreamhosters.com/wp-content/uploads/2016/02/jlamp-16.pdf JLAMP2016>.- . 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
manual/Funcons/Core/Computations/Normal/GeneratingBuiltin.hs view
@@ -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)
manual/Funcons/Core/Values/Composite/MapsBuiltin.hs view
@@ -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"
manual/Funcons/Core/Values/Composite/MultisetsBuiltin.hs view
@@ -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
manual/Funcons/Core/Values/Primitive/BoolBuiltin.hs view
@@ -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 []
manual/Funcons/Core/Values/Primitive/CharactersBuiltin.hs view
@@ -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_)
manual/Funcons/Core/Values/TypesBuiltin.hs view
@@ -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"
manual/Funcons/MetaProgramming.hs view
@@ -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)
src/Funcons/Core.hs view
@@ -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_)
src/Funcons/EDSL.hs view
@@ -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
src/Funcons/Entities.hs view
@@ -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
src/Funcons/Exceptions.hs view
@@ -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
src/Funcons/GLLParser.hs view
@@ -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" <:=>
src/Funcons/MSOS.hs view
@@ -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 ->
src/Funcons/Patterns.hs view
@@ -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)
src/Funcons/Printer.hs view
@@ -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
src/Funcons/RunOptions.hs view
@@ -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")
src/Funcons/Simulation.hs view
@@ -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
src/Funcons/Substitution.hs view
@@ -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:
src/Funcons/Tools.hs view
@@ -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.
src/Funcons/TypeSubstitution.hs view
@@ -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)
src/Funcons/Types.hs view
@@ -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