{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Kanren.Example.Matche (example, eithero') where

import Control.Lens (Prism, from)
import Control.Lens.TH
import Data.Bifunctor (bimap)
import Data.Function ((&))
import Data.Tagged (Tagged)
import GHC.Generics (Generic)

import Kanren.Core
import Kanren.Goal
import Kanren.LogicalBase
import Kanren.Match
import Kanren.TH

eithero :: (Logical a, Logical b) => Term (Either a b) -> Goal ()
eithero :: forall a b. (Logical a, Logical b) => Term (Either a b) -> Goal ()
eithero =
  Term (Either a b) -> Goal ()
forall a x. Term a -> Goal x
matche
    (Term (Either a b) -> Goal ())
-> ((Term (Either a b) -> Goal ()) -> Term (Either a b) -> Goal ())
-> Term (Either a b)
-> Goal ()
forall a b. a -> (a -> b) -> b
& Prism' (Logic (Either a b)) (Term a)
-> (Term a -> Goal ())
-> (Term (Either a b) -> Goal ())
-> Term (Either a b)
-> Goal ()
forall a v x.
(Logical a, Fresh v) =>
Prism' (Logic a) v
-> (v -> Goal x) -> (Term a -> Goal x) -> Term a -> Goal x
on p (Term a) (f (Term a))
-> p (Logic (Either a b)) (f (Logic (Either a b)))
p (Term a) (f (Term a))
-> p (LogicEither a b) (f (LogicEither a b))
forall a1 b a2 (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Term a1) (f (Term a2))
-> p (LogicEither a1 b) (f (LogicEither a2 b))
Prism' (Logic (Either a b)) (Term a)
_LogicLeft (\Term a
_ -> () -> Goal ()
forall a. a -> Goal a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    (Term (Either a b) -> Goal ())
-> ((Term (Either a b) -> Goal ()) -> Term (Either a b) -> Goal ())
-> Term (Either a b)
-> Goal ()
forall a b. a -> (a -> b) -> b
& Prism' (Logic (Either a b)) (Term b)
-> (Term b -> Goal ())
-> (Term (Either a b) -> Goal ())
-> Term (Either a b)
-> Goal ()
forall a v x.
(Logical a, Fresh v) =>
Prism' (Logic a) v
-> (v -> Goal x) -> (Term a -> Goal x) -> Term a -> Goal x
on p (Term b) (f (Term b))
-> p (Logic (Either a b)) (f (Logic (Either a b)))
p (Term b) (f (Term b))
-> p (LogicEither a b) (f (LogicEither a b))
forall a b1 b2 (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Term b1) (f (Term b2))
-> p (LogicEither a b1) (f (LogicEither a b2))
Prism' (Logic (Either a b)) (Term b)
_LogicRight (\Term b
_ -> () -> Goal ()
forall a. a -> Goal a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

nestedo :: Term (Either (Either Int Bool) Int) -> Goal ()
nestedo :: Term (Either (Either Int Bool) Int) -> Goal ()
nestedo =
  Term (Either (Either Int Bool) Int) -> Goal ()
forall a x. Term a -> Goal x
matche
    (Term (Either (Either Int Bool) Int) -> Goal ())
-> ((Term (Either (Either Int Bool) Int) -> Goal ())
    -> Term (Either (Either Int Bool) Int) -> Goal ())
-> Term (Either (Either Int Bool) Int)
-> Goal ()
forall a b. a -> (a -> b) -> b
& Prism' (Logic (Either (Either Int Bool) Int)) (Term Int)
-> (Term Int -> Goal ())
-> (Term (Either (Either Int Bool) Int) -> Goal ())
-> Term (Either (Either Int Bool) Int)
-> Goal ()
forall a v x.
(Logical a, Fresh v) =>
Prism' (Logic a) v
-> (v -> Goal x) -> (Term a -> Goal x) -> Term a -> Goal x
on (p (Term (Either Int Bool)) (f (Term (Either Int Bool)))
-> p (LogicEither (Either Int Bool) Int)
     (f (LogicEither (Either Int Bool) Int))
forall a1 b a2 (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Term a1) (f (Term a2))
-> p (LogicEither a1 b) (f (LogicEither a2 b))
_LogicLeft (p (Term (Either Int Bool)) (f (Term (Either Int Bool)))
 -> p (LogicEither (Either Int Bool) Int)
      (f (LogicEither (Either Int Bool) Int)))
-> (p (Term Int) (f (Term Int))
    -> p (Term (Either Int Bool)) (f (Term (Either Int Bool))))
-> p (Term Int) (f (Term Int))
-> p (LogicEither (Either Int Bool) Int)
     (f (LogicEither (Either Int Bool) Int))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Logic (Either Int Bool)) (f (Logic (Either Int Bool)))
-> p (Term (Either Int Bool)) (f (Term (Either Int Bool)))
p (LogicEither Int Bool) (f (LogicEither Int Bool))
-> p (Term (Either Int Bool)) (f (Term (Either Int Bool)))
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Logic a) (f (Logic a)) -> p (Term a) (f (Term a))
_Value (p (LogicEither Int Bool) (f (LogicEither Int Bool))
 -> p (Term (Either Int Bool)) (f (Term (Either Int Bool))))
-> (p (Term Int) (f (Term Int))
    -> p (LogicEither Int Bool) (f (LogicEither Int Bool)))
-> p (Term Int) (f (Term Int))
-> p (Term (Either Int Bool)) (f (Term (Either Int Bool)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Term Int) (f (Term Int))
-> p (LogicEither Int Bool) (f (LogicEither Int Bool))
forall a1 b a2 (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Term a1) (f (Term a2))
-> p (LogicEither a1 b) (f (LogicEither a2 b))
_LogicLeft) (Term Int -> Term Int -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term Int
42)
    (Term (Either (Either Int Bool) Int) -> Goal ())
-> ((Term (Either (Either Int Bool) Int) -> Goal ())
    -> Term (Either (Either Int Bool) Int) -> Goal ())
-> Term (Either (Either Int Bool) Int)
-> Goal ()
forall a b. a -> (a -> b) -> b
& Prism' (Logic (Either (Either Int Bool) Int)) (Term Bool)
-> (Term Bool -> Goal ())
-> (Term (Either (Either Int Bool) Int) -> Goal ())
-> Term (Either (Either Int Bool) Int)
-> Goal ()
forall a v x.
(Logical a, Fresh v) =>
Prism' (Logic a) v
-> (v -> Goal x) -> (Term a -> Goal x) -> Term a -> Goal x
on (p (Term (Either Int Bool)) (f (Term (Either Int Bool)))
-> p (LogicEither (Either Int Bool) Int)
     (f (LogicEither (Either Int Bool) Int))
forall a1 b a2 (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Term a1) (f (Term a2))
-> p (LogicEither a1 b) (f (LogicEither a2 b))
_LogicLeft (p (Term (Either Int Bool)) (f (Term (Either Int Bool)))
 -> p (LogicEither (Either Int Bool) Int)
      (f (LogicEither (Either Int Bool) Int)))
-> (p (Term Bool) (f (Term Bool))
    -> p (Term (Either Int Bool)) (f (Term (Either Int Bool))))
-> p (Term Bool) (f (Term Bool))
-> p (LogicEither (Either Int Bool) Int)
     (f (LogicEither (Either Int Bool) Int))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Logic (Either Int Bool)) (f (Logic (Either Int Bool)))
-> p (Term (Either Int Bool)) (f (Term (Either Int Bool)))
p (LogicEither Int Bool) (f (LogicEither Int Bool))
-> p (Term (Either Int Bool)) (f (Term (Either Int Bool)))
forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Logic a) (f (Logic a)) -> p (Term a) (f (Term a))
_Value (p (LogicEither Int Bool) (f (LogicEither Int Bool))
 -> p (Term (Either Int Bool)) (f (Term (Either Int Bool))))
-> (p (Term Bool) (f (Term Bool))
    -> p (LogicEither Int Bool) (f (LogicEither Int Bool)))
-> p (Term Bool) (f (Term Bool))
-> p (Term (Either Int Bool)) (f (Term (Either Int Bool)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Term Bool) (f (Term Bool))
-> p (LogicEither Int Bool) (f (LogicEither Int Bool))
forall a b1 b2 (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Term b1) (f (Term b2))
-> p (LogicEither a b1) (f (LogicEither a b2))
_LogicRight) (Term Bool -> Term Bool -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bool -> Term Bool
forall a. Logic a -> Term a
Value Bool
Logic Bool
True)
    (Term (Either (Either Int Bool) Int) -> Goal ())
-> ((Term (Either (Either Int Bool) Int) -> Goal ())
    -> Term (Either (Either Int Bool) Int) -> Goal ())
-> Term (Either (Either Int Bool) Int)
-> Goal ()
forall a b. a -> (a -> b) -> b
& Prism' (Logic (Either (Either Int Bool) Int)) (Term Int)
-> (Term Int -> Goal ())
-> (Term (Either (Either Int Bool) Int) -> Goal ())
-> Term (Either (Either Int Bool) Int)
-> Goal ()
forall a v x.
(Logical a, Fresh v) =>
Prism' (Logic a) v
-> (v -> Goal x) -> (Term a -> Goal x) -> Term a -> Goal x
on p (Term Int) (f (Term Int))
-> p (Logic (Either (Either Int Bool) Int))
     (f (Logic (Either (Either Int Bool) Int)))
p (Term Int) (f (Term Int))
-> p (LogicEither (Either Int Bool) Int)
     (f (LogicEither (Either Int Bool) Int))
forall a b1 b2 (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Term b1) (f (Term b2))
-> p (LogicEither a b1) (f (LogicEither a b2))
Prism' (Logic (Either (Either Int Bool) Int)) (Term Int)
_LogicRight (Term Int -> Term Int -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term Int
1729)

-- Exhaustive pattern-matching

eithero' :: (Logical a, Logical b) => Term (Either a b) -> Goal ()
eithero' :: forall a b. (Logical a, Logical b) => Term (Either a b) -> Goal ()
eithero' =
  Matched (Checked, Checked) (Either a b) -> Goal ()
forall m a x. Exhausted m => Matched m a -> Goal x
matche'
    (Matched (Checked, Checked) (Either a b) -> Goal ())
-> ((Matched (Checked, Checked) (Either a b) -> Goal ())
    -> Matched (Remaining, Checked) (Either a b) -> Goal ())
-> Matched (Remaining, Checked) (Either a b)
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic (Either a b))
  (Remaining, Checked)
  (Checked, Checked)
  (Term a)
  Remaining
  Checked
-> (Term a -> Goal ())
-> (Matched (Checked, Checked) (Either a b) -> Goal ())
-> Matched (Remaining, Checked) (Either a b)
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' p (Tagged Remaining (Term a)) (f (Tagged Checked (Term a)))
-> p (Tagged (Remaining, Checked) (Logic (Either a b)))
     (f (Tagged (Checked, Checked) (Logic (Either a b))))
p (Tagged Remaining (Term a)) (f (Tagged Checked (Term a)))
-> p (Tagged (Remaining, Checked) (LogicEither a b))
     (f (Tagged (Checked, Checked) (LogicEither a b)))
forall a b logicLeft logicRight logicLeft' (p :: * -> * -> *)
       (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged logicLeft (Term a)) (f (Tagged logicLeft' (Term a)))
-> p (Tagged (logicLeft, logicRight) (LogicEither a b))
     (f (Tagged (logicLeft', logicRight) (LogicEither a b)))
ExhaustivePrism
  (Logic (Either a b))
  (Remaining, Checked)
  (Checked, Checked)
  (Term a)
  Remaining
  Checked
_LogicLeft' (\Term a
_ -> () -> Goal ()
forall a. a -> Goal a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    (Matched (Remaining, Checked) (Either a b) -> Goal ())
-> ((Matched (Remaining, Checked) (Either a b) -> Goal ())
    -> Matched (Remaining, Remaining) (Either a b) -> Goal ())
-> Matched (Remaining, Remaining) (Either a b)
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic (Either a b))
  (Remaining, Remaining)
  (Remaining, Checked)
  (Term b)
  Remaining
  Checked
-> (Term b -> Goal ())
-> (Matched (Remaining, Checked) (Either a b) -> Goal ())
-> Matched (Remaining, Remaining) (Either a b)
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' p (Tagged Remaining (Term b)) (f (Tagged Checked (Term b)))
-> p (Tagged (Remaining, Remaining) (Logic (Either a b)))
     (f (Tagged (Remaining, Checked) (Logic (Either a b))))
p (Tagged Remaining (Term b)) (f (Tagged Checked (Term b)))
-> p (Tagged (Remaining, Remaining) (LogicEither a b))
     (f (Tagged (Remaining, Checked) (LogicEither a b)))
forall a b logicLeft logicRight logicRight' (p :: * -> * -> *)
       (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged logicRight (Term b)) (f (Tagged logicRight' (Term b)))
-> p (Tagged (logicLeft, logicRight) (LogicEither a b))
     (f (Tagged (logicLeft, logicRight') (LogicEither a b)))
ExhaustivePrism
  (Logic (Either a b))
  (Remaining, Remaining)
  (Remaining, Checked)
  (Term b)
  Remaining
  Checked
_LogicRight' (\Term b
_ -> () -> Goal ()
forall a. a -> Goal a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
    (Matched (Remaining, Remaining) (Either a b) -> Goal ())
-> ((Matched (Remaining, Remaining) (Either a b) -> Goal ())
    -> Term (Either a b) -> Goal ())
-> Term (Either a b)
-> Goal ()
forall a b. a -> (a -> b) -> b
& (Matched (Remaining, Remaining) (Either a b) -> Goal ())
-> Term (Either a b) -> Goal ()
forall m a x. (Matched m a -> Goal x) -> Term a -> Goal x
enter'

nestedo' :: Term (Either (Either Int Bool) Int) -> Goal ()
nestedo' :: Term (Either (Either Int Bool) Int) -> Goal ()
nestedo' =
  Matched
  ((Checked, Checked), Checked) (Either (Either Int Bool) Int)
-> Goal ()
forall m a x. Exhausted m => Matched m a -> Goal x
matche'
    (Matched
   ((Checked, Checked), Checked) (Either (Either Int Bool) Int)
 -> Goal ())
-> ((Matched
       ((Checked, Checked), Checked) (Either (Either Int Bool) Int)
     -> Goal ())
    -> Matched
         ((Remaining, Checked), Checked) (Either (Either Int Bool) Int)
    -> Goal ())
-> Matched
     ((Remaining, Checked), Checked) (Either (Either Int Bool) Int)
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic (Either (Either Int Bool) Int))
  ((Remaining, Checked), Checked)
  ((Checked, Checked), Checked)
  (Term Int)
  Remaining
  Checked
-> (Term Int -> Goal ())
-> (Matched
      ((Checked, Checked), Checked) (Either (Either Int Bool) Int)
    -> Goal ())
-> Matched
     ((Remaining, Checked), Checked) (Either (Either Int Bool) Int)
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' (p (Tagged (Remaining, Checked) (Term (Either Int Bool)))
  (f (Tagged (Checked, Checked) (Term (Either Int Bool))))
-> p (Tagged
        ((Remaining, Checked), Checked)
        (LogicEither (Either Int Bool) Int))
     (f (Tagged
           ((Checked, Checked), Checked) (LogicEither (Either Int Bool) Int)))
forall a b logicLeft logicRight logicLeft' (p :: * -> * -> *)
       (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged logicLeft (Term a)) (f (Tagged logicLeft' (Term a)))
-> p (Tagged (logicLeft, logicRight) (LogicEither a b))
     (f (Tagged (logicLeft', logicRight) (LogicEither a b)))
_LogicLeft' (p (Tagged (Remaining, Checked) (Term (Either Int Bool)))
   (f (Tagged (Checked, Checked) (Term (Either Int Bool))))
 -> p (Tagged
         ((Remaining, Checked), Checked)
         (LogicEither (Either Int Bool) Int))
      (f (Tagged
            ((Checked, Checked), Checked)
            (LogicEither (Either Int Bool) Int))))
-> (p (Tagged Remaining (Term Int)) (f (Tagged Checked (Term Int)))
    -> p (Tagged (Remaining, Checked) (Term (Either Int Bool)))
         (f (Tagged (Checked, Checked) (Term (Either Int Bool)))))
-> p (Tagged Remaining (Term Int)) (f (Tagged Checked (Term Int)))
-> p (Tagged
        ((Remaining, Checked), Checked)
        (LogicEither (Either Int Bool) Int))
     (f (Tagged
           ((Checked, Checked), Checked) (LogicEither (Either Int Bool) Int)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged (Remaining, Checked) (Logic (Either Int Bool)))
  (f (Tagged (Checked, Checked) (Logic (Either Int Bool))))
-> p (Tagged (Remaining, Checked) (Term (Either Int Bool)))
     (f (Tagged (Checked, Checked) (Term (Either Int Bool))))
p (Tagged (Remaining, Checked) (LogicEither Int Bool))
  (f (Tagged (Checked, Checked) (LogicEither Int Bool)))
-> p (Tagged (Remaining, Checked) (Term (Either Int Bool)))
     (f (Tagged (Checked, Checked) (Term (Either Int Bool))))
forall a m m' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged m (Logic a)) (f (Tagged m' (Logic a)))
-> p (Tagged m (Term a)) (f (Tagged m' (Term a)))
_Value' (p (Tagged (Remaining, Checked) (LogicEither Int Bool))
   (f (Tagged (Checked, Checked) (LogicEither Int Bool)))
 -> p (Tagged (Remaining, Checked) (Term (Either Int Bool)))
      (f (Tagged (Checked, Checked) (Term (Either Int Bool)))))
-> (p (Tagged Remaining (Term Int)) (f (Tagged Checked (Term Int)))
    -> p (Tagged (Remaining, Checked) (LogicEither Int Bool))
         (f (Tagged (Checked, Checked) (LogicEither Int Bool))))
-> p (Tagged Remaining (Term Int)) (f (Tagged Checked (Term Int)))
-> p (Tagged (Remaining, Checked) (Term (Either Int Bool)))
     (f (Tagged (Checked, Checked) (Term (Either Int Bool))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged Remaining (Term Int)) (f (Tagged Checked (Term Int)))
-> p (Tagged (Remaining, Checked) (LogicEither Int Bool))
     (f (Tagged (Checked, Checked) (LogicEither Int Bool)))
forall a b logicLeft logicRight logicLeft' (p :: * -> * -> *)
       (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged logicLeft (Term a)) (f (Tagged logicLeft' (Term a)))
-> p (Tagged (logicLeft, logicRight) (LogicEither a b))
     (f (Tagged (logicLeft', logicRight) (LogicEither a b)))
_LogicLeft') (Term Int -> Term Int -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term Int
42)
    (Matched
   ((Remaining, Checked), Checked) (Either (Either Int Bool) Int)
 -> Goal ())
-> ((Matched
       ((Remaining, Checked), Checked) (Either (Either Int Bool) Int)
     -> Goal ())
    -> Matched
         ((Remaining, Remaining), Checked) (Either (Either Int Bool) Int)
    -> Goal ())
-> Matched
     ((Remaining, Remaining), Checked) (Either (Either Int Bool) Int)
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic (Either (Either Int Bool) Int))
  ((Remaining, Remaining), Checked)
  ((Remaining, Checked), Checked)
  (Term Bool)
  Remaining
  Checked
-> (Term Bool -> Goal ())
-> (Matched
      ((Remaining, Checked), Checked) (Either (Either Int Bool) Int)
    -> Goal ())
-> Matched
     ((Remaining, Remaining), Checked) (Either (Either Int Bool) Int)
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' (p (Tagged (Remaining, Remaining) (Term (Either Int Bool)))
  (f (Tagged (Remaining, Checked) (Term (Either Int Bool))))
-> p (Tagged
        ((Remaining, Remaining), Checked)
        (LogicEither (Either Int Bool) Int))
     (f (Tagged
           ((Remaining, Checked), Checked)
           (LogicEither (Either Int Bool) Int)))
forall a b logicLeft logicRight logicLeft' (p :: * -> * -> *)
       (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged logicLeft (Term a)) (f (Tagged logicLeft' (Term a)))
-> p (Tagged (logicLeft, logicRight) (LogicEither a b))
     (f (Tagged (logicLeft', logicRight) (LogicEither a b)))
_LogicLeft' (p (Tagged (Remaining, Remaining) (Term (Either Int Bool)))
   (f (Tagged (Remaining, Checked) (Term (Either Int Bool))))
 -> p (Tagged
         ((Remaining, Remaining), Checked)
         (LogicEither (Either Int Bool) Int))
      (f (Tagged
            ((Remaining, Checked), Checked)
            (LogicEither (Either Int Bool) Int))))
-> (p (Tagged Remaining (Term Bool))
      (f (Tagged Checked (Term Bool)))
    -> p (Tagged (Remaining, Remaining) (Term (Either Int Bool)))
         (f (Tagged (Remaining, Checked) (Term (Either Int Bool)))))
-> p (Tagged Remaining (Term Bool))
     (f (Tagged Checked (Term Bool)))
-> p (Tagged
        ((Remaining, Remaining), Checked)
        (LogicEither (Either Int Bool) Int))
     (f (Tagged
           ((Remaining, Checked), Checked)
           (LogicEither (Either Int Bool) Int)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged (Remaining, Remaining) (Logic (Either Int Bool)))
  (f (Tagged (Remaining, Checked) (Logic (Either Int Bool))))
-> p (Tagged (Remaining, Remaining) (Term (Either Int Bool)))
     (f (Tagged (Remaining, Checked) (Term (Either Int Bool))))
p (Tagged (Remaining, Remaining) (LogicEither Int Bool))
  (f (Tagged (Remaining, Checked) (LogicEither Int Bool)))
-> p (Tagged (Remaining, Remaining) (Term (Either Int Bool)))
     (f (Tagged (Remaining, Checked) (Term (Either Int Bool))))
forall a m m' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged m (Logic a)) (f (Tagged m' (Logic a)))
-> p (Tagged m (Term a)) (f (Tagged m' (Term a)))
_Value' (p (Tagged (Remaining, Remaining) (LogicEither Int Bool))
   (f (Tagged (Remaining, Checked) (LogicEither Int Bool)))
 -> p (Tagged (Remaining, Remaining) (Term (Either Int Bool)))
      (f (Tagged (Remaining, Checked) (Term (Either Int Bool)))))
-> (p (Tagged Remaining (Term Bool))
      (f (Tagged Checked (Term Bool)))
    -> p (Tagged (Remaining, Remaining) (LogicEither Int Bool))
         (f (Tagged (Remaining, Checked) (LogicEither Int Bool))))
-> p (Tagged Remaining (Term Bool))
     (f (Tagged Checked (Term Bool)))
-> p (Tagged (Remaining, Remaining) (Term (Either Int Bool)))
     (f (Tagged (Remaining, Checked) (Term (Either Int Bool))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged Remaining (Term Bool)) (f (Tagged Checked (Term Bool)))
-> p (Tagged (Remaining, Remaining) (LogicEither Int Bool))
     (f (Tagged (Remaining, Checked) (LogicEither Int Bool)))
forall a b logicLeft logicRight logicRight' (p :: * -> * -> *)
       (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged logicRight (Term b)) (f (Tagged logicRight' (Term b)))
-> p (Tagged (logicLeft, logicRight) (LogicEither a b))
     (f (Tagged (logicLeft, logicRight') (LogicEither a b)))
_LogicRight') (Term Bool -> Term Bool -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bool -> Term Bool
forall a. Logic a -> Term a
Value Bool
Logic Bool
True)
    (Matched
   ((Remaining, Remaining), Checked) (Either (Either Int Bool) Int)
 -> Goal ())
-> ((Matched
       ((Remaining, Remaining), Checked) (Either (Either Int Bool) Int)
     -> Goal ())
    -> Matched
         ((Remaining, Remaining), Remaining) (Either (Either Int Bool) Int)
    -> Goal ())
-> Matched
     ((Remaining, Remaining), Remaining) (Either (Either Int Bool) Int)
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic (Either (Either Int Bool) Int))
  ((Remaining, Remaining), Remaining)
  ((Remaining, Remaining), Checked)
  (Term Int)
  Remaining
  Checked
-> (Term Int -> Goal ())
-> (Matched
      ((Remaining, Remaining), Checked) (Either (Either Int Bool) Int)
    -> Goal ())
-> Matched
     ((Remaining, Remaining), Remaining) (Either (Either Int Bool) Int)
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' p (Tagged Remaining (Term Int)) (f (Tagged Checked (Term Int)))
-> p (Tagged
        ((Remaining, Remaining), Remaining)
        (Logic (Either (Either Int Bool) Int)))
     (f (Tagged
           ((Remaining, Remaining), Checked)
           (Logic (Either (Either Int Bool) Int))))
p (Tagged Remaining (Term Int)) (f (Tagged Checked (Term Int)))
-> p (Tagged
        ((Remaining, Remaining), Remaining)
        (LogicEither (Either Int Bool) Int))
     (f (Tagged
           ((Remaining, Remaining), Checked)
           (LogicEither (Either Int Bool) Int)))
forall a b logicLeft logicRight logicRight' (p :: * -> * -> *)
       (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged logicRight (Term b)) (f (Tagged logicRight' (Term b)))
-> p (Tagged (logicLeft, logicRight) (LogicEither a b))
     (f (Tagged (logicLeft, logicRight') (LogicEither a b)))
ExhaustivePrism
  (Logic (Either (Either Int Bool) Int))
  ((Remaining, Remaining), Remaining)
  ((Remaining, Remaining), Checked)
  (Term Int)
  Remaining
  Checked
_LogicRight' (Term Int -> Term Int -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term Int
1729)
    (Matched
   ((Remaining, Remaining), Remaining) (Either (Either Int Bool) Int)
 -> Goal ())
-> ((Matched
       ((Remaining, Remaining), Remaining) (Either (Either Int Bool) Int)
     -> Goal ())
    -> Term (Either (Either Int Bool) Int) -> Goal ())
-> Term (Either (Either Int Bool) Int)
-> Goal ()
forall a b. a -> (a -> b) -> b
& (Matched
   ((Remaining, Remaining), Remaining) (Either (Either Int Bool) Int)
 -> Goal ())
-> Term (Either (Either Int Bool) Int) -> Goal ()
forall m a x. (Matched m a -> Goal x) -> Term a -> Goal x
enter'

data Nat
  = Z
  | S Nat
  deriving (Int -> Nat -> ShowS
[Nat] -> ShowS
Nat -> String
(Int -> Nat -> ShowS)
-> (Nat -> String) -> ([Nat] -> ShowS) -> Show Nat
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Nat -> ShowS
showsPrec :: Int -> Nat -> ShowS
$cshow :: Nat -> String
show :: Nat -> String
$cshowList :: [Nat] -> ShowS
showList :: [Nat] -> ShowS
Show, (forall x. Nat -> Rep Nat x)
-> (forall x. Rep Nat x -> Nat) -> Generic Nat
forall x. Rep Nat x -> Nat
forall x. Nat -> Rep Nat x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Nat -> Rep Nat x
from :: forall x. Nat -> Rep Nat x
$cto :: forall x. Rep Nat x -> Nat
to :: forall x. Rep Nat x -> Nat
Generic)

makeLogical ''Nat
makePrisms ''LogicNat

_Z' :: Prism (Tagged (z, s) LogicNat) (Tagged (z', s) LogicNat) (Tagged z ()) (Tagged z' ())
_Z' :: forall z s z' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged z ()) (f (Tagged z' ()))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z', s) LogicNat))
_Z' = AnIso
  LogicNat
  LogicNat
  (Tagged (z', s) LogicNat)
  (Tagged (z, s) LogicNat)
-> Iso
     (Tagged (z, s) LogicNat)
     (Tagged (z', s) LogicNat)
     LogicNat
     LogicNat
forall s t a b. AnIso s t a b -> Iso b a t s
from AnIso
  LogicNat
  LogicNat
  (Tagged (z', s) LogicNat)
  (Tagged (z, s) LogicNat)
forall b b' s s' (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (Tagged s b) (f (Tagged s' b')) -> p b (f b')
_Tagged (p LogicNat (f LogicNat)
 -> p (Tagged (z, s) LogicNat) (f (Tagged (z', s) LogicNat)))
-> (p (Tagged z ()) (f (Tagged z' ())) -> p LogicNat (f LogicNat))
-> p (Tagged z ()) (f (Tagged z' ()))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z', s) LogicNat))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p () (f ()) -> p LogicNat (f LogicNat)
Prism' LogicNat ()
_LogicZ (p () (f ()) -> p LogicNat (f LogicNat))
-> (p (Tagged z ()) (f (Tagged z' ())) -> p () (f ()))
-> p (Tagged z ()) (f (Tagged z' ()))
-> p LogicNat (f LogicNat)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged z ()) (f (Tagged z' ())) -> p () (f ())
forall b b' s s' (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (Tagged s b) (f (Tagged s' b')) -> p b (f b')
_Tagged

_S' :: Prism (Tagged (z, s) LogicNat) (Tagged (z, s') LogicNat) (Tagged s (Term Nat)) (Tagged s' (Term Nat))
_S' :: forall z s s' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z, s') LogicNat))
_S' = AnIso
  LogicNat
  LogicNat
  (Tagged (z, s') LogicNat)
  (Tagged (z, s) LogicNat)
-> Iso
     (Tagged (z, s) LogicNat)
     (Tagged (z, s') LogicNat)
     LogicNat
     LogicNat
forall s t a b. AnIso s t a b -> Iso b a t s
from AnIso
  LogicNat
  LogicNat
  (Tagged (z, s') LogicNat)
  (Tagged (z, s) LogicNat)
forall b b' s s' (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (Tagged s b) (f (Tagged s' b')) -> p b (f b')
_Tagged (p LogicNat (f LogicNat)
 -> p (Tagged (z, s) LogicNat) (f (Tagged (z, s') LogicNat)))
-> (p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
    -> p LogicNat (f LogicNat))
-> p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z, s') LogicNat))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Term Nat) (f (Term Nat)) -> p LogicNat (f LogicNat)
Prism' LogicNat (Term Nat)
_LogicS (p (Term Nat) (f (Term Nat)) -> p LogicNat (f LogicNat))
-> (p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
    -> p (Term Nat) (f (Term Nat)))
-> p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
-> p LogicNat (f LogicNat)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
-> p (Term Nat) (f (Term Nat))
forall b b' s s' (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (Tagged s b) (f (Tagged s' b')) -> p b (f b')
_Tagged

natToInto :: Term Nat -> Term Int -> Goal ()
natToInto :: Term Nat -> Term Int -> Goal ()
natToInto Term Nat
nat Term Int
int =
  Term Nat
nat
    Term Nat -> (Term Nat -> Goal ()) -> Goal ()
forall a b. a -> (a -> b) -> b
& ( Matched (Checked, (Checked, (Checked, Checked))) Nat -> Goal ()
forall m a x. Exhausted m => Matched m a -> Goal x
matche'
          (Matched (Checked, (Checked, (Checked, Checked))) Nat -> Goal ())
-> ((Matched (Checked, (Checked, (Checked, Checked))) Nat
     -> Goal ())
    -> Matched (Remaining, (Checked, (Checked, Checked))) Nat
    -> Goal ())
-> Matched (Remaining, (Checked, (Checked, Checked))) Nat
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic Nat)
  (Remaining, (Checked, (Checked, Checked)))
  (Checked, (Checked, (Checked, Checked)))
  ()
  Remaining
  Checked
-> (() -> Goal ())
-> (Matched (Checked, (Checked, (Checked, Checked))) Nat
    -> Goal ())
-> Matched (Remaining, (Checked, (Checked, Checked))) Nat
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged
        (Remaining, (Checked, (Checked, Checked))) (Logic Nat))
     (f (Tagged (Checked, (Checked, (Checked, Checked))) (Logic Nat)))
p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, (Checked, (Checked, Checked))) LogicNat)
     (f (Tagged (Checked, (Checked, (Checked, Checked))) LogicNat))
forall z s z' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged z ()) (f (Tagged z' ()))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z', s) LogicNat))
ExhaustivePrism
  (Logic Nat)
  (Remaining, (Checked, (Checked, Checked)))
  (Checked, (Checked, (Checked, Checked)))
  ()
  Remaining
  Checked
_Z' (\() -> Term Int
int Term Int -> Term Int -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term Int
0)
          (Matched (Remaining, (Checked, (Checked, Checked))) Nat -> Goal ())
-> ((Matched (Remaining, (Checked, (Checked, Checked))) Nat
     -> Goal ())
    -> Matched (Remaining, (Remaining, (Checked, Checked))) Nat
    -> Goal ())
-> Matched (Remaining, (Remaining, (Checked, Checked))) Nat
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic Nat)
  (Remaining, (Remaining, (Checked, Checked)))
  (Remaining, (Checked, (Checked, Checked)))
  ()
  Remaining
  Checked
-> (() -> Goal ())
-> (Matched (Remaining, (Checked, (Checked, Checked))) Nat
    -> Goal ())
-> Matched (Remaining, (Remaining, (Checked, Checked))) Nat
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' (p (Tagged (Remaining, (Checked, Checked)) (Term Nat))
  (f (Tagged (Checked, (Checked, Checked)) (Term Nat)))
-> p (Tagged (Remaining, (Remaining, (Checked, Checked))) LogicNat)
     (f (Tagged (Remaining, (Checked, (Checked, Checked))) LogicNat))
forall z s s' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z, s') LogicNat))
_S' (p (Tagged (Remaining, (Checked, Checked)) (Term Nat))
   (f (Tagged (Checked, (Checked, Checked)) (Term Nat)))
 -> p (Tagged (Remaining, (Remaining, (Checked, Checked))) LogicNat)
      (f (Tagged (Remaining, (Checked, (Checked, Checked))) LogicNat)))
-> (p (Tagged Remaining ()) (f (Tagged Checked ()))
    -> p (Tagged (Remaining, (Checked, Checked)) (Term Nat))
         (f (Tagged (Checked, (Checked, Checked)) (Term Nat))))
-> p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, (Remaining, (Checked, Checked))) LogicNat)
     (f (Tagged (Remaining, (Checked, (Checked, Checked))) LogicNat))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged (Remaining, (Checked, Checked)) (Logic Nat))
  (f (Tagged (Checked, (Checked, Checked)) (Logic Nat)))
-> p (Tagged (Remaining, (Checked, Checked)) (Term Nat))
     (f (Tagged (Checked, (Checked, Checked)) (Term Nat)))
p (Tagged (Remaining, (Checked, Checked)) LogicNat)
  (f (Tagged (Checked, (Checked, Checked)) LogicNat))
-> p (Tagged (Remaining, (Checked, Checked)) (Term Nat))
     (f (Tagged (Checked, (Checked, Checked)) (Term Nat)))
forall a m m' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged m (Logic a)) (f (Tagged m' (Logic a)))
-> p (Tagged m (Term a)) (f (Tagged m' (Term a)))
_Value' (p (Tagged (Remaining, (Checked, Checked)) LogicNat)
   (f (Tagged (Checked, (Checked, Checked)) LogicNat))
 -> p (Tagged (Remaining, (Checked, Checked)) (Term Nat))
      (f (Tagged (Checked, (Checked, Checked)) (Term Nat))))
-> (p (Tagged Remaining ()) (f (Tagged Checked ()))
    -> p (Tagged (Remaining, (Checked, Checked)) LogicNat)
         (f (Tagged (Checked, (Checked, Checked)) LogicNat)))
-> p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, (Checked, Checked)) (Term Nat))
     (f (Tagged (Checked, (Checked, Checked)) (Term Nat)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, (Checked, Checked)) LogicNat)
     (f (Tagged (Checked, (Checked, Checked)) LogicNat))
forall z s z' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged z ()) (f (Tagged z' ()))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z', s) LogicNat))
_Z') (\() -> Term Int
int Term Int -> Term Int -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term Int
1)
          (Matched (Remaining, (Remaining, (Checked, Checked))) Nat
 -> Goal ())
-> ((Matched (Remaining, (Remaining, (Checked, Checked))) Nat
     -> Goal ())
    -> Matched (Remaining, (Remaining, (Remaining, Checked))) Nat
    -> Goal ())
-> Matched (Remaining, (Remaining, (Remaining, Checked))) Nat
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic Nat)
  (Remaining, (Remaining, (Remaining, Checked)))
  (Remaining, (Remaining, (Checked, Checked)))
  ()
  Remaining
  Checked
-> (() -> Goal ())
-> (Matched (Remaining, (Remaining, (Checked, Checked))) Nat
    -> Goal ())
-> Matched (Remaining, (Remaining, (Remaining, Checked))) Nat
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' (p (Tagged (Remaining, (Remaining, Checked)) (Term Nat))
  (f (Tagged (Remaining, (Checked, Checked)) (Term Nat)))
-> p (Tagged
        (Remaining, (Remaining, (Remaining, Checked))) LogicNat)
     (f (Tagged (Remaining, (Remaining, (Checked, Checked))) LogicNat))
forall z s s' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z, s') LogicNat))
_S' (p (Tagged (Remaining, (Remaining, Checked)) (Term Nat))
   (f (Tagged (Remaining, (Checked, Checked)) (Term Nat)))
 -> p (Tagged
         (Remaining, (Remaining, (Remaining, Checked))) LogicNat)
      (f (Tagged (Remaining, (Remaining, (Checked, Checked))) LogicNat)))
-> (p (Tagged Remaining ()) (f (Tagged Checked ()))
    -> p (Tagged (Remaining, (Remaining, Checked)) (Term Nat))
         (f (Tagged (Remaining, (Checked, Checked)) (Term Nat))))
-> p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged
        (Remaining, (Remaining, (Remaining, Checked))) LogicNat)
     (f (Tagged (Remaining, (Remaining, (Checked, Checked))) LogicNat))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged (Remaining, (Remaining, Checked)) (Logic Nat))
  (f (Tagged (Remaining, (Checked, Checked)) (Logic Nat)))
-> p (Tagged (Remaining, (Remaining, Checked)) (Term Nat))
     (f (Tagged (Remaining, (Checked, Checked)) (Term Nat)))
p (Tagged (Remaining, (Remaining, Checked)) LogicNat)
  (f (Tagged (Remaining, (Checked, Checked)) LogicNat))
-> p (Tagged (Remaining, (Remaining, Checked)) (Term Nat))
     (f (Tagged (Remaining, (Checked, Checked)) (Term Nat)))
forall a m m' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged m (Logic a)) (f (Tagged m' (Logic a)))
-> p (Tagged m (Term a)) (f (Tagged m' (Term a)))
_Value' (p (Tagged (Remaining, (Remaining, Checked)) LogicNat)
   (f (Tagged (Remaining, (Checked, Checked)) LogicNat))
 -> p (Tagged (Remaining, (Remaining, Checked)) (Term Nat))
      (f (Tagged (Remaining, (Checked, Checked)) (Term Nat))))
-> (p (Tagged Remaining ()) (f (Tagged Checked ()))
    -> p (Tagged (Remaining, (Remaining, Checked)) LogicNat)
         (f (Tagged (Remaining, (Checked, Checked)) LogicNat)))
-> p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, (Remaining, Checked)) (Term Nat))
     (f (Tagged (Remaining, (Checked, Checked)) (Term Nat)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged (Remaining, Checked) (Term Nat))
  (f (Tagged (Checked, Checked) (Term Nat)))
-> p (Tagged (Remaining, (Remaining, Checked)) LogicNat)
     (f (Tagged (Remaining, (Checked, Checked)) LogicNat))
forall z s s' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z, s') LogicNat))
_S' (p (Tagged (Remaining, Checked) (Term Nat))
   (f (Tagged (Checked, Checked) (Term Nat)))
 -> p (Tagged (Remaining, (Remaining, Checked)) LogicNat)
      (f (Tagged (Remaining, (Checked, Checked)) LogicNat)))
-> (p (Tagged Remaining ()) (f (Tagged Checked ()))
    -> p (Tagged (Remaining, Checked) (Term Nat))
         (f (Tagged (Checked, Checked) (Term Nat))))
-> p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, (Remaining, Checked)) LogicNat)
     (f (Tagged (Remaining, (Checked, Checked)) LogicNat))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged (Remaining, Checked) (Logic Nat))
  (f (Tagged (Checked, Checked) (Logic Nat)))
-> p (Tagged (Remaining, Checked) (Term Nat))
     (f (Tagged (Checked, Checked) (Term Nat)))
p (Tagged (Remaining, Checked) LogicNat)
  (f (Tagged (Checked, Checked) LogicNat))
-> p (Tagged (Remaining, Checked) (Term Nat))
     (f (Tagged (Checked, Checked) (Term Nat)))
forall a m m' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged m (Logic a)) (f (Tagged m' (Logic a)))
-> p (Tagged m (Term a)) (f (Tagged m' (Term a)))
_Value' (p (Tagged (Remaining, Checked) LogicNat)
   (f (Tagged (Checked, Checked) LogicNat))
 -> p (Tagged (Remaining, Checked) (Term Nat))
      (f (Tagged (Checked, Checked) (Term Nat))))
-> (p (Tagged Remaining ()) (f (Tagged Checked ()))
    -> p (Tagged (Remaining, Checked) LogicNat)
         (f (Tagged (Checked, Checked) LogicNat)))
-> p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, Checked) (Term Nat))
     (f (Tagged (Checked, Checked) (Term Nat)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, Checked) LogicNat)
     (f (Tagged (Checked, Checked) LogicNat))
forall z s z' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged z ()) (f (Tagged z' ()))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z', s) LogicNat))
_Z') (\() -> Term Int
int Term Int -> Term Int -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term Int
2)
          (Matched (Remaining, (Remaining, (Remaining, Checked))) Nat
 -> Goal ())
-> ((Matched (Remaining, (Remaining, (Remaining, Checked))) Nat
     -> Goal ())
    -> Matched (Remaining, (Remaining, (Remaining, Remaining))) Nat
    -> Goal ())
-> Matched (Remaining, (Remaining, (Remaining, Remaining))) Nat
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic Nat)
  (Remaining, (Remaining, (Remaining, Remaining)))
  (Remaining, (Remaining, (Remaining, Checked)))
  (Term Nat)
  Remaining
  Checked
-> (Term Nat -> Goal ())
-> (Matched (Remaining, (Remaining, (Remaining, Checked))) Nat
    -> Goal ())
-> Matched (Remaining, (Remaining, (Remaining, Remaining))) Nat
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' (p (Tagged (Remaining, (Remaining, Remaining)) (Term Nat))
  (f (Tagged (Remaining, (Remaining, Checked)) (Term Nat)))
-> p (Tagged
        (Remaining, (Remaining, (Remaining, Remaining))) LogicNat)
     (f (Tagged
           (Remaining, (Remaining, (Remaining, Checked))) LogicNat))
forall z s s' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z, s') LogicNat))
_S' (p (Tagged (Remaining, (Remaining, Remaining)) (Term Nat))
   (f (Tagged (Remaining, (Remaining, Checked)) (Term Nat)))
 -> p (Tagged
         (Remaining, (Remaining, (Remaining, Remaining))) LogicNat)
      (f (Tagged
            (Remaining, (Remaining, (Remaining, Checked))) LogicNat)))
-> (p (Tagged Remaining (Term Nat)) (f (Tagged Checked (Term Nat)))
    -> p (Tagged (Remaining, (Remaining, Remaining)) (Term Nat))
         (f (Tagged (Remaining, (Remaining, Checked)) (Term Nat))))
-> p (Tagged Remaining (Term Nat)) (f (Tagged Checked (Term Nat)))
-> p (Tagged
        (Remaining, (Remaining, (Remaining, Remaining))) LogicNat)
     (f (Tagged
           (Remaining, (Remaining, (Remaining, Checked))) LogicNat))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged (Remaining, (Remaining, Remaining)) (Logic Nat))
  (f (Tagged (Remaining, (Remaining, Checked)) (Logic Nat)))
-> p (Tagged (Remaining, (Remaining, Remaining)) (Term Nat))
     (f (Tagged (Remaining, (Remaining, Checked)) (Term Nat)))
p (Tagged (Remaining, (Remaining, Remaining)) LogicNat)
  (f (Tagged (Remaining, (Remaining, Checked)) LogicNat))
-> p (Tagged (Remaining, (Remaining, Remaining)) (Term Nat))
     (f (Tagged (Remaining, (Remaining, Checked)) (Term Nat)))
forall a m m' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged m (Logic a)) (f (Tagged m' (Logic a)))
-> p (Tagged m (Term a)) (f (Tagged m' (Term a)))
_Value' (p (Tagged (Remaining, (Remaining, Remaining)) LogicNat)
   (f (Tagged (Remaining, (Remaining, Checked)) LogicNat))
 -> p (Tagged (Remaining, (Remaining, Remaining)) (Term Nat))
      (f (Tagged (Remaining, (Remaining, Checked)) (Term Nat))))
-> (p (Tagged Remaining (Term Nat)) (f (Tagged Checked (Term Nat)))
    -> p (Tagged (Remaining, (Remaining, Remaining)) LogicNat)
         (f (Tagged (Remaining, (Remaining, Checked)) LogicNat)))
-> p (Tagged Remaining (Term Nat)) (f (Tagged Checked (Term Nat)))
-> p (Tagged (Remaining, (Remaining, Remaining)) (Term Nat))
     (f (Tagged (Remaining, (Remaining, Checked)) (Term Nat)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged (Remaining, Remaining) (Term Nat))
  (f (Tagged (Remaining, Checked) (Term Nat)))
-> p (Tagged (Remaining, (Remaining, Remaining)) LogicNat)
     (f (Tagged (Remaining, (Remaining, Checked)) LogicNat))
forall z s s' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z, s') LogicNat))
_S' (p (Tagged (Remaining, Remaining) (Term Nat))
   (f (Tagged (Remaining, Checked) (Term Nat)))
 -> p (Tagged (Remaining, (Remaining, Remaining)) LogicNat)
      (f (Tagged (Remaining, (Remaining, Checked)) LogicNat)))
-> (p (Tagged Remaining (Term Nat)) (f (Tagged Checked (Term Nat)))
    -> p (Tagged (Remaining, Remaining) (Term Nat))
         (f (Tagged (Remaining, Checked) (Term Nat))))
-> p (Tagged Remaining (Term Nat)) (f (Tagged Checked (Term Nat)))
-> p (Tagged (Remaining, (Remaining, Remaining)) LogicNat)
     (f (Tagged (Remaining, (Remaining, Checked)) LogicNat))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged (Remaining, Remaining) (Logic Nat))
  (f (Tagged (Remaining, Checked) (Logic Nat)))
-> p (Tagged (Remaining, Remaining) (Term Nat))
     (f (Tagged (Remaining, Checked) (Term Nat)))
p (Tagged (Remaining, Remaining) LogicNat)
  (f (Tagged (Remaining, Checked) LogicNat))
-> p (Tagged (Remaining, Remaining) (Term Nat))
     (f (Tagged (Remaining, Checked) (Term Nat)))
forall a m m' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged m (Logic a)) (f (Tagged m' (Logic a)))
-> p (Tagged m (Term a)) (f (Tagged m' (Term a)))
_Value' (p (Tagged (Remaining, Remaining) LogicNat)
   (f (Tagged (Remaining, Checked) LogicNat))
 -> p (Tagged (Remaining, Remaining) (Term Nat))
      (f (Tagged (Remaining, Checked) (Term Nat))))
-> (p (Tagged Remaining (Term Nat)) (f (Tagged Checked (Term Nat)))
    -> p (Tagged (Remaining, Remaining) LogicNat)
         (f (Tagged (Remaining, Checked) LogicNat)))
-> p (Tagged Remaining (Term Nat)) (f (Tagged Checked (Term Nat)))
-> p (Tagged (Remaining, Remaining) (Term Nat))
     (f (Tagged (Remaining, Checked) (Term Nat)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p (Tagged Remaining (Term Nat)) (f (Tagged Checked (Term Nat)))
-> p (Tagged (Remaining, Remaining) LogicNat)
     (f (Tagged (Remaining, Checked) LogicNat))
forall z s s' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged s (Term Nat)) (f (Tagged s' (Term Nat)))
-> p (Tagged (z, s) LogicNat) (f (Tagged (z, s') LogicNat))
_S') (Goal () -> Term Nat -> Goal ()
forall a b. a -> b -> a
const Goal ()
forall x. Goal x
failo) -- give up
          (Matched (Remaining, (Remaining, (Remaining, Remaining))) Nat
 -> Goal ())
-> ((Matched (Remaining, (Remaining, (Remaining, Remaining))) Nat
     -> Goal ())
    -> Term Nat -> Goal ())
-> Term Nat
-> Goal ()
forall a b. a -> (a -> b) -> b
& (Matched (Remaining, (Remaining, (Remaining, Remaining))) Nat
 -> Goal ())
-> Term Nat -> Goal ()
forall m a x. (Matched m a -> Goal x) -> Term a -> Goal x
enter'
      )

example :: IO ()
example :: IO ()
example = do
  String -> IO ()
putStrLn String
"eithero:"
  (Term (Either Int Bool) -> IO ())
-> [Term (Either Int Bool)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Term (Either Int Bool) -> IO ()
forall a. Show a => a -> IO ()
print ([Term (Either Int Bool)] -> IO ())
-> [Term (Either Int Bool)] -> IO ()
forall a b. (a -> b) -> a -> b
$ (Term (Either Int Bool) -> Goal ()) -> [Term (Either Int Bool)]
forall v. Fresh v => (v -> Goal ()) -> [v]
run (forall a b. (Logical a, Logical b) => Term (Either a b) -> Goal ()
eithero @Int @Bool)

  String -> IO ()
putStrLn String
"\neithero':"
  (Term (Either Int Bool) -> IO ())
-> [Term (Either Int Bool)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Term (Either Int Bool) -> IO ()
forall a. Show a => a -> IO ()
print ([Term (Either Int Bool)] -> IO ())
-> [Term (Either Int Bool)] -> IO ()
forall a b. (a -> b) -> a -> b
$ (Term (Either Int Bool) -> Goal ()) -> [Term (Either Int Bool)]
forall v. Fresh v => (v -> Goal ()) -> [v]
run (forall a b. (Logical a, Logical b) => Term (Either a b) -> Goal ()
eithero' @Int @Bool)

  String -> IO ()
putStrLn String
"\nnestedo:"
  (Maybe (Either (Either Int Bool) Int) -> IO ())
-> [Maybe (Either (Either Int Bool) Int)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Maybe (Either (Either Int Bool) Int) -> IO ()
forall a. Show a => a -> IO ()
print ([Maybe (Either (Either Int Bool) Int)] -> IO ())
-> [Maybe (Either (Either Int Bool) Int)] -> IO ()
forall a b. (a -> b) -> a -> b
$ Term (Either (Either Int Bool) Int)
-> Maybe (Either (Either Int Bool) Int)
forall a. Logical a => Term a -> Maybe a
extract' (Term (Either (Either Int Bool) Int)
 -> Maybe (Either (Either Int Bool) Int))
-> [Term (Either (Either Int Bool) Int)]
-> [Maybe (Either (Either Int Bool) Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term (Either (Either Int Bool) Int) -> Goal ())
-> [Term (Either (Either Int Bool) Int)]
forall v. Fresh v => (v -> Goal ()) -> [v]
run Term (Either (Either Int Bool) Int) -> Goal ()
nestedo

  String -> IO ()
putStrLn String
"\nnestedo':"
  (Maybe (Either (Either Int Bool) Int) -> IO ())
-> [Maybe (Either (Either Int Bool) Int)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Maybe (Either (Either Int Bool) Int) -> IO ()
forall a. Show a => a -> IO ()
print ([Maybe (Either (Either Int Bool) Int)] -> IO ())
-> [Maybe (Either (Either Int Bool) Int)] -> IO ()
forall a b. (a -> b) -> a -> b
$ Term (Either (Either Int Bool) Int)
-> Maybe (Either (Either Int Bool) Int)
forall a. Logical a => Term a -> Maybe a
extract' (Term (Either (Either Int Bool) Int)
 -> Maybe (Either (Either Int Bool) Int))
-> [Term (Either (Either Int Bool) Int)]
-> [Maybe (Either (Either Int Bool) Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term (Either (Either Int Bool) Int) -> Goal ())
-> [Term (Either (Either Int Bool) Int)]
forall v. Fresh v => (v -> Goal ()) -> [v]
run Term (Either (Either Int Bool) Int) -> Goal ()
nestedo'

  String -> IO ()
putStrLn String
"\nnatToInto:"
  ((Maybe Nat, Maybe Int) -> IO ())
-> [(Maybe Nat, Maybe Int)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Maybe Nat, Maybe Int) -> IO ()
forall a. Show a => a -> IO ()
print ([(Maybe Nat, Maybe Int)] -> IO ())
-> [(Maybe Nat, Maybe Int)] -> IO ()
forall a b. (a -> b) -> a -> b
$ (Term Nat -> Maybe Nat)
-> (Term Int -> Maybe Int)
-> (Term Nat, Term Int)
-> (Maybe Nat, Maybe Int)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Term Nat -> Maybe Nat
forall a. Logical a => Term a -> Maybe a
extract' Term Int -> Maybe Int
forall a. Logical a => Term a -> Maybe a
extract' ((Term Nat, Term Int) -> (Maybe Nat, Maybe Int))
-> [(Term Nat, Term Int)] -> [(Maybe Nat, Maybe Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term Nat, Term Int) -> Goal ()) -> [(Term Nat, Term Int)]
forall v. Fresh v => (v -> Goal ()) -> [v]
run ((Term Nat -> Term Int -> Goal ())
-> (Term Nat, Term Int) -> Goal ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Term Nat -> Term Int -> Goal ()
natToInto)