{-# LANGUAGE OverloadedStrings #-}
module Funcons.Core.Values.Composite.Sequences.Sequences where
import Funcons.EDSL
import Funcons.Operations hiding (Values)
entities = []
types = typeEnvFromList
[]
funcons = libFromList
[("length",StrictFuncon stepLength),("index",StrictFuncon stepIndex),("first",StrictFuncon stepFirst),("second",StrictFuncon stepSecond),("third",StrictFuncon stepThird),("is-in",StrictFuncon stepIs_in),("first-n",StrictFuncon stepFirst_n),("drop-first-n",StrictFuncon stepDrop_first_n),("reverse",StrictFuncon stepReverse),("n-of",StrictFuncon stepN_of),("intersperse",StrictFuncon stepIntersperse),("filter-defined",StrictFuncon stepFilter_defined)]
length_ fargs = FApp "length" (fargs)
stepLength fargs =
evalRules [rewrite1,rewrite2] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [] env
rewriteTermTo (TFuncon (FValue (Nat 0))) env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TApp "nat-succ" [TApp "length" [TVar "V*"]]) env
index_ fargs = FApp "index" (fargs)
stepIndex fargs =
evalRules [rewrite1,rewrite2,rewrite3,rewrite4] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPLit (Nat 1),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TVar "V") env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
env <- sideCondition (SCPatternMatch (TApp "nat-pred" [TVar "N"]) (VPMetaVar "N'")) env
rewriteTermTo (TApp "index" [TVar "N'",TVar "V*"]) env
rewrite3 = do
let env = emptyEnv
env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TName "none") env
rewrite4 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "P") (TName "pos-ints")] env
rewriteTermTo (TName "none") env
first_ fargs = FApp "first" (fargs)
stepFirst fargs =
evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TVar "V1") env
second_ fargs = FApp "second" (fargs)
stepSecond fargs =
evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "values"),VPAnnotated (VPMetaVar "V2") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TVar "V2") env
third_ fargs = FApp "third" (fargs)
stepThird fargs =
evalRules [rewrite1] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V1") (TName "values"),VPAnnotated (VPMetaVar "V2") (TName "values"),VPAnnotated (VPMetaVar "V3") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TVar "V3") env
is_in_ fargs = FApp "is-in" (fargs)
stepIs_in fargs =
evalRules [rewrite1,rewrite2] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "V'") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TApp "or" [TApp "is-equal" [TVar "V",TVar "V'"],TApp "is-in" [TVar "V",TVar "V*"]]) env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values")] env
rewriteTermTo (TName "false") env
first_n_ fargs = FApp "first-n" (fargs)
stepFirst_n fargs =
evalRules [rewrite1,rewrite2,rewrite3] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TSeq []) env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
env <- sideCondition (SCPatternMatch (TApp "nat-pred" [TVar "N"]) (VPMetaVar "N'")) env
rewriteTermTo (TApp "first-n" [TVar "N'",TVar "V*"]) env
rewrite3 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints")] env
rewriteTermTo (TName "none") env
drop_first_n_ fargs = FApp "drop-first-n" (fargs)
stepDrop_first_n fargs =
evalRules [rewrite1,rewrite2,rewrite3] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPLit (Nat 0),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TVar "V*") env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints"),VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
env <- sideCondition (SCPatternMatch (TApp "nat-pred" [TVar "N"]) (VPMetaVar "N'")) env
rewriteTermTo (TApp "drop-first-n" [TVar "N'",TVar "V*"]) env
rewrite3 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints")] env
rewriteTermTo (TName "none") env
reverse_ fargs = FApp "reverse" (fargs)
stepReverse fargs =
evalRules [rewrite1,rewrite2] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [] env
rewriteTermTo (TSeq []) env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TSeq [TApp "reverse" [TVar "V*"],TVar "V"]) env
n_of_ fargs = FApp "n-of" (fargs)
stepN_of fargs =
evalRules [rewrite1,rewrite2] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPLit (Nat 0),VPMetaVar "V"] env
rewriteTermTo (TSeq []) env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "pos-ints"),VPAnnotated (VPMetaVar "V") (TName "values")] env
env <- sideCondition (SCPatternMatch (TApp "nat-pred" [TVar "N"]) (VPMetaVar "N'")) env
rewriteTermTo (TSeq [TVar "V",TApp "n-of" [TVar "N'",TVar "V"]]) env
intersperse_ fargs = FApp "intersperse" (fargs)
stepIntersperse fargs =
evalRules [rewrite1,rewrite2,rewrite3] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V'") (TName "values")] env
rewriteTermTo (TSeq []) env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V'") (TName "values"),VPMetaVar "V"] env
rewriteTermTo (TVar "V") env
rewrite3 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V'") (TName "values"),VPAnnotated (VPMetaVar "V1") (TName "values"),VPAnnotated (VPMetaVar "V2") (TName "values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TSeq [TVar "V1",TVar "V'",TApp "intersperse" [TVar "V'",TVar "V2",TVar "V*"]]) env
filter_defined_ fargs = FApp "filter-defined" (fargs)
stepFilter_defined fargs =
evalRules [rewrite1,rewrite2,rewrite3] []
where rewrite1 = do
let env = emptyEnv
env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "defined-values"),VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TSeq [TVar "V",TApp "filter-defined" [TVar "V*"]]) env
rewrite2 = do
let env = emptyEnv
env <- vsMatch fargs [PADT "none" [],VPAnnotated (VPSeqVar "V*" StarOp) (TSortSeq (TName "values") StarOp)] env
rewriteTermTo (TApp "filter-defined" [TVar "V*"]) env
rewrite3 = do
let env = emptyEnv
env <- vsMatch fargs [] env
rewriteTermTo (TSeq []) env