-- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Abstraction/Patterns/Patterns.cbs
{-# LANGUAGE OverloadedStrings #-}

module Funcons.Core.Values.Abstraction.Patterns.Patterns where

import Funcons.EDSL

import Funcons.Operations hiding (Values,libFromList)
entities :: [a]
entities = []

types :: TypeRelation
types = [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList
    [(Name
"patterns",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"patterns" [] [Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"pattern" [Name -> [FTerm] -> FTerm
TApp Name
"abstractions" [FTerm -> FTerm -> FTerm
TSortComputesFrom (Name -> FTerm
TName Name
"values") (Name -> FTerm
TName Name
"environments")]] ([TPattern] -> Maybe [TPattern]
forall a. a -> Maybe a
Just [])])]

funcons :: FunconLibrary
funcons = [(Name, EvalFunction)] -> FunconLibrary
libFromList
    [(Name
"pattern",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepPattern),(Name
"pattern-any",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepPattern_any),(Name
"pattern-bind",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepPattern_bind),(Name
"pattern-type",NonStrictFuncon -> EvalFunction
NonStrictFuncon NonStrictFuncon
stepPattern_type),(Name
"pattern-else",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepPattern_else),(Name
"pattern-unite",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepPattern_unite),(Name
"match",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepMatch),(Name
"match-loosely",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepMatch_loosely),(Name
"case-match",[Strictness] -> Strictness -> NonStrictFuncon -> EvalFunction
PartiallyStrictFuncon [Strictness
Strict,Strictness
NonStrict] Strictness
NonStrict NonStrictFuncon
stepCase_match),(Name
"case-match-loosely",[Strictness] -> Strictness -> NonStrictFuncon -> EvalFunction
PartiallyStrictFuncon [Strictness
Strict,Strictness
NonStrict] Strictness
NonStrict NonStrictFuncon
stepCase_match_loosely),(Name
"case-variant-value",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepCase_variant_value),(Name
"patterns",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepPatterns)]

pattern_ :: [Funcons] -> Funcons
pattern_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"pattern" ([Funcons]
fargs)
stepPattern :: StrictFuncon
stepPattern [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [MetaVar -> VPattern
VPMetaVar MetaVar
"_X1"] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"_X1") (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp)) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"datatype-value" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
112)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
97)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
114)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
110)])])),MetaVar -> FTerm
TVar MetaVar
"_X1"]) Env
env

pattern_any_ :: Funcons
pattern_any_ = Name -> Funcons
FName Name
"pattern-any"
stepPattern_any :: NullaryFuncon
stepPattern_any = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"pattern" [Name -> [FTerm] -> FTerm
TApp Name
"abstraction" [Name -> [FTerm] -> FTerm
TApp Name
"map" []]]) Env
forall k a. Map k a
env

pattern_bind_ :: [Funcons] -> Funcons
pattern_bind_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"pattern-bind" ([Funcons]
fargs)
stepPattern_bind :: StrictFuncon
stepPattern_bind [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I") (Name -> FTerm
TName Name
"identifiers")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"pattern" [Name -> [FTerm] -> FTerm
TApp Name
"abstraction" [Name -> [FTerm] -> FTerm
TApp Name
"bind-value" [MetaVar -> FTerm
TVar MetaVar
"I",Name -> FTerm
TName Name
"given"]]]) Env
env

pattern_type_ :: [Funcons] -> Funcons
pattern_type_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"pattern-type" ([Funcons]
fargs)
stepPattern_type :: NonStrictFuncon
stepPattern_type [Funcons]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [MetaVar -> FPattern
PMetaVar MetaVar
"T"] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"pattern" [Name -> [FTerm] -> FTerm
TApp Name
"abstraction" [Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-in-type" [Name -> FTerm
TName Name
"given",MetaVar -> FTerm
TVar MetaVar
"T"],Name -> [FTerm] -> FTerm
TApp Name
"map" [],Name -> FTerm
TName Name
"fail"]]]) Env
env

