{-# LANGUAGE CPP
           , DataKinds
           , PolyKinds
           , GADTs
           , TypeOperators
           , TypeFamilies
           , Rank2Types
           , ScopedTypeVariables
           , FlexibleInstances
           , FlexibleContexts
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.04.28
-- |
-- Module      :  Language.Hakaru.Syntax.DatumCase
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Reduction of case analysis on user-defined data types.
----------------------------------------------------------------
module Language.Hakaru.Syntax.DatumCase
    (
    -- * External API
      MatchResult(..)
    , DatumEvaluator
    , matchBranches
    , matchBranch

    -- * Internal API
    , MatchState(..)
    , matchTopPattern
    , matchPattern
    , viewDatum
    ) where

import Data.Proxy (Proxy(..))
import Prelude hiding ((<>))

import Language.Hakaru.Syntax.IClasses
-- TODO: make things polykinded so we can make our ABT implementation
-- independend of Hakaru's type system.
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Syntax.Datum
import Language.Hakaru.Syntax.AST (Term(Datum_))
import Language.Hakaru.Syntax.ABT

import qualified Data.Text        as Text
import           Data.Number.Nat  (fromNat)
import           Text.PrettyPrint (Doc, (<+>), (<>))
import qualified Text.PrettyPrint as PP

----------------------------------------------------------------
----------------------------------------------------------------
-- TODO: would it be better to combine the 'Maybe' for failure into
-- the MatchResult itself instead of nesting the types? That'd make
-- the return types for 'matchBranch'\/'matchBranches' a bit trickier;
-- we'd prolly have to turn MatchResult into a monad (namely the
-- @Maybe (Either e (Writer (DList...) (Reader (List1...) a)))@
-- monad, or similar but restricting the Reader to a stream consumer).

