module Prelude.Type.Match where
import Prelude.Type.Families
import Prelude.Type.Integer
class Match (a :: k) (b :: k) (p :: Bool) | a b -> p
instance (a ~ b, p ~ True) => Match a b p
instance a ~ b => Match (a :: ()) b True
instance Match Nothing (Just a) False
instance (nothing ~ Nothing, true ~ true) => Match Nothing nothing true
instance false ~ False => Match (Just a) Nothing false
instance (just_b ~ Just b, Match a b p) => Match (Just a) just_b p
instance Match True False False
instance (true ~ True, match ~ True) => Match True true match
instance Match False True False
instance (false ~ False, match ~ True) => Match False false match
instance Match LT EQ False
instance Match LT GT False
instance (lt ~ LT, match ~ True) => Match LT lt match
instance Match EQ LT False
instance Match EQ GT False
instance (eq ~ EQ, match ~ True) => Match EQ eq match
instance Match GT EQ False
instance Match GT LT False
instance (gt ~ GT, match ~ True) => Match GT gt match
instance Match (Left a) (Right b) False
instance Match (Right a) (Left b) False
instance (left_b ~ Left b, Match a b p) => Match (Left a) left_b p
instance (right_b ~ Right b, Match a b p) => Match (Right a) right_b p
instance (e_f ~ '(e, f), Match a e p, Match b f q, r ~ (p && q)) => Match '(a, b) e_f r
instance (e_f_g ~ '(e, f, g), Match a e p, Match b f q, Match c g r, (p && q) ~ s, (r && s) ~ t) => Match '(a, b, c) e_f_g t
instance (e_f_g_h ~ '(e, f, g, h), Match a e p, Match b f q, Match c g r, Match d h s, (p && q) ~ t, (r && s) ~ u, (t && u) ~ v)
=> Match '(a, b, c, d) e_f_g_h v
instance Match '[] (x ': xs) False
instance Match (x ': xs) '[] False
instance (nil ~ '[], true ~ True) => Match '[] nil true
instance (cons ~ (y ': ys),
Match x y m,
If m
(Match xs ys p)
(p ~ False))
=> Match (x ': xs) cons p
instance Match Ones (One j) False
instance Match Ones (Zero j) False
instance Match Ones Zeros False
instance Match Zeros Ones False
instance Match Zeros (One j) False
instance Match Zeros (Zero j) False
instance Match (One i) Ones False
instance Match (One i) Zeros False
instance Match (One i) (Zero j) False
instance Match (Zero i) Ones False
instance Match (Zero i) (One i) False
instance Match (Zero i) Zeros False
instance (ones ~ Ones, true ~ True) => Match Ones ones true
instance (zeros ~ Zeros, true ~ True) => Match Zeros zeros true
instance (one_j ~ (One j), Match i j p) => Match (One i) one_j p
instance (zero_j ~ (Zero j), Match i j p) => Match (Zero i) zero_j p