pattern_else_ :: [Funcons] -> Funcons
pattern_else_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"pattern-else" ([Funcons]
fargs)
stepPattern_else :: StrictFuncon
stepPattern_else [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"P1") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"P2") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"pattern" [Name -> [FTerm] -> FTerm
TApp Name
"abstraction" [Name -> [FTerm] -> FTerm
TApp Name
"else" [Name -> [FTerm] -> FTerm
TApp Name
"match" [Name -> FTerm
TName Name
"given",MetaVar -> FTerm
TVar MetaVar
"P1"],Name -> [FTerm] -> FTerm
TApp Name
"match" [Name -> FTerm
TName Name
"given",MetaVar -> FTerm
TVar MetaVar
"P2"]]]]) Env
env

pattern_unite_ :: [Funcons] -> Funcons
pattern_unite_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"pattern-unite" ([Funcons]
fargs)
stepPattern_unite :: StrictFuncon
stepPattern_unite [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"P1") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"P2") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"pattern" [Name -> [FTerm] -> FTerm
TApp Name
"abstraction" [Name -> [FTerm] -> FTerm
TApp Name
"collateral" [Name -> [FTerm] -> FTerm
TApp Name
"match" [Name -> FTerm
TName Name
"given",MetaVar -> FTerm
TVar MetaVar
"P1"],Name -> [FTerm] -> FTerm
TApp Name
"match" [Name -> FTerm
TName Name
"given",MetaVar -> FTerm
TVar MetaVar
"P2"]]]]) Env
env

match_ :: [Funcons] -> Funcons
match_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"match" ([Funcons]
fargs)
stepMatch :: StrictFuncon
stepMatch [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2,NullaryFuncon
rewrite3,NullaryFuncon
rewrite4,NullaryFuncon
rewrite5] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values"),Name -> [VPattern] -> VPattern
PADT Name
"pattern" [Name -> [VPattern] -> VPattern
PADT Name
"abstraction" [MetaVar -> VPattern
VPMetaVar MetaVar
"X"]]] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"give" [MetaVar -> FTerm
TVar MetaVar
"V",MetaVar -> FTerm
TVar MetaVar
"X"]) Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I1") (Name -> FTerm
TName Name
"identifiers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V1*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)],Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I2") (Name -> FTerm
TName Name
"identifiers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V2*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)]] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCInequality (MetaVar -> FTerm
TVar MetaVar
"I2") (Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
112)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
97)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
114)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
110)])])))) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"I1",MetaVar -> FTerm
TVar MetaVar
"I2"]],Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [Name -> [FTerm] -> FTerm
TApp Name
"length" [MetaVar -> FTerm
TVar MetaVar
"V1*"],Name -> [FTerm] -> FTerm
TApp Name
"length" [MetaVar -> FTerm
TVar MetaVar
"V2*"]]],Name -> [FTerm] -> FTerm
TApp Name
"collateral" [Name -> [FTerm] -> FTerm
TApp Name
"interleave-map" [Name -> [FTerm] -> FTerm
TApp Name
"match" [Name -> [FTerm] -> FTerm
TApp Name
"tuple-elements" [Name -> FTerm
TName Name
"given"]],Name -> [FTerm] -> FTerm
TApp Name
"tuple-zip" [Name -> [FTerm] -> FTerm
TApp Name
"tuple" [MetaVar -> FTerm
TVar MetaVar
"V1*"],Name -> [FTerm] -> FTerm
TApp Name
"tuple" [MetaVar -> FTerm
TVar MetaVar
"V2*"]]]]]) Env
env
          rewrite3 :: NullaryFuncon
rewrite3 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M1") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp]),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M2") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp])] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M2"]) ([FTerm] -> FTerm
TSet [])) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M1"],[FTerm] -> FTerm
TSet []],Name -> [FTerm] -> FTerm
TApp Name
"map" [],Name -> FTerm
TName Name
"fail"]) Env
env
          rewrite4 :: NullaryFuncon
