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

module Funcons.Core.Values.Primitive.Integers.Integers 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
"bounded-integers",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBounded_integers),(Name
"bounded-ints",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBounded_integers),(Name
"positive-integers",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepPositive_integers),(Name
"pos-ints",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepPositive_integers),(Name
"negative-integers",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepNegative_integers),(Name
"neg-ints",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepNegative_integers),(Name
"natural-numbers",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepNatural_numbers),(Name
"nats",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepNatural_numbers),(Name
"integer-negate",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepInteger_negate),(Name
"int-neg",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepInteger_negate),(Name
"integer-sequence",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepInteger_sequence)]

bounded_integers_ :: [Funcons] -> Funcons
bounded_integers_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"bounded-integers" ([Funcons]
fargs)
bounded_ints_ :: [Funcons] -> Funcons
bounded_ints_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"bounded-integers" ([Funcons]
fargs)
stepBounded_integers :: StrictFuncon
stepBounded_integers [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
"M") (Name -> FTerm
TName Name
"integers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"integers")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (FTerm -> FTerm -> FTerm
TSortInter (Name -> [FTerm] -> FTerm
TApp Name
"integers-from" [MetaVar -> FTerm
TVar MetaVar
"M"]) (Name -> [FTerm] -> FTerm
TApp Name
"integers-up-to" [MetaVar -> FTerm
TVar MetaVar
"N"])) Env
env

positive_integers_ :: Funcons
positive_integers_ = Name -> Funcons
FName Name
"positive-integers"
pos_ints_ :: Funcons
pos_ints_ = Name -> Funcons
FName Name
"positive-integers"
stepPositive_integers :: NullaryFuncon
stepPositive_integers = [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
"integers-from" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
1))]) Env
forall k a. Map k a
env

negative_integers_ :: Funcons
negative_integers_ = Name -> Funcons
FName Name
"negative-integers"
neg_ints_ :: Funcons
neg_ints_ = Name -> Funcons
FName Name
"negative-integers"
stepNegative_integers :: NullaryFuncon
stepNegative_integers = [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
"integers-up-to" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat (-Integer
1)))]) Env
forall k a. Map k a
env

natural_numbers_ :: Funcons
natural_numbers_ = Name -> Funcons
FName Name
"natural-numbers"
nats_ :: Funcons
nats_ = Name -> Funcons
FName Name
"natural-numbers"
stepNatural_numbers :: NullaryFuncon
stepNatural_numbers = [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
"integers-from" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
0))]) Env
forall k a. Map k a
env

integer_negate_ :: [Funcons] -> Funcons
integer_negate_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"integer-negate" ([Funcons]
fargs)
int_neg_ :: [Funcons] -> Funcons
int_neg_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"integer-negate" ([Funcons]
fargs)
stepInteger_negate :: StrictFuncon
stepInteger_negate [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
"N") (Name -> FTerm
TName Name
"integers")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"integer-subtract" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
0)),MetaVar -> FTerm
TVar MetaVar
"N"]) Env
env

integer_sequence_ :: [Funcons] -> Funcons
integer_sequence_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"integer-sequence" ([Funcons]
fargs)
stepInteger_sequence :: StrictFuncon
stepInteger_sequence [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1,NullaryFuncon
rewrite2] []
    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
"M") (Name -> FTerm
TName Name
"integers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"integers")] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-greater" [MetaVar -> FTerm
TVar MetaVar
"M",MetaVar -> FTerm
TVar MetaVar
"N"]) (Name -> FTerm
TName Name
"false")) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo ([FTerm] -> FTerm
TSeq [MetaVar -> FTerm
TVar MetaVar
"M",Name -> [FTerm] -> FTerm
TApp Name
"integer-sequence" [Name -> [FTerm] -> FTerm
TApp Name
"integer-add" [MetaVar -> FTerm
TVar MetaVar
"M",Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
1))],MetaVar -> FTerm
TVar MetaVar
"N"]]) 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 [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M") (Name -> FTerm
TName Name
"integers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"integers")] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (Name -> [FTerm] -> FTerm
TApp Name
"is-greater" [MetaVar -> FTerm
TVar MetaVar
"M",MetaVar -> FTerm
TVar MetaVar
"N"]) (Name -> FTerm
TName Name
"true")) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo ([FTerm] -> FTerm
TSeq []) Env
env