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

module Funcons.Core.Values.Composite.Sequences.Sequences where

import Funcons.EDSL

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

types :: TypeRelation
types = [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList
    []

funcons :: FunconLibrary
funcons = [(Name, EvalFunction)] -> FunconLibrary
libFromList
    [(Name
"length",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepLength),(Name
"is-in",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_in),(Name
"index",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIndex),(Name
"first",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepFirst),(Name
"second",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSecond),(Name
"third",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepThird),(Name
"first-n",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepFirst_n),(Name
"drop-first-n",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepDrop_first_n),(Name
"reverse",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepReverse),(Name
"n-of",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepN_of),(Name
"intersperse",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIntersperse)]

length_ :: [Funcons] -> Funcons
length_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"length" ([Funcons]
fargs)
stepLength :: StrictFuncon
stepLength [Values]
fargs =
    [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules [Rewrite Rewritten
rewrite1,Rewrite Rewritten
rewrite2] []
    where rewrite1 :: Rewrite Rewritten
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 [] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
0))) Env
env
          rewrite2 :: Rewrite Rewritten
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 [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"natural-successor" [Name -> [FTerm] -> FTerm
TApp Name
"length" [MetaVar -> FTerm
TVar MetaVar
"V*"]]) Env
env

is_in_ :: [Funcons] -> Funcons
is_in_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-in" ([Funcons]
fargs)
stepIs_in :: StrictFuncon
stepIs_in [Values]
fargs =
    [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules [Rewrite Rewritten
rewrite1,Rewrite Rewritten
rewrite2] []
    where rewrite1 :: Rewrite Rewritten
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"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V'") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"or" [Name -> [FTerm] -> FTerm
TApp Name
"is-equal" [MetaVar -> FTerm
TVar MetaVar
"V",MetaVar -> FTerm
TVar MetaVar
"V'"],Name -> [FTerm] -> FTerm
TApp Name
"is-in" [MetaVar -> FTerm
TVar MetaVar
"V",MetaVar -> FTerm
TVar MetaVar
"V*"]]) Env
env
          rewrite2 :: Rewrite Rewritten
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 [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env

index_ :: [Funcons] -> Funcons
index_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"index" ([Funcons]
fargs)
stepIndex :: StrictFuncon
stepIndex [Values]
fargs =
    [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules [Rewrite Rewritten
rewrite1,Rewrite Rewritten
rewrite2,Rewrite Rewritten
rewrite3,Rewrite Rewritten
rewrite4] []
    where rewrite1 :: Rewrite Rewritten
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 [Values -> VPattern
VPLit (Integer -> Values
forall t. Integer -> Values t
Nat Integer
1),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env
          rewrite2 :: Rewrite Rewritten
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 [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"positive-integers"),VPattern -> FTerm -> VPattern
VPAnnotated VPattern
VPWildCard (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" 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 -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"natural-predecessor" [MetaVar -> FTerm
TVar MetaVar
"N"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"N'"]) Env
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"index" [MetaVar -> FTerm
TVar MetaVar
"N'",MetaVar -> FTerm
TVar MetaVar
"V*"]) Env
env
          rewrite3 :: Rewrite Rewritten
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 [Values -> VPattern
VPLit (Integer -> Values
forall t. Integer -> Values t
Nat Integer
0),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq []) Env
env
          rewrite4 :: Rewrite Rewritten
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 VPattern
VPWildCard (Name -> FTerm
TName Name
"positive-integers")] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq []) Env
env

