{-# LANGUAGE OverloadedStrings #-}
module Funcons.Core.Values.ValueTypes.ValueTypes where
import Funcons.EDSL
import Funcons.Operations hiding (Values)
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_ fargs = FApp "is-in-type" (fargs)
is_ fargs = FApp "is-in-type" (fargs)
stepIs_in_type 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
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
rewriteTermTo (TName "false") env
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 "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 [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "T'") (TName "types")] env
env <- sideCondition (SCIsInSort (TVar "V") (TSortComplement (TVar "T'"))) env
rewriteTermTo (TName "none") env
is_defined_ fargs = FApp "is-defined" (fargs)
is_def_ fargs = FApp "is-defined" (fargs)
stepIs_defined fargs =
evalRules [rewrite1,rewrite2] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "defined-values")] env
rewriteTermTo (TName "true") env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [PADT "none" []] env
rewriteTermTo (TName "false") env
is_equal_ fargs = FApp "is-equal" (fargs)
is_eq_ fargs = FApp "is-equal" (fargs)
stepIs_equal fargs =
evalRules [rewrite1,rewrite2,rewrite3,rewrite4] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "ground-values"),VPAnnotated (VPMetaVar "W") (TName "ground-values")] env
env <- sideCondition (SCEquality (TVar "V") (TVar "W")) env
rewriteTermTo (TName "true") env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "ground-values"),VPAnnotated (VPMetaVar "W") (TName "ground-values")] env
env <- sideCondition (SCInequality (TVar "V") (TVar "W")) env
rewriteTermTo (TName "false") env
rewrite3 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TSortComplement (TName "ground-values")),VPAnnotated (VPMetaVar "W") (TName "values")] env
rewriteTermTo (TName "false") env
rewrite4 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "W") (TSortComplement (TName "ground-values"))] env
rewriteTermTo (TName "false") env