rewrite4 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M1") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp]),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M2") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp])] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCInequality (Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M2"]) ([FTerm] -> FTerm
TSet [])) Env
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"some-element" [Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M2"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"K"]) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"K",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M1"]],Name -> [FTerm] -> FTerm
TApp Name
"collateral" [Name -> [FTerm] -> FTerm
TApp Name
"match" [Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"M1",MetaVar -> FTerm
TVar MetaVar
"K"],Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"M2",MetaVar -> FTerm
TVar MetaVar
"K"]],Name -> [FTerm] -> FTerm
TApp Name
"match" [Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"M1",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"K"]],Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"M2",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"K"]]]],Name -> FTerm
TName Name
"fail"]) Env
env
          rewrite5 :: NullaryFuncon
rewrite5 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"P") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"P") (FTerm -> FTerm
TSortComplement (FTerm -> FTerm -> FTerm
TSortUnion (Name -> FTerm
TName Name
"datatype-values") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp])))) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"V",MetaVar -> FTerm
TVar MetaVar
"P"],Name -> [FTerm] -> FTerm
TApp Name
"map" [],Name -> FTerm
TName Name
"fail"]) Env
env

match_loosely_ :: [Funcons] -> Funcons
match_loosely_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"match-loosely" ([Funcons]
fargs)
stepMatch_loosely :: StrictFuncon
stepMatch_loosely [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2,NullaryFuncon
rewrite3,NullaryFuncon
rewrite4,NullaryFuncon
rewrite5] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values"),Name -> [VPattern] -> VPattern
PADT Name
"pattern" [Name -> [VPattern] -> VPattern
PADT Name
"abstraction" [MetaVar -> VPattern
VPMetaVar MetaVar
"X"]]] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"give" [MetaVar -> FTerm
TVar MetaVar
"V",MetaVar -> FTerm
TVar MetaVar
"X"]) Env
env
          rewrite2 :: NullaryFuncon
rewrite2 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I1") (Name -> FTerm
TName Name
"identifiers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V1*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)],Name -> [VPattern] -> VPattern
PADT Name
"datatype-value" [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I2") (Name -> FTerm
TName Name
"identifiers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V2*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)]] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCInequality (MetaVar -> FTerm
TVar MetaVar
"I2") (Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
112)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
97)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
114)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
110)])])))) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"sequential" [Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"I1",MetaVar -> FTerm
TVar MetaVar
"I2"]],Name -> [FTerm] -> FTerm
TApp Name
"check-true" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [Name -> [FTerm] -> FTerm
TApp Name
"length" [MetaVar -> FTerm
TVar MetaVar
"V1*"],Name -> [FTerm] -> FTerm
TApp Name
"length" [MetaVar -> FTerm
TVar MetaVar
"V2*"]]],Name -> [FTerm] -> FTerm
TApp Name
"collateral" [Name -> [FTerm] -> FTerm
TApp Name
"interleave-map" [Name -> [FTerm] -> FTerm
TApp Name
"match-loosely" [Name -> [FTerm] -> FTerm
TApp Name
"tuple-elements" [Name -> FTerm
TName Name
"given"]],Name -> [FTerm] -> FTerm
TApp Name
"tuple-zip" [Name -> [FTerm] -> FTerm
TApp Name
"tuple" [MetaVar -> FTerm
TVar MetaVar
"V1*"],Name -> [FTerm] -> FTerm
TApp Name
"tuple" [MetaVar -> FTerm
TVar MetaVar
"V2*"]]]]]) Env
env
          rewrite3 :: NullaryFuncon
rewrite3 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M1") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp]),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M2") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp])] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M2"]) ([FTerm] -> FTerm
TSet [])) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"map" []) Env
env
          rewrite4 :: NullaryFuncon