first_ :: [Funcons] -> Funcons
first_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"first" ([Funcons]
fargs)
stepFirst :: StrictFuncon
stepFirst [Values]
fargs =
    [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules [Rewrite Rewritten
rewrite1] []
    where rewrite1 :: Rewrite Rewritten
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"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env

second_ :: [Funcons] -> Funcons
second_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"second" ([Funcons]
fargs)
stepSecond :: StrictFuncon
stepSecond [Values]
fargs =
    [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules [Rewrite Rewritten
rewrite1] []
    where rewrite1 :: Rewrite Rewritten
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 VPattern
VPWildCard (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env

third_ :: [Funcons] -> Funcons
third_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"third" ([Funcons]
fargs)
stepThird :: StrictFuncon
stepThird [Values]
fargs =
    [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules [Rewrite Rewritten
rewrite1] []
    where rewrite1 :: Rewrite Rewritten
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 VPattern
VPWildCard (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated VPattern
VPWildCard (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env

first_n_ :: [Funcons] -> Funcons
first_n_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"first-n" ([Funcons]
fargs)
stepFirst_n :: StrictFuncon
stepFirst_n [Values]
fargs =
    [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules [Rewrite Rewritten
rewrite1,Rewrite Rewritten
rewrite2,Rewrite Rewritten
rewrite3] []
    where rewrite1 :: Rewrite Rewritten
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 [Values -> VPattern
VPLit (Integer -> Values
forall t. Integer -> Values t
Nat Integer
0),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq []) Env
env
          rewrite2 :: Rewrite Rewritten
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 [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"positive-integers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" 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 -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"natural-predecessor" [MetaVar -> FTerm
TVar MetaVar
"N"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"N'"]) Env
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq [MetaVar -> FTerm
TVar MetaVar
"V",Name -> [FTerm] -> FTerm
TApp Name
"first-n" [MetaVar -> FTerm
TVar MetaVar
"N'",MetaVar -> FTerm
TVar MetaVar
"V*"]]) Env
env
          rewrite3 :: Rewrite Rewritten
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
"N") (Name -> FTerm
TName Name
"positive-integers")] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq []) Env
env

drop_first_n_ :: [Funcons] -> Funcons
drop_first_n_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"drop-first-n" ([Funcons]
fargs)
stepDrop_first_n :: StrictFuncon
stepDrop_first_n [Values]
fargs =
    [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules [Rewrite Rewritten
rewrite1,Rewrite Rewritten
rewrite2,Rewrite Rewritten
rewrite3] []
    where rewrite1 :: Rewrite Rewritten
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 [Values -> VPattern
VPLit (Integer -> Values
forall t. Integer -> Values t
Nat Integer
0),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"V*") Env
env
          rewrite2 :: Rewrite Rewritten
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 [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"positive-integers"),VPattern -> FTerm -> VPattern
VPAnnotated VPattern
VPWildCard (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" 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 -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"natural-predecessor" [MetaVar -> FTerm
TVar MetaVar
"N"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"N'"]) Env
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"drop-first-n" [MetaVar -> FTerm
TVar MetaVar
"N'",MetaVar -> FTerm
TVar MetaVar
"V*"]) Env
env
          rewrite3 :: Rewrite Rewritten
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
"N") (Name -> FTerm
TName Name
"positive-integers")] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq []) Env
env

reverse_ :: [Funcons] -> Funcons
reverse_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"reverse" ([Funcons]
fargs)
stepReverse :: StrictFuncon
stepReverse [Values]
fargs =
    [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules [Rewrite Rewritten
rewrite1,Rewrite Rewritten
rewrite2] []
    where rewrite1 :: Rewrite Rewritten
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 [] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq []) Env
env
          rewrite2 :: Rewrite Rewritten
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 [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq [Name -> [FTerm] -> FTerm
TApp Name
"reverse" [MetaVar -> FTerm
TVar MetaVar
"V*"],MetaVar -> FTerm
TVar MetaVar
"V"]) Env
env

n_of_ :: [Funcons] -> Funcons
n_of_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"n-of" ([Funcons]
fargs)
stepN_of :: StrictFuncon
stepN_of [Values]
fargs =
    [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules [Rewrite Rewritten
rewrite1,Rewrite Rewritten
rewrite2] []
    where rewrite1 :: Rewrite Rewritten
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 [Values -> VPattern
VPLit (Integer -> Values
forall t. Integer -> Values t
Nat Integer
0),VPattern -> FTerm -> VPattern
VPAnnotated VPattern
VPWildCard (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq []) Env
env
          rewrite2 :: Rewrite Rewritten
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 [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"positive-integers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> [VPattern] -> SideCondition
SCPatternMatch (Name -> [FTerm] -> FTerm
TApp Name
"natural-predecessor" [MetaVar -> FTerm
TVar MetaVar
"N"]) [MetaVar -> VPattern
VPMetaVar MetaVar
"N'"]) Env
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq [MetaVar -> FTerm
TVar MetaVar
"V",Name -> [FTerm] -> FTerm
TApp Name
"n-of" [MetaVar -> FTerm
TVar MetaVar
"N'",MetaVar -> FTerm
TVar MetaVar
"V"]]) Env
env

intersperse_ :: [Funcons] -> Funcons
intersperse_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"intersperse" ([Funcons]
fargs)
stepIntersperse :: StrictFuncon
stepIntersperse [Values]
fargs =
    [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules [Rewrite Rewritten
rewrite1,Rewrite Rewritten
rewrite2,Rewrite Rewritten
rewrite3] []
    where rewrite1 :: Rewrite Rewritten
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 VPattern
VPWildCard (Name -> FTerm
TName Name
"values")] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq []) Env
env
          rewrite2 :: Rewrite Rewritten
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 [VPattern -> FTerm -> VPattern
VPAnnotated VPattern
VPWildCard (Name -> FTerm
TName Name
"values"),MetaVar -> VPattern
VPMetaVar MetaVar
"V"] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env
          rewrite3 :: Rewrite Rewritten
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
"V'") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V1") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V2") (Name -> FTerm
TName Name
"values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"V*" SeqSortOp
StarOp) (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
StarOp)] Env
forall k a. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq [MetaVar -> FTerm
TVar MetaVar
"V1",MetaVar -> FTerm
TVar MetaVar
"V'",Name -> [FTerm] -> FTerm
TApp Name
"intersperse" [MetaVar -> FTerm
TVar MetaVar
"V'",MetaVar -> FTerm
TVar MetaVar
"V2",MetaVar -> FTerm
TVar MetaVar
"V*"]]) Env
env