-- BUG: haddock doesn't like annotations on GADT constructors. So
-- here we'll avoid using the GADT syntax, even though it'd make
-- the data type declaration prettier\/cleaner.
-- <https://github.com/hakaru-dev/hakaru/issues/6>
data MatchResult
    (ast :: Hakaru -> *)
    (abt :: [Hakaru] -> Hakaru -> *)
    (a   :: Hakaru)

    -- | Our 'DatumEvaluator' failed (perhaps in a nested pattern),
    -- thus preventing us from continuing case-reduction.
    = GotStuck

    -- | We successfully matched everything. The first argument
    -- gives the substitution for all the pattern variables. The
    -- second argument gives the body of the branch matched. N.B.,
    -- the substitution maps variables to some type @ast@ which is
    -- defined by the 'DatumEvaluator' used; it is not necessarily
    -- @abt '[]@! However, the body is definitely @abt '[]@ since
    -- thats what a 'Branch' stores after we account for the
    -- pattern-bound variables.
    --
    -- N.B., because the substitution may not have the right type
    -- (and because we are lazy), we do not perform substitution.
    -- Thus, the body has \"free\" variables which are defined\/bound
    -- in the association list. It's up to callers to perform the
    -- substitution, push the assocs onto the heap, or whatever.
    | Matched !(Assocs ast) !(abt '[] a)


instance (Show1 ast, Show2 abt) => Show1 (MatchResult ast abt) where
    showsPrec1 :: Int -> MatchResult ast abt i -> ShowS
showsPrec1 Int
_ MatchResult ast abt i
GotStuck           = String -> ShowS
showString String
"GotStuck"
    showsPrec1 Int
p (Matched Assocs ast
rho abt '[] i
body) =
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
            ( String -> ShowS
showString String
"Matched "
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Assocs ast -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec  Int
11 Assocs ast
rho
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
            ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> abt '[] i -> ShowS
forall k1 k2 (a :: k1 -> k2 -> *) (i :: k1) (j :: k2).
Show2 a =>
Int -> a i j -> ShowS
showsPrec2 Int
11 abt '[] i
body
            )

instance (Show1 ast, Show2 abt) => Show (MatchResult ast abt a) where
    showsPrec :: Int -> MatchResult ast abt a -> ShowS
showsPrec = Int -> MatchResult ast abt a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1
    show :: MatchResult ast abt a -> String
show      = MatchResult ast abt a -> String
forall k (a :: k -> *) (i :: k). Show1 a => a i -> String
show1


-- | A function for trying to extract a 'Datum' from an arbitrary
-- term. This function is called every time we enter the 'matchPattern'
-- function. If this function returns 'Nothing' then the final
-- 'MatchResult' will be 'GotStuck'; otherwise, this function returns
-- 'Just' some 'Datum' that we can take apart to continue matching.
--
-- We don't care anything about the monad @m@, we just order the
-- effects in a top-down left-to-right manner as we traverse the
-- pattern. However, do note that we may end up calling this evaluator
-- repeatedly on the same argument, so it should be sufficiently
-- idempotent to work under those conditions. In particular,
-- 'matchBranches' will call it once on the top-level scrutinee for
-- each branch. (We should fix that, but it'll require using pattern
-- automata rather than a list of patterns\/branches.)
--
-- TODO: we could change this from returning 'Maybe' to returning
-- 'Either', that way the evaluator could give some reason for its
-- failure (we would store it in the 'GotStuck' constructor).
type DatumEvaluator ast m =
    forall t
    .  ast (HData' t)
    -> m (Maybe (Datum ast (HData' t)))


-- TODO: see the todo for 'matchBranch' about changing the return
-- type. For this function we'd want to return the list of branches
-- including not just the stuck one but all the ones after it too.
-- (Though there's no need to return earlier branches, since we
-- already know they won't match.)
--
-- | Walk through a list of branches and try matching against them
-- in order. We just call 'matchBranches' repeatedly, and return
-- the first non-failure.
matchBranches
    :: (ABT Term abt, Monad m)
    => DatumEvaluator ast m
    -> ast a
    -> [Branch a abt b]
    -> m (Maybe (MatchResult ast abt b))
matchBranches :: DatumEvaluator ast m
-> ast a -> [Branch a abt b] -> m (Maybe (MatchResult ast abt b))
matchBranches DatumEvaluator ast m
getDatum ast a
e = [Branch a abt b] -> m (Maybe (MatchResult ast abt b))
go
    where
    -- TODO: isn't there a combinator in "Control.Monad" for this?
    -- TODO: lift the call to 'getDatum' out here, to avoid duplicating work
    go :: [Branch a abt b] -> m (Maybe (MatchResult ast abt b))
go []     = Maybe (MatchResult ast abt b) -> m (Maybe (MatchResult ast abt b))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (MatchResult ast abt b)
forall a. Maybe a
Nothing
    go (Branch a abt b
b:[Branch a abt b]
bs) = do
        Maybe (MatchResult ast abt b)
match <- DatumEvaluator ast m
-> ast a -> Branch a abt b -> m (Maybe (MatchResult ast abt b))
forall (abt :: [Hakaru] -> Hakaru -> *) (m :: * -> *)
       (ast :: Hakaru -> *) (a :: Hakaru) (b :: Hakaru).
(ABT Term abt, Monad m) =>
DatumEvaluator ast m
-> ast a -> Branch a abt b -> m (Maybe (MatchResult ast abt b))
matchBranch DatumEvaluator ast m
getDatum ast a
e Branch a abt b
b
        case Maybe (MatchResult ast abt b)
match of
            Maybe (MatchResult ast abt b)
Nothing -> [Branch a abt b] -> m (Maybe (MatchResult ast abt b))
go [Branch a abt b]
bs
            Just MatchResult ast abt b
_  -> Maybe (MatchResult ast abt b) -> m (Maybe (MatchResult ast abt b))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (MatchResult ast abt b)
match


-- TODO: change the result type to have values @Nothing@, @Just
-- (GotStuck modifiedScrutinee theStuckBranch)@ and @Just (Matched
-- assocs body)@. That is, give more information about getting
-- stuck, and avoid returning stupid stuff when we get stuck.
--
-- | Try matching against a single branch. This function is a thin
-- wrapper around 'matchTopPattern'; we just take apart the 'Branch'
-- to extract the pattern, list of variables to bind, and the body
-- of the branch.
matchBranch
    :: (ABT Term abt, Monad m)
    => DatumEvaluator ast m
    -> ast a
    -> Branch a abt b
    -> m (Maybe (MatchResult ast abt b))
matchBranch :: DatumEvaluator ast m
-> ast a -> Branch a abt b -> m (Maybe (MatchResult ast abt b))
matchBranch DatumEvaluator ast m
getDatum ast a
e (Branch Pattern xs a
pat abt xs b
body) = do
    let (List1 Variable xs
vars,abt '[] b
body') = abt xs b -> (List1 Variable xs, abt '[] b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> (List1 Variable xs, abt '[] a)
caseBinds abt xs b
body
    Maybe (MatchState ast '[])
match <- DatumEvaluator ast m
-> ast a
-> Pattern xs a
-> List1 Variable xs
-> m (Maybe (MatchState ast '[]))
forall (m :: * -> *) (ast :: Hakaru -> *) (a :: Hakaru)
       (vars :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> ast a
-> Pattern vars a
-> List1 Variable vars
-> m (Maybe (MatchState ast '[]))
matchTopPattern DatumEvaluator ast m
getDatum ast a
e Pattern xs a
pat List1 Variable xs
vars
    Maybe (MatchResult ast abt b) -> m (Maybe (MatchResult ast abt b))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (MatchResult ast abt b)
 -> m (Maybe (MatchResult ast abt b)))
-> Maybe (MatchResult ast abt b)
-> m (Maybe (MatchResult ast abt b))
forall a b. (a -> b) -> a -> b
$
        case Maybe (MatchState ast '[])
match of
        Maybe (MatchState ast '[])
Nothing                  -> Maybe (MatchResult ast abt b)
forall a. Maybe a
Nothing
        Just MatchState ast '[]
GotStuck_           -> MatchResult ast abt b -> Maybe (MatchResult ast abt b)
forall a. a -> Maybe a
Just MatchResult ast abt b
forall (ast :: Hakaru -> *) (abt :: [Hakaru] -> Hakaru -> *)
       (a :: Hakaru).
MatchResult ast abt a
GotStuck
        Just (Matched_ DList (Assoc ast)
rho List1 Variable '[]
Nil1) ->
            MatchResult ast abt b -> Maybe (MatchResult ast abt b)
forall a. a -> Maybe a
Just (Assocs ast -> abt '[] b -> MatchResult ast abt b
forall (ast :: Hakaru -> *) (abt :: [Hakaru] -> Hakaru -> *)
       (a :: Hakaru).
Assocs ast -> abt '[] a -> MatchResult ast abt a
Matched ([Assoc ast] -> Assocs ast
forall k (ast :: k -> *). [Assoc ast] -> Assocs ast
toAssocs ([Assoc ast] -> Assocs ast) -> [Assoc ast] -> Assocs ast
forall a b. (a -> b) -> a -> b
$ DList (Assoc ast)
rho []) abt '[] b
body')


----------------------------------------------------------------
type DList a = [a] -> [a]

-- | The internal version of 'MatchResult' for giving us the properly
-- generalized inductive hypothesis.
data MatchState
    (ast  :: Hakaru -> *)
    (vars :: [Hakaru])

    -- | Our 'DatumEvaluator' failed (perhaps in a nested pattern),
    -- thus preventing us from continuing case-reduction.
    = GotStuck_

    -- TODO: we used to use @DList1 (Pair1 Variable (abt '[]))
    -- vars1@ for the first argument, with @vars1@ another parameter
    -- to the type; this would be helpful internally for guaranteeing
    -- that we return the right number and types of bindings.
    -- However, because the user-facing 'matchBranch' uses 'Branch'
    -- which existentializes over @vars1@, we'd need our user-facing
    -- 'MatchResult' type to also existentialize over @vars1@. Also,
    -- actually keeping track of @vars1@ makes the 'matchStruct'
    -- function much more difficult to get to typecheck. But,
    -- supposing we get that working, would the added guarantees
    -- of this more specific type be helpful for anyone else?
    --
    -- | We successfully matched everything (so far). The first
    -- argument gives the bindings for all the pattern variables
    -- we've already checked. The second argument gives the pattern
    -- variables remaining to be bound by checking the rest of the
    -- pattern.
    | Matched_
        (DList (Assoc ast))
        (List1 Variable vars)


instance Show1 ast => Show (MatchState ast vars) where
    showsPrec :: Int -> MatchState ast vars -> ShowS
showsPrec Int
p = Doc -> ShowS
forall a. Show a => a -> ShowS
shows (Doc -> ShowS)
-> (MatchState ast vars -> Doc) -> MatchState ast vars -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> MatchState ast vars -> Doc
forall (ast :: Hakaru -> *) (vars :: [Hakaru]).
Show1 ast =>
Int -> MatchState ast vars -> Doc
ppMatchState Int
p

ppMatchState :: Show1 ast => Int -> MatchState ast vars -> Doc
ppMatchState :: Int -> MatchState ast vars -> Doc
ppMatchState Int
_ MatchState ast vars
GotStuck_ = String -> Doc
PP.text String
"GotStuck_"
ppMatchState Int
p (Matched_ DList (Assoc ast)
boundVars List1 Variable vars
unboundVars) =
    let f :: String
f = String
"Matched_" in
    Bool -> Doc -> Doc
parens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9)
        (String -> Doc
PP.text String
f Doc -> Doc -> Doc
<+> Int -> Doc -> Doc
PP.nest (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
f) ([Doc] -> Doc
PP.sep
            [ [Doc] -> Doc
ppList ([Doc] -> Doc) -> ([Assoc ast] -> [Doc]) -> [Assoc ast] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Assoc ast -> Doc) -> [Assoc ast] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Assoc ast -> Doc
forall k (ast :: k -> *). Show1 ast => Assoc ast -> Doc
prettyPrecAssoc ([Assoc ast] -> Doc) -> [Assoc ast] -> Doc
forall a b. (a -> b) -> a -> b
$ DList (Assoc ast)
boundVars []
            , [Doc] -> Doc
ppList ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ List1 Variable vars -> [Doc]
forall k (xs :: [k]). List1 Variable xs -> [Doc]
ppVariables List1 Variable vars
unboundVars
            ]))
    where
    ppList :: [Doc] -> Doc
ppList       = Doc -> Doc
PP.brackets (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Doc -> Doc
PP.nest Int
1 (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
PP.fsep ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
PP.punctuate Doc
PP.comma
    parens :: Bool -> Doc -> Doc
parens Bool
True  = Doc -> Doc
PP.parens   (Doc -> Doc) -> (Doc -> Doc) -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Doc -> Doc
PP.nest Int
1
    parens Bool
False = Doc -> Doc
forall a. a -> a
id

    prettyPrecAssoc :: Show1 ast => Assoc ast -> Doc
    prettyPrecAssoc :: Assoc ast -> Doc
prettyPrecAssoc (Assoc Variable a
x ast a
e) =
        -- PP.cat $ ppFun 11 "Assoc" [ppVariable x, ...]
        let f :: String
f = String
"Assoc" in
        [Doc] -> Doc
PP.cat [String -> Doc
PP.text String
f Doc -> Doc -> Doc
<+> Int -> Doc -> Doc
PP.nest (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
f) ([Doc] -> Doc
PP.sep
            [ Variable a -> Doc
forall k (a :: k). Variable a -> Doc
ppVariable Variable a
x
            , String -> Doc
PP.text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> ast a -> ShowS
forall k (a :: k -> *) (i :: k). Show1 a => Int -> a i -> ShowS
showsPrec1 Int
11 ast a
e String
""
            ])]

    ppVariables :: List1 Variable xs -> [Doc]
    ppVariables :: List1 Variable xs -> [Doc]
ppVariables List1 Variable xs
Nil1         = []
    ppVariables (Cons1 Variable x
x List1 Variable xs
xs) = Variable x -> Doc
forall k (a :: k). Variable a -> Doc
ppVariable Variable x
x Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: List1 Variable xs -> [Doc]
forall k (xs :: [k]). List1 Variable xs -> [Doc]
ppVariables List1 Variable xs
xs

    ppVariable :: Variable a -> Doc
    ppVariable :: Variable a -> Doc
ppVariable Variable a
x = Doc
hint Doc -> Doc -> Doc
<> (Int -> Doc
PP.int (Int -> Doc) -> (Variable a -> Int) -> Variable a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Int
fromNat (Nat -> Int) -> (Variable a -> Nat) -> Variable a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID) Variable a
x
        where
        hint :: Doc
hint
            | Text -> Bool
Text.null (Variable a -> Text
forall k (a :: k). Variable a -> Text
varHint Variable a
x) = Char -> Doc
PP.char Char
'x' -- We used to use '_' but...
            | Bool
otherwise             = (String -> Doc
PP.text (String -> Doc) -> (Variable a -> String) -> Variable a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
Text.unpack (Text -> String) -> (Variable a -> Text) -> Variable a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable a -> Text
forall k (a :: k). Variable a -> Text
varHint) Variable a
x


-- | Try matching against a (top-level) pattern. This function is
-- a thin wrapper around 'matchPattern' in order to restrict the
-- type.
matchTopPattern
    :: (Monad m)
    => DatumEvaluator ast m
    -> ast a
    -> Pattern vars a
    -> List1 Variable vars
    -> m (Maybe (MatchState ast '[]))
matchTopPattern :: DatumEvaluator ast m
-> ast a
-> Pattern vars a
-> List1 Variable vars
-> m (Maybe (MatchState ast '[]))
matchTopPattern DatumEvaluator ast m
getDatum ast a
e Pattern vars a
pat List1 Variable vars
vars =
    case Proxy vars -> TypeEq vars (vars ++ '[])
forall k (proxy :: [k] -> *) (xs :: [k]).
proxy xs -> TypeEq xs (xs ++ '[])
eqAppendIdentity (Pattern vars a -> Proxy vars
forall k k (f :: k -> k -> *) (i :: k) (j :: k). f i j -> Proxy i
secondProxy Pattern vars a
pat) of
    TypeEq vars (vars ++ '[])
Refl -> DatumEvaluator ast m
-> ast a
-> Pattern vars a
-> List1 Variable (vars ++ '[])
-> m (Maybe (MatchState ast '[]))
forall (m :: * -> *) (ast :: Hakaru -> *) (a :: Hakaru)
       (vars1 :: [Hakaru]) (vars2 :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> ast a
-> Pattern vars1 a
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchPattern DatumEvaluator ast m
getDatum ast a
e Pattern vars a
pat List1 Variable vars
List1 Variable (vars ++ '[])
vars

secondProxy :: f i j -> Proxy i
secondProxy :: f i j -> Proxy i
secondProxy f i j
_ = Proxy i
forall k (t :: k). Proxy t
Proxy


-- | A trivial \"evaluation function\". If the term is already a
-- 'Datum_', then we extract the 'Datum' value; otherwise we fail.
-- You can 'return' the result to turn this into an 'DatumEvaluator'.
viewDatum
    :: (ABT Term abt)
    => abt '[] (HData' t)
    -> Maybe (Datum (abt '[]) (HData' t))
viewDatum :: abt '[] (HData' t) -> Maybe (Datum (abt '[]) (HData' t))
viewDatum abt '[] (HData' t)
e =
    abt '[] (HData' t)
-> (Variable (HData' t) -> Maybe (Datum (abt '[]) (HData' t)))
-> (Term abt (HData' t) -> Maybe (Datum (abt '[]) (HData' t)))
-> Maybe (Datum (abt '[]) (HData' t))
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] (HData' t)
e (Maybe (Datum (abt '[]) (HData' t))
-> Variable (HData' t) -> Maybe (Datum (abt '[]) (HData' t))
forall a b. a -> b -> a
const Maybe (Datum (abt '[]) (HData' t))
forall a. Maybe a
Nothing) ((Term abt (HData' t) -> Maybe (Datum (abt '[]) (HData' t)))
 -> Maybe (Datum (abt '[]) (HData' t)))
-> (Term abt (HData' t) -> Maybe (Datum (abt '[]) (HData' t)))
-> Maybe (Datum (abt '[]) (HData' t))
forall a b. (a -> b) -> a -> b
$ \Term abt (HData' t)
t ->
        case Term abt (HData' t)
t of
        Datum_ Datum (abt '[]) (HData' t)
d -> Datum (abt '[]) (HData' t) -> Maybe (Datum (abt '[]) (HData' t))
forall a. a -> Maybe a
Just Datum (abt '[]) (HData' t)
Datum (abt '[]) (HData' t)
d
        Term abt (HData' t)
_        -> Maybe (Datum (abt '[]) (HData' t))
forall a. Maybe a
Nothing


-- | Try matching against a (potentially nested) pattern. This
-- function generalizes 'matchTopPattern', which is necessary for
-- being able to handle nested patterns correctly. You probably
-- don't ever need to call this function.
matchPattern
    :: (Monad m)
    => DatumEvaluator ast m
    -> ast a
    -> Pattern vars1 a
    -> List1 Variable (vars1 ++ vars2)
    -> m (Maybe (MatchState ast vars2))
matchPattern :: DatumEvaluator ast m
-> ast a
-> Pattern vars1 a
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchPattern DatumEvaluator ast m
getDatum ast a
e Pattern vars1 a
pat List1 Variable (vars1 ++ vars2)
vars =
    case Pattern vars1 a
pat of
    Pattern vars1 a
PWild              -> Maybe (MatchState ast vars2) -> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (MatchState ast vars2) -> m (Maybe (MatchState ast vars2)))
-> (MatchState ast vars2 -> Maybe (MatchState ast vars2))
-> MatchState ast vars2
-> m (Maybe (MatchState ast vars2))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MatchState ast vars2 -> Maybe (MatchState ast vars2)
forall a. a -> Maybe a
Just (MatchState ast vars2 -> m (Maybe (MatchState ast vars2)))
-> MatchState ast vars2 -> m (Maybe (MatchState ast vars2))
forall a b. (a -> b) -> a -> b
$ DList (Assoc ast) -> List1 Variable vars2 -> MatchState ast vars2
forall (ast :: Hakaru -> *) (vars :: [Hakaru]).
DList (Assoc ast) -> List1 Variable vars -> MatchState ast vars
Matched_ DList (Assoc ast)
forall a. a -> a
id List1 Variable vars2
List1 Variable (vars1 ++ vars2)
vars
    Pattern vars1 a
PVar               ->
        case List1 Variable (vars1 ++ vars2)
vars of
        Cons1 Variable x
x List1 Variable xs
vars'  -> Maybe (MatchState ast xs) -> m (Maybe (MatchState ast xs))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (MatchState ast xs) -> m (Maybe (MatchState ast xs)))
-> (MatchState ast xs -> Maybe (MatchState ast xs))
-> MatchState ast xs
-> m (Maybe (MatchState ast xs))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MatchState ast xs -> Maybe (MatchState ast xs)
forall a. a -> Maybe a
Just (MatchState ast xs -> m (Maybe (MatchState ast xs)))
-> MatchState ast xs -> m (Maybe (MatchState ast xs))
forall a b. (a -> b) -> a -> b
$ DList (Assoc ast) -> List1 Variable xs -> MatchState ast xs
forall (ast :: Hakaru -> *) (vars :: [Hakaru]).
DList (Assoc ast) -> List1 Variable vars -> MatchState ast vars
Matched_ (Variable x -> ast x -> Assoc ast
forall k (ast :: k -> *) (a :: k). Variable a -> ast a -> Assoc ast
Assoc Variable x
x ast a
ast x
e Assoc ast -> DList (Assoc ast)
forall a. a -> [a] -> [a]
:) List1 Variable xs
vars'
    PDatum Text
_hint1 PDatumCode (Code t) vars1 (HData' t)
pat1 -> do
        Maybe (Datum ast (HData' t))
mb <- ast (HData' t) -> m (Maybe (Datum ast (HData' t)))
DatumEvaluator ast m
getDatum ast a
ast (HData' t)
e
        case Maybe (Datum ast (HData' t))
mb of
            Maybe (Datum ast (HData' t))
Nothing                     -> Maybe (MatchState ast vars2) -> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (MatchState ast vars2) -> m (Maybe (MatchState ast vars2)))
-> Maybe (MatchState ast vars2) -> m (Maybe (MatchState ast vars2))
forall a b. (a -> b) -> a -> b
$ MatchState ast vars2 -> Maybe (MatchState ast vars2)
forall a. a -> Maybe a
Just MatchState ast vars2
forall (ast :: Hakaru -> *) (vars :: [Hakaru]). MatchState ast vars
GotStuck_
            Just (Datum Text
_hint2 Sing (HData' t)
_typ2 DatumCode (Code t) ast (HData' t)
d) -> DatumEvaluator ast m
-> DatumCode (Code t) ast (HData' t)
-> PDatumCode (Code t) vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) (ast :: Hakaru -> *) (xss :: [[HakaruFun]])
       (t :: HakaruCon) (vars1 :: [Hakaru]) (vars2 :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> DatumCode xss ast (HData' t)
-> PDatumCode xss vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchCode DatumEvaluator ast m
getDatum DatumCode (Code t) ast (HData' t)
DatumCode (Code t) ast (HData' t)
d PDatumCode (Code t) vars1 (HData' t)
PDatumCode (Code t) vars1 (HData' t)
pat1 List1 Variable (vars1 ++ vars2)
vars


matchCode
    :: (Monad m)
    => DatumEvaluator ast m
    -> DatumCode  xss ast   (HData' t)
    -> PDatumCode xss vars1 (HData' t)
    -> List1 Variable (vars1 ++ vars2)
    -> m (Maybe (MatchState ast vars2))
matchCode :: DatumEvaluator ast m
-> DatumCode xss ast (HData' t)
-> PDatumCode xss vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchCode DatumEvaluator ast m
getDatum DatumCode xss ast (HData' t)
d PDatumCode xss vars1 (HData' t)
pat List1 Variable (vars1 ++ vars2)
vars =
    case (DatumCode xss ast (HData' t)
d,PDatumCode xss vars1 (HData' t)
pat) of
    (Inr DatumCode xss ast (HData' t)
d2, PInr pat2) -> DatumEvaluator ast m
-> DatumCode xss ast (HData' t)
-> PDatumCode xss vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) (ast :: Hakaru -> *) (xss :: [[HakaruFun]])
       (t :: HakaruCon) (vars1 :: [Hakaru]) (vars2 :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> DatumCode xss ast (HData' t)
-> PDatumCode xss vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchCode   DatumEvaluator ast m
getDatum DatumCode xss ast (HData' t)
d2 PDatumCode xss vars1 (HData' t)
PDatumCode xss vars1 (HData' t)
pat2 List1 Variable (vars1 ++ vars2)
vars
    (Inl DatumStruct xs ast (HData' t)
d1, PInl pat1) -> DatumEvaluator ast m
-> DatumStruct xs ast (HData' t)
-> PDatumStruct xs vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) (ast :: Hakaru -> *) (xs :: [HakaruFun])
       (t :: HakaruCon) (vars1 :: [Hakaru]) (vars2 :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> DatumStruct xs ast (HData' t)
-> PDatumStruct xs vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchStruct DatumEvaluator ast m
getDatum DatumStruct xs ast (HData' t)
d1 PDatumStruct xs vars1 (HData' t)
PDatumStruct xs vars1 (HData' t)
pat1 List1 Variable (vars1 ++ vars2)
vars
    (DatumCode xss ast (HData' t), PDatumCode xss vars1 (HData' t))
_                   -> Maybe (MatchState ast vars2) -> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (MatchState ast vars2)
forall a. Maybe a
Nothing


matchStruct
    :: forall m ast xs t vars1 vars2
    .  (Monad m)
    => DatumEvaluator ast m
    -> DatumStruct  xs ast   (HData' t)
    -> PDatumStruct xs vars1 (HData' t)
    -> List1 Variable (vars1 ++ vars2)
    -> m (Maybe (MatchState ast vars2))
matchStruct :: DatumEvaluator ast m
-> DatumStruct xs ast (HData' t)
-> PDatumStruct xs vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchStruct DatumEvaluator ast m
getDatum DatumStruct xs ast (HData' t)
d PDatumStruct xs vars1 (HData' t)
pat List1 Variable (vars1 ++ vars2)
vars =
    case (DatumStruct xs ast (HData' t)
d,PDatumStruct xs vars1 (HData' t)
pat) of
    (DatumStruct xs ast (HData' t)
Done,     PDatumStruct xs vars1 (HData' t)
PDone)     -> Maybe (MatchState ast vars2) -> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (MatchState ast vars2) -> m (Maybe (MatchState ast vars2)))
-> (MatchState ast vars2 -> Maybe (MatchState ast vars2))
-> MatchState ast vars2
-> m (Maybe (MatchState ast vars2))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MatchState ast vars2 -> Maybe (MatchState ast vars2)
forall a. a -> Maybe a
Just (MatchState ast vars2 -> m (Maybe (MatchState ast vars2)))
-> MatchState ast vars2 -> m (Maybe (MatchState ast vars2))
forall a b. (a -> b) -> a -> b
$ DList (Assoc ast) -> List1 Variable vars2 -> MatchState ast vars2
forall (ast :: Hakaru -> *) (vars :: [Hakaru]).
DList (Assoc ast) -> List1 Variable vars -> MatchState ast vars
Matched_ DList (Assoc ast)
forall a. a -> a
id List1 Variable vars2
List1 Variable (vars1 ++ vars2)
vars
    (Et DatumFun x ast (HData' t)
d1 DatumStruct xs ast (HData' t)
d2, PEt p1 p2) ->
        let vars0 :: List1 Variable (vars1 ++ (vars2 ++ vars2))
vars0 =
                case
                    Proxy vars1
-> Proxy vars2
-> Proxy vars2
-> TypeEq ((vars1 ++ vars2) ++ vars2) (vars1 ++ (vars2 ++ vars2))
forall k (proxy1 :: [k] -> *) (xs :: [k]) (proxy2 :: [k] -> *)
       (ys :: [k]) (proxy3 :: [k] -> *) (zs :: [k]).
proxy1 xs
-> proxy2 ys
-> proxy3 zs
-> TypeEq ((xs ++ ys) ++ zs) (xs ++ (ys ++ zs))
eqAppendAssoc
                        (PDatumFun x vars1 (HData' t) -> Proxy vars1
forall k k (f :: k -> k -> *) (i :: k) (j :: k). f i j -> Proxy i
secondProxy PDatumFun x vars1 (HData' t)
p1)
                        (PDatumStruct xs vars2 (HData' t) -> Proxy vars2
forall k k (f :: k -> k -> *) (i :: k) (j :: k). f i j -> Proxy i
secondProxy PDatumStruct xs vars2 (HData' t)
p2)
                        (Proxy vars2
forall k (t :: k). Proxy t
Proxy :: Proxy vars2) -- HACK: is there any other way to get our hands on @vars2@?
                of TypeEq ((vars1 ++ vars2) ++ vars2) (vars1 ++ (vars2 ++ vars2))
Refl -> List1 Variable (vars1 ++ vars2)
List1 Variable (vars1 ++ (vars2 ++ vars2))
vars
        in
        DatumEvaluator ast m
-> DatumFun x ast (HData' t)
-> PDatumFun x vars1 (HData' t)
-> List1 Variable (vars1 ++ (vars2 ++ vars2))
-> m (Maybe (MatchState ast (vars2 ++ vars2)))
forall (m :: * -> *) (ast :: Hakaru -> *) (x :: HakaruFun)
       (t :: HakaruCon) (vars1 :: [Hakaru]) (vars2 :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> DatumFun x ast (HData' t)
-> PDatumFun x vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchFun    DatumEvaluator ast m
getDatum DatumFun x ast (HData' t)
d1 PDatumFun x vars1 (HData' t)
PDatumFun x vars1 (HData' t)
p1 List1 Variable (vars1 ++ (vars2 ++ vars2))
vars0 m (Maybe (MatchState ast (vars2 ++ vars2)))
-> (DList (Assoc ast)
    -> List1 Variable (vars2 ++ vars2)
    -> m (Maybe (MatchState ast vars2)))
-> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) (ast :: Hakaru -> *) (vars :: [Hakaru])
       (ast :: Hakaru -> *) (vars :: [Hakaru]).
Monad m =>
m (Maybe (MatchState ast vars))
-> (DList (Assoc ast)
    -> List1 Variable vars -> m (Maybe (MatchState ast vars)))
-> m (Maybe (MatchState ast vars))
`bindMMR` \DList (Assoc ast)
xs1 List1 Variable (vars2 ++ vars2)
vars1 ->
        DatumEvaluator ast m
-> DatumStruct xs ast (HData' t)
-> PDatumStruct xs vars2 (HData' t)
-> List1 Variable (vars2 ++ vars2)
-> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) (ast :: Hakaru -> *) (xs :: [HakaruFun])
       (t :: HakaruCon) (vars1 :: [Hakaru]) (vars2 :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> DatumStruct xs ast (HData' t)
-> PDatumStruct xs vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchStruct DatumEvaluator ast m
getDatum DatumStruct xs ast (HData' t)
d2 PDatumStruct xs vars2 (HData' t)
PDatumStruct xs vars2 (HData' t)
p2 List1 Variable (vars2 ++ vars2)
vars1 m (Maybe (MatchState ast vars2))
-> (DList (Assoc ast)
    -> List1 Variable vars2 -> m (Maybe (MatchState ast vars2)))
-> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) (ast :: Hakaru -> *) (vars :: [Hakaru])
       (ast :: Hakaru -> *) (vars :: [Hakaru]).
Monad m =>
m (Maybe (MatchState ast vars))
-> (DList (Assoc ast)
    -> List1 Variable vars -> m (Maybe (MatchState ast vars)))
-> m (Maybe (MatchState ast vars))
`bindMMR` \DList (Assoc ast)
xs2 List1 Variable vars2
vars2 ->
        Maybe (MatchState ast vars2) -> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (MatchState ast vars2) -> m (Maybe (MatchState ast vars2)))
-> (MatchState ast vars2 -> Maybe (MatchState ast vars2))
-> MatchState ast vars2
-> m (Maybe (MatchState ast vars2))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MatchState ast vars2 -> Maybe (MatchState ast vars2)
forall a. a -> Maybe a
Just (MatchState ast vars2 -> m (Maybe (MatchState ast vars2)))
-> MatchState ast vars2 -> m (Maybe (MatchState ast vars2))
forall a b. (a -> b) -> a -> b
$ DList (Assoc ast) -> List1 Variable vars2 -> MatchState ast vars2
forall (ast :: Hakaru -> *) (vars :: [Hakaru]).
DList (Assoc ast) -> List1 Variable vars -> MatchState ast vars
Matched_ (DList (Assoc ast)
xs1 DList (Assoc ast) -> DList (Assoc ast) -> DList (Assoc ast)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DList (Assoc ast)
xs2) List1 Variable vars2
vars2
    where
    -- TODO: just turn @Maybe MatchState@ into a monad already?
    bindMMR :: m (Maybe (MatchState ast vars))
-> (DList (Assoc ast)
    -> List1 Variable vars -> m (Maybe (MatchState ast vars)))
-> m (Maybe (MatchState ast vars))
bindMMR m (Maybe (MatchState ast vars))
m DList (Assoc ast)
-> List1 Variable vars -> m (Maybe (MatchState ast vars))
k = do
        Maybe (MatchState ast vars)
mb <- m (Maybe (MatchState ast vars))
m
        case Maybe (MatchState ast vars)
mb of
            Maybe (MatchState ast vars)
Nothing                  -> Maybe (MatchState ast vars) -> m (Maybe (MatchState ast vars))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (MatchState ast vars)
forall a. Maybe a
Nothing
            Just MatchState ast vars
GotStuck_           -> Maybe (MatchState ast vars) -> m (Maybe (MatchState ast vars))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (MatchState ast vars) -> m (Maybe (MatchState ast vars)))
-> Maybe (MatchState ast vars) -> m (Maybe (MatchState ast vars))
forall a b. (a -> b) -> a -> b
$ MatchState ast vars -> Maybe (MatchState ast vars)
forall a. a -> Maybe a
Just MatchState ast vars
forall (ast :: Hakaru -> *) (vars :: [Hakaru]). MatchState ast vars
GotStuck_
            Just (Matched_ DList (Assoc ast)
xs List1 Variable vars
vars') -> DList (Assoc ast)
-> List1 Variable vars -> m (Maybe (MatchState ast vars))
k DList (Assoc ast)
xs List1 Variable vars
vars'

matchFun
    :: (Monad m)
    => DatumEvaluator ast m
    -> DatumFun  x ast   (HData' t)
    -> PDatumFun x vars1 (HData' t)
    -> List1 Variable (vars1 ++ vars2)
    -> m (Maybe (MatchState ast vars2))
matchFun :: DatumEvaluator ast m
-> DatumFun x ast (HData' t)
-> PDatumFun x vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchFun DatumEvaluator ast m
getDatum DatumFun x ast (HData' t)
d PDatumFun x vars1 (HData' t)
pat List1 Variable (vars1 ++ vars2)
vars =
    case (DatumFun x ast (HData' t)
d,PDatumFun x vars1 (HData' t)
pat) of
    (Konst ast b
d2, PKonst p2) -> DatumEvaluator ast m
-> ast b
-> Pattern vars1 b
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) (ast :: Hakaru -> *) (a :: Hakaru)
       (vars1 :: [Hakaru]) (vars2 :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> ast a
-> Pattern vars1 a
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchPattern DatumEvaluator ast m
getDatum ast b
d2 Pattern vars1 b
Pattern vars1 b
p2 List1 Variable (vars1 ++ vars2)
vars
    (Ident ast (HData' t)
d1, PIdent p1) -> DatumEvaluator ast m
-> ast (HData' t)
-> Pattern vars1 (HData' t)
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
forall (m :: * -> *) (ast :: Hakaru -> *) (a :: Hakaru)
       (vars1 :: [Hakaru]) (vars2 :: [Hakaru]).
Monad m =>
DatumEvaluator ast m
-> ast a
-> Pattern vars1 a
-> List1 Variable (vars1 ++ vars2)
-> m (Maybe (MatchState ast vars2))
matchPattern DatumEvaluator ast m
getDatum ast (HData' t)
d1 Pattern vars1 (HData' t)
p1 List1 Variable (vars1 ++ vars2)
vars

----------------------------------------------------------------
----------------------------------------------------------- fin.