rewrite4 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M1") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp]),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M2") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp])] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCInequality (Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M2"]) ([FTerm] -> FTerm
TSet [])) Env
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"some-element" [Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M2"]]) [MetaVar -> VPattern
VPMetaVar MetaVar
"K"]) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-in-set" [MetaVar -> FTerm
TVar MetaVar
"K",Name -> [FTerm] -> FTerm
TApp Name
"dom" [MetaVar -> FTerm
TVar MetaVar
"M1"]],Name -> [FTerm] -> FTerm
TApp Name
"collateral" [Name -> [FTerm] -> FTerm
TApp Name
"match-loosely" [Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"M1",MetaVar -> FTerm
TVar MetaVar
"K"],Name -> [FTerm] -> FTerm
TApp Name
"map-lookup" [MetaVar -> FTerm
TVar MetaVar
"M2",MetaVar -> FTerm
TVar MetaVar
"K"]],Name -> [FTerm] -> FTerm
TApp Name
"match-loosely" [Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"M1",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"K"]],Name -> [FTerm] -> FTerm
TApp Name
"map-delete" [MetaVar -> FTerm
TVar MetaVar
"M2",[FTerm] -> FTerm
TSet [MetaVar -> FTerm
TVar MetaVar
"K"]]]],Name -> FTerm
TName Name
"fail"]) Env
env
          rewrite5 :: NullaryFuncon
rewrite5 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"DV") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"P") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"P") (FTerm -> FTerm
TSortComplement (FTerm -> FTerm -> FTerm
TSortUnion (Name -> FTerm
TName Name
"datatype-values") (Name -> [FTerm] -> FTerm
TApp Name
"maps" [FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp,FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp])))) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"if-true-else" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"DV",MetaVar -> FTerm
TVar MetaVar
"P"],Name -> [FTerm] -> FTerm
TApp Name
"map" [],Name -> FTerm
TName Name
"fail"]) Env
env

case_match_ :: [Funcons] -> Funcons
case_match_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"case-match" ([Funcons]
fargs)
stepCase_match :: NonStrictFuncon
stepCase_match [Funcons]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"P") (Name -> FTerm
TName Name
"values"),MetaVar -> FPattern
PMetaVar MetaVar
"X"] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"scope" [Name -> [FTerm] -> FTerm
TApp Name
"match" [Name -> FTerm
TName Name
"given",MetaVar -> FTerm
TVar MetaVar
"P"],MetaVar -> FTerm
TVar MetaVar
"X"]) Env
env

case_match_loosely_ :: [Funcons] -> Funcons
case_match_loosely_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"case-match-loosely" ([Funcons]
fargs)
stepCase_match_loosely :: NonStrictFuncon
stepCase_match_loosely [Funcons]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
fargs [FPattern -> FTerm -> FPattern
PAnnotated (MetaVar -> FPattern
PMetaVar MetaVar
"P") (Name -> FTerm
TName Name
"values"),MetaVar -> FPattern
PMetaVar MetaVar
"X"] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"scope" [Name -> [FTerm] -> FTerm
TApp Name
"match-loosely" [Name -> FTerm
TName Name
"given",MetaVar -> FTerm
TVar MetaVar
"P"],MetaVar -> FTerm
TVar MetaVar
"X"]) Env
env

case_variant_value_ :: [Funcons] -> Funcons
case_variant_value_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"case-variant-value" ([Funcons]
fargs)
stepCase_variant_value :: StrictFuncon
stepCase_variant_value [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"I") (Name -> FTerm
TName Name
"identifiers")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"case-match" [Name -> [FTerm] -> FTerm
TApp Name
"variant" [MetaVar -> FTerm
TVar MetaVar
"I",Name -> FTerm
TName Name
"pattern-any"],Name -> [FTerm] -> FTerm
TApp Name
"variant-value" [Name -> FTerm
TName Name
"given"]]) Env
env

patterns_ :: Funcons
patterns_ = Name -> Funcons
FName Name
"patterns"
stepPatterns :: NullaryFuncon
stepPatterns = Name -> StrictFuncon
rewriteType Name
"patterns" []