{-# LANGUAGE CPP
, DataKinds
, PolyKinds
, GADTs
, TypeOperators
, TypeFamilies
, Rank2Types
, ScopedTypeVariables
, FlexibleInstances
, FlexibleContexts
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Syntax.DatumCase
(
MatchResult(..)
, DatumEvaluator
, matchBranches
, matchBranch
, MatchState(..)
, matchTopPattern
, matchPattern
, viewDatum
) where
import Data.Proxy (Proxy(..))
import Prelude hiding ((<>))
import Language.Hakaru.Syntax.IClasses
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
data MatchResult
(ast :: Hakaru -> *)
(abt :: [Hakaru] -> Hakaru -> *)
(a :: Hakaru)
= GotStuck
| 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
type DatumEvaluator ast m =
forall t
. ast (HData' t)
-> m (Maybe (Datum ast (HData' t)))
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
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
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]
data MatchState
(ast :: Hakaru -> *)
(vars :: [Hakaru])
= GotStuck_
| 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) =
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'
| 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
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
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
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)
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
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