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

module Funcons.Core.Values.ValueTypes.ValueTypes 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
"is-in-type",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_in_type),(Name
"is",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_in_type),(Name
"is-value",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_value),(Name
"is-val",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_value),(Name
"when-true",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepWhen_true),(Name
"when",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepWhen_true),(Name
"cast-to-type",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepCast_to_type),(Name
"cast",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepCast_to_type),(Name
"is-equal",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_equal),(Name
"is-eq",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_equal)]

is_in_type_ :: [Funcons] -> Funcons
is_in_type_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-in-type" ([Funcons]
fargs)
is_ :: [Funcons] -> Funcons
is_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-in-type" ([Funcons]
fargs)
stepIs_in_type :: StrictFuncon
stepIs_in_type [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 = 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
"T") (Name -> FTerm
TName Name
"types")] forall {k} {a}. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"V") (MetaVar -> FTerm
TVar MetaVar
"T")) Env
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> FTerm
TName Name
"true") Env
env
          rewrite2 :: Rewrite Rewritten
rewrite2 = do
            let env :: Map k a
env = 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
"T") (Name -> FTerm
TName Name
"types")] forall {k} {a}. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"V") (FTerm -> FTerm
TSortComplement (MetaVar -> FTerm
TVar MetaVar
"T"))) Env
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env

is_value_ :: [Funcons] -> Funcons
is_value_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-value" ([Funcons]
fargs)
is_val_ :: [Funcons] -> Funcons
is_val_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-value" ([Funcons]
fargs)
stepIs_value :: StrictFuncon
stepIs_value [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 = 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")] forall {k} {a}. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> FTerm
TName Name
"true") Env
env
          rewrite2 :: Rewrite Rewritten
rewrite2 = do
            let env :: Map k a
env = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [] forall {k} {a}. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env

when_true_ :: [Funcons] -> Funcons
when_true_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"when-true" ([Funcons]
fargs)
when_ :: [Funcons] -> Funcons
when_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"when-true" ([Funcons]
fargs)
stepWhen_true :: StrictFuncon
stepWhen_true [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 = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"true" [],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] 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 = forall {k} {a}. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [Name -> [VPattern] -> VPattern
PADT Name
"false" [],VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"V") (Name -> FTerm
TName Name
"values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq []) Env
env

cast_to_type_ :: [Funcons] -> Funcons
cast_to_type_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"cast-to-type" ([Funcons]
fargs)
cast_ :: [Funcons] -> Funcons
cast_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"cast-to-type" ([Funcons]
fargs)
stepCast_to_type :: StrictFuncon
stepCast_to_type [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 = 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
"T") (Name -> FTerm
TName Name
"types")] forall {k} {a}. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"V") (MetaVar -> FTerm
TVar MetaVar
"T")) Env
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (MetaVar -> FTerm
TVar MetaVar
"V") Env
env
          rewrite2 :: Rewrite Rewritten
rewrite2 = do
            let env :: Map k a
env = 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
"T") (Name -> FTerm
TName Name
"types")] forall {k} {a}. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"V") (FTerm -> FTerm
TSortComplement (MetaVar -> FTerm
TVar MetaVar
"T"))) Env
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo ([FTerm] -> FTerm
TSeq []) Env
env

is_equal_ :: [Funcons] -> Funcons
is_equal_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-equal" ([Funcons]
fargs)
is_eq_ :: [Funcons] -> Funcons
is_eq_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-equal" ([Funcons]
fargs)
stepIs_equal :: StrictFuncon
stepIs_equal [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 = 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
"ground-values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"W") (Name -> FTerm
TName Name
"ground-values")] forall {k} {a}. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCEquality (MetaVar -> FTerm
TVar MetaVar
"V") (MetaVar -> FTerm
TVar MetaVar
"W")) Env
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> FTerm
TName Name
"true") Env
env
          rewrite2 :: Rewrite Rewritten
rewrite2 = do
            let env :: Map k a
env = 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
"ground-values"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"W") (Name -> FTerm
TName Name
"ground-values")] forall {k} {a}. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCInequality (MetaVar -> FTerm
TVar MetaVar
"V") (MetaVar -> FTerm
TVar MetaVar
"W")) Env
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env
          rewrite3 :: Rewrite Rewritten
rewrite3 = do
            let env :: Map k a
env = 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") (FTerm -> FTerm
TSortComplement (Name -> FTerm
TName Name
"ground-values")),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"W") (Name -> FTerm
TName Name
"values")] forall {k} {a}. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env
          rewrite4 :: Rewrite Rewritten
rewrite4 = do
            let env :: Map k a
env = 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
"W") (FTerm -> FTerm
TSortComplement (Name -> FTerm
TName Name
"ground-values"))] forall {k} {a}. Map k a
env
            FTerm -> Env -> Rewrite Rewritten
rewriteTermTo (Name -> FTerm
TName Name
"false") Env
env