-- GeNeRaTeD fOr: ../../CBS/Funcons/Abstractions/Patterns/match.aterm
{-# LANGUAGE OverloadedStrings #-}

module Funcons.Core.Abstractions.Patterns.Match where

import Funcons.EDSL

entities = []

types = typeEnvFromList
    []

funcons = libFromList
    [("match",StrictFuncon stepMatch)]

-- |
-- /match(V,P)/ matches the (potentially composite) value /V/ against the
--   (potentially composite) pattern /P/ .
match_ fargs = FApp "match" (FTuple fargs)
stepMatch fargs =
    evalRules [rewrite1,rewrite2,rewrite3,rewrite4,rewrite5,rewrite6,rewrite7,rewrite8,rewrite9,rewrite10] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "P") (TApp "thunks" (TTuple [TSortComputesFrom (TName "values") (TName "environments")]))] env
            rewriteTermTo (TApp "apply" (TTuple [TVar "P",TVar "V"])) env
          rewrite2 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPMetaVar "P"] env
            env <- sideCondition (SCNotInSort (TVar "P") (TApp "thunks" (TTuple [TSortComputesFrom (TName "values") (TName "environments")]))) env
            env <- sideCondition (SCNotInSort (TVar "P") (TName "algebraic-datatypes")) env
            env <- sideCondition (SCNotInSort (TVar "P") (TApp "lists" (TTuple [TName "values"]))) env
            env <- sideCondition (SCNotInSort (TVar "P") (TApp "maps" (TTuple [TName "values",TName "values"]))) env
            env <- sideCondition (SCNotInSort (TVar "P") (TApp "tuples" (TTuple [TName "values",TSortSeq (TName "values") PlusOp]))) env
            env <- sideCondition (SCNotInSort (TVar "P") (TApp "vectors" (TTuple [TName "values"]))) env
            rewriteTermTo (TApp "sequential" (TTuple [TApp "check-true" (TTuple [TApp "is-equal" (TTuple [TVar "V",TVar "P"])]),TName "map-empty"])) env
          rewrite3 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "P") (TName "algebraic-datatypes")] env
            rewriteTermTo (TApp "sequential" (TTuple [TApp "check-true" (TTuple [TApp "is-in-type" (TTuple [TVar "V",TName "algebraic-datatypes"])]),TApp "check-true" (TTuple [TApp "is-equal" (TTuple [TApp "algebraic-datatype-constructor" (TTuple [TVar "V"]),TApp "algebraic-datatype-constructor" (TTuple [TVar "P"])])]),TApp "match" (TTuple [TApp "algebraic-datatype-value" (TTuple [TVar "V"]),TApp "algebraic-datatype-value" (TTuple [TVar "P"])])])) env
          rewrite4 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),PList []] env
            rewriteTermTo (TApp "sequential" (TTuple [TApp "check-true" (TTuple [TApp "is-equal" (TTuple [TVar "V",TList []])]),TName "map-empty"])) env
          rewrite5 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),PList [VPMetaVar "P",VPSeqVar "P*" StarOp]] env
            rewriteTermTo (TApp "sequential" (TTuple [TApp "check-true" (TTuple [TApp "is-in-type" (TTuple [TVar "V",TApp "lists" (TTuple [TName "values"])])]),TApp "check-true" (TTuple [TApp "not" (TTuple [TApp "is-nil" (TTuple [TVar "V"])])]),TApp "map-unite" (TTuple [TApp "match" (TTuple [TApp "head" (TTuple [TVar "V"]),TVar "P"]),TApp "match" (TTuple [TApp "tail" (TTuple [TVar "V"]),TList [TVar "P*"]])])])) env
          rewrite6 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPMetaVar "P"] env
            env <- sideCondition (SCEquality (TVar "P") (TName "map-empty")) env
            rewriteTermTo (TApp "sequential" (TTuple [TApp "check-true" (TTuple [TApp "is-equal" (TTuple [TVar "V",TName "map-empty"])]),TName "map-empty"])) env
          rewrite7 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "VM") (TName "values"),VPAnnotated (VPMetaVar "PM") (TApp "maps" (TTuple [TName "values",TName "values"]))] env
            env <- sideCondition (SCPatternMatch (TApp "some-element" (TTuple [TApp "domain" (TTuple [TVar "PM"])])) (VPMetaVar "K")) env
            rewriteTermTo (TApp "sequential" (TTuple [TApp "check-true" (TTuple [TApp "is-in-type" (TTuple [TVar "VM",TApp "maps" (TTuple [TName "values",TName "values"])])]),TApp "check-true" (TTuple [TApp "is-equal" (TTuple [TApp "domain" (TTuple [TVar "PM"]),TApp "domain" (TTuple [TVar "VM"])])]),TApp "map-unite" (TTuple [TApp "match" (TTuple [TApp "lookup" (TTuple [TVar "K",TVar "VM"]),TApp "lookup" (TTuple [TVar "K",TVar "PM"])]),TApp "match" (TTuple [TApp "map-delete" (TTuple [TVar "VM",TSet [TVar "K"]]),TApp "map-delete" (TTuple [TVar "PM",TSet [TVar "K"]])])])])) env
          rewrite8 = do
            let env = emptyEnv
            env <- vsMatch fargs [PTuple [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPSeqVar "V+" PlusOp) (TName "values")],PTuple [VPAnnotated (VPMetaVar "P") (TName "values"),VPAnnotated (VPSeqVar "P+" PlusOp) (TName "values")]] env
            rewriteTermTo (TApp "map-unite" (TTuple [TApp "match" (TTuple [TVar "V",TVar "P"]),TApp "match" (TTuple [TTuple [TVar "V+"],TTuple [TVar "P+"]])])) env
          rewrite9 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),PTuple [VPAnnotated (VPMetaVar "P") (TName "values"),VPAnnotated (VPSeqVar "P+" PlusOp) (TName "values")]] env
            env <- sideCondition (SCNotInSort (TVar "V") (TApp "tuples" (TTuple [TName "values",TSortSeq (TName "values") PlusOp]))) env
            rewriteTo (FName "fail")
          rewrite10 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "V") (TName "values"),VPAnnotated (VPMetaVar "P") (TApp "vectors" (TTuple [TName "patterns"]))] env
            rewriteTermTo (TApp "sequential" (TTuple [TApp "check-true" (TTuple [TApp "is-in-type" (TTuple [TVar "V",TApp "vectors" (TTuple [TName "values"])])]),TApp "match" (TTuple [TApp "vector-to-list" (TTuple [TVar "V"]),TApp "vector-to-list" (TTuple [TVar "P"])])])) env