{-# LANGUAGE BangPatterns               #-}
{-# LANGUAGE DeriveAnyClass             #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DeriveTraversable          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs               #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE PatternSynonyms            #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE ViewPatterns               #-}

module Telomare where --(IExpr(..), ParserTerm(..), LamType(..), Term1(..), Term2(..), Term3(..), Term4(..)
               --, FragExpr(..), FragIndex, TelomareLike, fromTelomare, toTelomare, rootFrag) where

import Control.Applicative (Applicative (liftA2), liftA, liftA3)
import Control.Comonad.Cofree (Cofree ((:<)))
import qualified Control.Comonad.Trans.Cofree as CofreeT (CofreeF (..))
import Control.DeepSeq (NFData (..))
import Control.Lens.Combinators (Plated (..), makePrisms, transform)
import Control.Monad.Except (ExceptT)
import Control.Monad.State (State)
import qualified Control.Monad.State as State
import Data.Bool (bool)
import Data.Char (chr, ord)
import Data.Eq.Deriving (deriveEq1)
import Data.Functor.Foldable (Base, Corecursive (embed),
                              Recursive (cata, project))
import Data.Functor.Foldable.TH (MakeBaseFunctor (makeBaseFunctor))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Ord.Deriving (deriveOrd1)
import qualified Data.Set as Set
import Data.Void (Void)
import Debug.Trace (trace, traceShow, traceShowId)
import GHC.Generics (Generic)
import Text.Show.Deriving (deriveShow1)

{- top level TODO list
 - change AbortFrag form to something more convenient
 - extract abort logic from arbitrary expressions (like, make quick dynamic check the way we have static check)
 - make sure recur calls in unsized recursion combinator are structurally smaller ... although, we can fail sizing and report that to user
-}
-- TODO replace with a Plated fold
class MonoidEndoFolder a where
  monoidFold :: Monoid m => (a -> m) -> a -> m

data IExpr
  = Zero                     -- no special syntax necessary
  | Pair !IExpr !IExpr       -- (,)
  | Env                      -- identifier
  | SetEnv !IExpr -- SetEnv takes a Pair where the right part is Env and the left part is Defer. Inside the Defer is a closed lambda with all argument information on the right (i.e. Env)
  | Defer !IExpr
  -- the rest of these should be no argument constructors, to be treated as functions with setenv
  | Gate !IExpr !IExpr
  | PLeft !IExpr             -- left
  | PRight !IExpr            -- right
  | Trace
  deriving (IExpr -> IExpr -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IExpr -> IExpr -> Bool
$c/= :: IExpr -> IExpr -> Bool
== :: IExpr -> IExpr -> Bool
$c== :: IExpr -> IExpr -> Bool
Eq, Int -> IExpr -> ShowS
[IExpr] -> ShowS
IExpr -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IExpr] -> ShowS
$cshowList :: [IExpr] -> ShowS
show :: IExpr -> String
$cshow :: IExpr -> String
showsPrec :: Int -> IExpr -> ShowS
$cshowsPrec :: Int -> IExpr -> ShowS
Show, Eq IExpr
IExpr -> IExpr -> Bool
IExpr -> IExpr -> Ordering
IExpr -> IExpr -> IExpr
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: IExpr -> IExpr -> IExpr
$cmin :: IExpr -> IExpr -> IExpr
max :: IExpr -> IExpr -> IExpr
$cmax :: IExpr -> IExpr -> IExpr
>= :: IExpr -> IExpr -> Bool
$c>= :: IExpr -> IExpr -> Bool
> :: IExpr -> IExpr -> Bool
$c> :: IExpr -> IExpr -> Bool
<= :: IExpr -> IExpr -> Bool
$c<= :: IExpr -> IExpr -> Bool
< :: IExpr -> IExpr -> Bool
$c< :: IExpr -> IExpr -> Bool
compare :: IExpr -> IExpr -> Ordering
$ccompare :: IExpr -> IExpr -> Ordering
Ord, ReadPrec [IExpr]
ReadPrec IExpr
Int -> ReadS IExpr
ReadS [IExpr]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [IExpr]
$creadListPrec :: ReadPrec [IExpr]
readPrec :: ReadPrec IExpr
$creadPrec :: ReadPrec IExpr
readList :: ReadS [IExpr]
$creadList :: ReadS [IExpr]
readsPrec :: Int -> ReadS IExpr
$creadsPrec :: Int -> ReadS IExpr
Read)
makeBaseFunctor ''IExpr -- Functorial version IExprF.

instance Plated IExpr where
  plate :: Traversal' IExpr IExpr
plate IExpr -> f IExpr
f = \case
    Pair IExpr
a IExpr
b -> IExpr -> IExpr -> IExpr
Pair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> f IExpr
f IExpr
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IExpr -> f IExpr
f IExpr
b
    SetEnv IExpr
x -> IExpr -> IExpr
SetEnv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> f IExpr
f IExpr
x
    Defer IExpr
x  -> IExpr -> IExpr
Defer forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> f IExpr
f IExpr
x
    Gate IExpr
l IExpr
r -> IExpr -> IExpr -> IExpr
Gate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> f IExpr
f IExpr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IExpr -> f IExpr
f IExpr
r
    PLeft IExpr
x  -> IExpr -> IExpr
PLeft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> f IExpr
f IExpr
x
    PRight IExpr
x -> IExpr -> IExpr
PRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> f IExpr
f IExpr
x
    IExpr
x        -> forall (f :: * -> *) a. Applicative f => a -> f a
pure IExpr
x

-- probably should get rid of this in favor of ExprT
data ExprA a
  = ZeroA a
  | PairA (ExprA a) (ExprA a) a
  | EnvA a
  | SetEnvA (ExprA a) a
  | DeferA (ExprA a) a
  | AbortA a
  | GateA (ExprA a) (ExprA a) a
  | PLeftA (ExprA a) a
  | PRightA (ExprA a) a
  | TraceA a
  deriving (ExprA a -> ExprA a -> Bool
forall a. Eq a => ExprA a -> ExprA a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExprA a -> ExprA a -> Bool
$c/= :: forall a. Eq a => ExprA a -> ExprA a -> Bool
== :: ExprA a -> ExprA a -> Bool
$c== :: forall a. Eq a => ExprA a -> ExprA a -> Bool
Eq, ExprA a -> ExprA a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (ExprA a)
forall a. Ord a => ExprA a -> ExprA a -> Bool
forall a. Ord a => ExprA a -> ExprA a -> Ordering
forall a. Ord a => ExprA a -> ExprA a -> ExprA a
min :: ExprA a -> ExprA a -> ExprA a
$cmin :: forall a. Ord a => ExprA a -> ExprA a -> ExprA a
max :: ExprA a -> ExprA a -> ExprA a
$cmax :: forall a. Ord a => ExprA a -> ExprA a -> ExprA a
>= :: ExprA a -> ExprA a -> Bool
$c>= :: forall a. Ord a => ExprA a -> ExprA a -> Bool
> :: ExprA a -> ExprA a -> Bool
$c> :: forall a. Ord a => ExprA a -> ExprA a -> Bool
<= :: ExprA a -> ExprA a -> Bool
$c<= :: forall a. Ord a => ExprA a -> ExprA a -> Bool
< :: ExprA a -> ExprA a -> Bool
$c< :: forall a. Ord a => ExprA a -> ExprA a -> Bool
compare :: ExprA a -> ExprA a -> Ordering
$ccompare :: forall a. Ord a => ExprA a -> ExprA a -> Ordering
Ord, Int -> ExprA a -> ShowS
forall a. Show a => Int -> ExprA a -> ShowS
forall a. Show a => [ExprA a] -> ShowS
forall a. Show a => ExprA a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExprA a] -> ShowS
$cshowList :: forall a. Show a => [ExprA a] -> ShowS
show :: ExprA a -> String
$cshow :: forall a. Show a => ExprA a -> String
showsPrec :: Int -> ExprA a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ExprA a -> ShowS
Show)

-- so we can add annotations at any location in the AST
data ExprT a
  = ZeroT
  | PairT (ExprT a) (ExprT a)
  | EnvT
  | SetEnvT (ExprT a)
  | DeferT (ExprT a)
  | AbortT
  | GateT (ExprT a) (ExprT a)
  | LeftT (ExprT a)
  | RightT (ExprT a)
  | TraceT
  | TagT (ExprT a) a
  deriving (ExprT a -> ExprT a -> Bool
forall a. Eq a => ExprT a -> ExprT a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExprT a -> ExprT a -> Bool
$c/= :: forall a. Eq a => ExprT a -> ExprT a -> Bool
== :: ExprT a -> ExprT a -> Bool
$c== :: forall a. Eq a => ExprT a -> ExprT a -> Bool
Eq, ExprT a -> ExprT a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (ExprT a)
forall a. Ord a => ExprT a -> ExprT a -> Bool
forall a. Ord a => ExprT a -> ExprT a -> Ordering
forall a. Ord a => ExprT a -> ExprT a -> ExprT a
min :: ExprT a -> ExprT a -> ExprT a
$cmin :: forall a. Ord a => ExprT a -> ExprT a -> ExprT a
max :: ExprT a -> ExprT a -> ExprT a
$cmax :: forall a. Ord a => ExprT a -> ExprT a -> ExprT a
>= :: ExprT a -> ExprT a -> Bool
$c>= :: forall a. Ord a => ExprT a -> ExprT a -> Bool
> :: ExprT a -> ExprT a -> Bool
$c> :: forall a. Ord a => ExprT a -> ExprT a -> Bool
<= :: ExprT a -> ExprT a -> Bool
$c<= :: forall a. Ord a => ExprT a -> ExprT a -> Bool
< :: ExprT a -> ExprT a -> Bool
$c< :: forall a. Ord a => ExprT a -> ExprT a -> Bool
compare :: ExprT a -> ExprT a -> Ordering
$ccompare :: forall a. Ord a => ExprT a -> ExprT a -> Ordering
Ord, Int -> ExprT a -> ShowS
forall a. Show a => Int -> ExprT a -> ShowS
forall a. Show a => [ExprT a] -> ShowS
forall a. Show a => ExprT a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExprT a] -> ShowS
$cshowList :: forall a. Show a => [ExprT a] -> ShowS
show :: ExprT a -> String
$cshow :: forall a. Show a => ExprT a -> String
showsPrec :: Int -> ExprT a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ExprT a -> ShowS
Show)

-- there must be a typeclass I can derive that does this
getA :: ExprA a -> a
getA :: forall a. ExprA a -> a
getA (ZeroA a
a)     = a
a
getA (PairA ExprA a
_ ExprA a
_ a
a) = a
a
getA (EnvA a
a)      = a
a
getA (SetEnvA ExprA a
_ a
a) = a
a
getA (DeferA ExprA a
_ a
a)  = a
a
getA (AbortA a
a)    = a
a
getA (GateA ExprA a
_ ExprA a
_ a
a) = a
a
getA (PLeftA ExprA a
_ a
a)  = a
a
getA (PRightA ExprA a
_ a
a) = a
a
getA (TraceA a
a)    = a
a

-- | Lambdas can be closed if it's expresion does not depend on any
--   outer binding.
data LamType l
  = Open l
  | Closed l
  deriving (LamType l -> LamType l -> Bool
forall l. Eq l => LamType l -> LamType l -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LamType l -> LamType l -> Bool
$c/= :: forall l. Eq l => LamType l -> LamType l -> Bool
== :: LamType l -> LamType l -> Bool
$c== :: forall l. Eq l => LamType l -> LamType l -> Bool
Eq, Int -> LamType l -> ShowS
forall l. Show l => Int -> LamType l -> ShowS
forall l. Show l => [LamType l] -> ShowS
forall l. Show l => LamType l -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LamType l] -> ShowS
$cshowList :: forall l. Show l => [LamType l] -> ShowS
show :: LamType l -> String
$cshow :: forall l. Show l => LamType l -> String
showsPrec :: Int -> LamType l -> ShowS
$cshowsPrec :: forall l. Show l => Int -> LamType l -> ShowS
Show, LamType l -> LamType l -> Bool
LamType l -> LamType l -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {l}. Ord l => Eq (LamType l)
forall l. Ord l => LamType l -> LamType l -> Bool
forall l. Ord l => LamType l -> LamType l -> Ordering
forall l. Ord l => LamType l -> LamType l -> LamType l
min :: LamType l -> LamType l -> LamType l
$cmin :: forall l. Ord l => LamType l -> LamType l -> LamType l
max :: LamType l -> LamType l -> LamType l
$cmax :: forall l. Ord l => LamType l -> LamType l -> LamType l
>= :: LamType l -> LamType l -> Bool
$c>= :: forall l. Ord l => LamType l -> LamType l -> Bool
> :: LamType l -> LamType l -> Bool
$c> :: forall l. Ord l => LamType l -> LamType l -> Bool
<= :: LamType l -> LamType l -> Bool
$c<= :: forall l. Ord l => LamType l -> LamType l -> Bool
< :: LamType l -> LamType l -> Bool
$c< :: forall l. Ord l => LamType l -> LamType l -> Bool
compare :: LamType l -> LamType l -> Ordering
$ccompare :: forall l. Ord l => LamType l -> LamType l -> Ordering
Ord)

-- | Parser AST
data ParserTerm l v
  = TZero
  | TPair (ParserTerm l v) (ParserTerm l v)
  | TVar v
  | TApp (ParserTerm l v) (ParserTerm l v)
  | TCheck (ParserTerm l v) (ParserTerm l v)
  | TITE (ParserTerm l v) (ParserTerm l v) (ParserTerm l v)
  | TLeft (ParserTerm l v)
  | TRight (ParserTerm l v)
  | TTrace (ParserTerm l v)
  | THash (ParserTerm l v)
  | TChurch Int
  | TLam (LamType l) (ParserTerm l v)
  | TLimitedRecursion (ParserTerm l v) (ParserTerm l v) (ParserTerm l v)
  deriving (ParserTerm l v -> ParserTerm l v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall l v.
(Eq v, Eq l) =>
ParserTerm l v -> ParserTerm l v -> Bool
/= :: ParserTerm l v -> ParserTerm l v -> Bool
$c/= :: forall l v.
(Eq v, Eq l) =>
ParserTerm l v -> ParserTerm l v -> Bool
== :: ParserTerm l v -> ParserTerm l v -> Bool
$c== :: forall l v.
(Eq v, Eq l) =>
ParserTerm l v -> ParserTerm l v -> Bool
Eq, ParserTerm l v -> ParserTerm l v -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {l} {v}. (Ord v, Ord l) => Eq (ParserTerm l v)
forall l v.
(Ord v, Ord l) =>
ParserTerm l v -> ParserTerm l v -> Bool
forall l v.
(Ord v, Ord l) =>
ParserTerm l v -> ParserTerm l v -> Ordering
forall l v.
(Ord v, Ord l) =>
ParserTerm l v -> ParserTerm l v -> ParserTerm l v
min :: ParserTerm l v -> ParserTerm l v -> ParserTerm l v
$cmin :: forall l v.
(Ord v, Ord l) =>
ParserTerm l v -> ParserTerm l v -> ParserTerm l v
max :: ParserTerm l v -> ParserTerm l v -> ParserTerm l v
$cmax :: forall l v.
(Ord v, Ord l) =>
ParserTerm l v -> ParserTerm l v -> ParserTerm l v
>= :: ParserTerm l v -> ParserTerm l v -> Bool
$c>= :: forall l v.
(Ord v, Ord l) =>
ParserTerm l v -> ParserTerm l v -> Bool
> :: ParserTerm l v -> ParserTerm l v -> Bool
$c> :: forall l v.
(Ord v, Ord l) =>
ParserTerm l v -> ParserTerm l v -> Bool
<= :: ParserTerm l v -> ParserTerm l v -> Bool
$c<= :: forall l v.
(Ord v, Ord l) =>
ParserTerm l v -> ParserTerm l v -> Bool
< :: ParserTerm l v -> ParserTerm l v -> Bool
$c< :: forall l v.
(Ord v, Ord l) =>
ParserTerm l v -> ParserTerm l v -> Bool
compare :: ParserTerm l v -> ParserTerm l v -> Ordering
$ccompare :: forall l v.
(Ord v, Ord l) =>
ParserTerm l v -> ParserTerm l v -> Ordering
Ord, forall a b. a -> ParserTerm l b -> ParserTerm l a
forall a b. (a -> b) -> ParserTerm l a -> ParserTerm l b
forall l a b. a -> ParserTerm l b -> ParserTerm l a
forall l a b. (a -> b) -> ParserTerm l a -> ParserTerm l b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> ParserTerm l b -> ParserTerm l a
$c<$ :: forall l a b. a -> ParserTerm l b -> ParserTerm l a
fmap :: forall a b. (a -> b) -> ParserTerm l a -> ParserTerm l b
$cfmap :: forall l a b. (a -> b) -> ParserTerm l a -> ParserTerm l b
Functor, forall a. ParserTerm l a -> Bool
forall l a. Eq a => a -> ParserTerm l a -> Bool
forall l a. Num a => ParserTerm l a -> a
forall l a. Ord a => ParserTerm l a -> a
forall m a. Monoid m => (a -> m) -> ParserTerm l a -> m
forall l m. Monoid m => ParserTerm l m -> m
forall l a. ParserTerm l a -> Bool
forall l a. ParserTerm l a -> Int
forall l a. ParserTerm l a -> [a]
forall a b. (a -> b -> b) -> b -> ParserTerm l a -> b
forall l a. (a -> a -> a) -> ParserTerm l a -> a
forall l m a. Monoid m => (a -> m) -> ParserTerm l a -> m
forall l b a. (b -> a -> b) -> b -> ParserTerm l a -> b
forall l a b. (a -> b -> b) -> b -> ParserTerm l a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => ParserTerm l a -> a
$cproduct :: forall l a. Num a => ParserTerm l a -> a
sum :: forall a. Num a => ParserTerm l a -> a
$csum :: forall l a. Num a => ParserTerm l a -> a
minimum :: forall a. Ord a => ParserTerm l a -> a
$cminimum :: forall l a. Ord a => ParserTerm l a -> a
maximum :: forall a. Ord a => ParserTerm l a -> a
$cmaximum :: forall l a. Ord a => ParserTerm l a -> a
elem :: forall a. Eq a => a -> ParserTerm l a -> Bool
$celem :: forall l a. Eq a => a -> ParserTerm l a -> Bool
length :: forall a. ParserTerm l a -> Int
$clength :: forall l a. ParserTerm l a -> Int
null :: forall a. ParserTerm l a -> Bool
$cnull :: forall l a. ParserTerm l a -> Bool
toList :: forall a. ParserTerm l a -> [a]
$ctoList :: forall l a. ParserTerm l a -> [a]
foldl1 :: forall a. (a -> a -> a) -> ParserTerm l a -> a
$cfoldl1 :: forall l a. (a -> a -> a) -> ParserTerm l a -> a
foldr1 :: forall a. (a -> a -> a) -> ParserTerm l a -> a
$cfoldr1 :: forall l a. (a -> a -> a) -> ParserTerm l a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> ParserTerm l a -> b
$cfoldl' :: forall l b a. (b -> a -> b) -> b -> ParserTerm l a -> b
foldl :: forall b a. (b -> a -> b) -> b -> ParserTerm l a -> b
$cfoldl :: forall l b a. (b -> a -> b) -> b -> ParserTerm l a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> ParserTerm l a -> b
$cfoldr' :: forall l a b. (a -> b -> b) -> b -> ParserTerm l a -> b
foldr :: forall a b. (a -> b -> b) -> b -> ParserTerm l a -> b
$cfoldr :: forall l a b. (a -> b -> b) -> b -> ParserTerm l a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> ParserTerm l a -> m
$cfoldMap' :: forall l m a. Monoid m => (a -> m) -> ParserTerm l a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> ParserTerm l a -> m
$cfoldMap :: forall l m a. Monoid m => (a -> m) -> ParserTerm l a -> m
fold :: forall m. Monoid m => ParserTerm l m -> m
$cfold :: forall l m. Monoid m => ParserTerm l m -> m
Foldable, forall l. Functor (ParserTerm l)
forall l. Foldable (ParserTerm l)
forall l (m :: * -> *) a.
Monad m =>
ParserTerm l (m a) -> m (ParserTerm l a)
forall l (f :: * -> *) a.
Applicative f =>
ParserTerm l (f a) -> f (ParserTerm l a)
forall l (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ParserTerm l a -> m (ParserTerm l b)
forall l (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ParserTerm l a -> f (ParserTerm l b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ParserTerm l a -> f (ParserTerm l b)
sequence :: forall (m :: * -> *) a.
Monad m =>
ParserTerm l (m a) -> m (ParserTerm l a)
$csequence :: forall l (m :: * -> *) a.
Monad m =>
ParserTerm l (m a) -> m (ParserTerm l a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ParserTerm l a -> m (ParserTerm l b)
$cmapM :: forall l (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ParserTerm l a -> m (ParserTerm l b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
ParserTerm l (f a) -> f (ParserTerm l a)
$csequenceA :: forall l (f :: * -> *) a.
Applicative f =>
ParserTerm l (f a) -> f (ParserTerm l a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ParserTerm l a -> f (ParserTerm l b)
$ctraverse :: forall l (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ParserTerm l a -> f (ParserTerm l b)
Traversable)
makeBaseFunctor ''ParserTerm -- Functorial version ParserTermF
deriveShow1 ''ParserTermF
deriveEq1 ''ParserTermF
deriveOrd1 ''ParserTermF

instance Plated (ParserTerm l v) where
  plate :: Traversal' (ParserTerm l v) (ParserTerm l v)
plate ParserTerm l v -> f (ParserTerm l v)
f = \case
    TITE ParserTerm l v
i ParserTerm l v
t ParserTerm l v
e -> forall l v.
ParserTerm l v
-> ParserTerm l v -> ParserTerm l v -> ParserTerm l v
TITE forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
e
    TPair ParserTerm l v
a ParserTerm l v
b  -> forall l v. ParserTerm l v -> ParserTerm l v -> ParserTerm l v
TPair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
b
    TApp ParserTerm l v
u ParserTerm l v
x   -> forall l v. ParserTerm l v -> ParserTerm l v -> ParserTerm l v
TApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
x
    TLam LamType l
s ParserTerm l v
x   -> forall l v. LamType l -> ParserTerm l v -> ParserTerm l v
TLam LamType l
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
x
    TLeft ParserTerm l v
x    -> forall l v. ParserTerm l v -> ParserTerm l v
TLeft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
x
    TRight ParserTerm l v
x   -> forall l v. ParserTerm l v -> ParserTerm l v
TRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
x
    TTrace ParserTerm l v
x   -> forall l v. ParserTerm l v -> ParserTerm l v
TTrace forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
x
    THash ParserTerm l v
x    -> forall l v. ParserTerm l v -> ParserTerm l v
THash forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
x
    TCheck ParserTerm l v
c ParserTerm l v
x -> forall l v. ParserTerm l v -> ParserTerm l v -> ParserTerm l v
TCheck forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParserTerm l v -> f (ParserTerm l v)
f ParserTerm l v
x
    ParserTerm l v
x          -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ParserTerm l v
x

instance (Show l, Show v) => Show (ParserTerm l v) where
  show :: ParserTerm l v -> String
show ParserTerm l v
x = forall s a. State s a -> s -> a
State.evalState (forall t a. Recursive t => (Base t a -> a) -> t -> a
cata Base (ParserTerm l v) (State Int String) -> State Int String
alg ParserTerm l v
x) Int
0 where
    alg :: (Base (ParserTerm l v)) (State Int String) -> State Int String
    alg :: Base (ParserTerm l v) (State Int String) -> State Int String
alg Base (ParserTerm l v) (State Int String)
ParserTermF l v (State Int String)
TZeroF = String -> State Int String
sindent String
"TZero"
    alg (TPairF State Int String
sl State Int String
sr) = String -> State Int String -> State Int String -> State Int String
indentWithTwoChildren String
"TPair" State Int String
sl State Int String
sr
    alg (TVarF v
v) = String -> State Int String
sindent forall a b. (a -> b) -> a -> b
$ String
"TVar " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show v
v
    alg (TAppF State Int String
sl State Int String
sr) = String -> State Int String -> State Int String -> State Int String
indentWithTwoChildren String
"TApp" State Int String
sl State Int String
sr
    alg (TCheckF State Int String
sl State Int String
sr) = String -> State Int String -> State Int String -> State Int String
indentWithTwoChildren String
"TCheck" State Int String
sl State Int String
sr
    alg (TITEF State Int String
sx State Int String
sy State Int String
sz) = do
      Int
i <- forall s (m :: * -> *). MonadState s m => m s
State.get
      forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
      String
x <- State Int String
sx
      forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
      String
y <- State Int String
sy
      forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
      String
z <- State Int String
sz
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int -> ShowS
indent Int
i String
"TITE\n" forall a. Semigroup a => a -> a -> a
<> String
x forall a. Semigroup a => a -> a -> a
<> String
"\n" forall a. Semigroup a => a -> a -> a
<> String
y forall a. Semigroup a => a -> a -> a
<> String
"\n" forall a. Semigroup a => a -> a -> a
<> String
z
    alg (TLeftF State Int String
l) = String -> State Int String -> State Int String
indentWithOneChild String
"TLeft" State Int String
l
    alg (TRightF State Int String
r) = String -> State Int String -> State Int String
indentWithOneChild String
"TRight" State Int String
r
    alg (TTraceF State Int String
x) = String -> State Int String -> State Int String
indentWithOneChild String
"TTrace" State Int String
x
    alg (THashF State Int String
x) = String -> State Int String -> State Int String
indentWithOneChild String
"THash" State Int String
x
    alg (TChurchF Int
n) = String -> State Int String
sindent forall a b. (a -> b) -> a -> b
$ String
"TChurch " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Int
n
    alg (TLamF LamType l
l State Int String
x) = String -> State Int String -> State Int String
indentWithOneChild (String
"TLam " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show LamType l
l) State Int String
x
    alg (TLimitedRecursionF State Int String
t State Int String
r State Int String
b) = String
-> State Int String
-> State Int String
-> State Int String
-> State Int String
indentWithThreeChildren String
"TLimitedRecursion" State Int String
t  State Int String
r  State Int String
b

-- |Helper function to indent. Usefull for indented Show instances.
indent :: Int -> String -> String
indent :: Int -> ShowS
indent Int
i String
str = forall a. Int -> a -> [a]
replicate Int
i Char
' ' forall a. Semigroup a => a -> a -> a
<> String
str

-- |Indentation with the State Monad.
sindent :: String -> State Int String
sindent :: String -> State Int String
sindent String
str = forall s (m :: * -> *). MonadState s m => m s
State.get forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Int
i -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int -> ShowS
indent Int
i String
str)

-- |One child indentation.
indentWithOneChild :: String -> State Int String -> State Int String
indentWithOneChild :: String -> State Int String -> State Int String
indentWithOneChild String
str State Int String
sx = do
  Int
i <- forall s (m :: * -> *). MonadState s m => m s
State.get
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
  String
x <- State Int String
sx
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int -> ShowS
indent Int
i (String
str forall a. Semigroup a => a -> a -> a
<> String
"\n") forall a. Semigroup a => a -> a -> a
<> String
x

indentWithOneChild' :: String -> State Int String -> State Int String
indentWithOneChild' :: String -> State Int String -> State Int String
indentWithOneChild' String
str State Int String
sx = do
  Int
i <- forall s (m :: * -> *). MonadState s m => m s
State.get
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
  String
x <- State Int String
sx
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ String
str forall a. Semigroup a => a -> a -> a
<> String
" " forall a. Semigroup a => a -> a -> a
<> String
x

indentWithTwoChildren' :: String -> State Int String -> State Int String -> State Int String
indentWithTwoChildren' :: String -> State Int String -> State Int String -> State Int String
indentWithTwoChildren' String
str State Int String
sl State Int String
sr = do
  Int
i <- forall s (m :: * -> *). MonadState s m => m s
State.get
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
  String
l <- State Int String
sl
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
  String
r <- State Int String
sr
  -- pure $ indent i (str <> "\n") <> l <> "\n" <> r
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ String
str forall a. Semigroup a => a -> a -> a
<> String
" " forall a. Semigroup a => a -> a -> a
<> String
l forall a. Semigroup a => a -> a -> a
<> String
"\n" forall a. Semigroup a => a -> a -> a
<> Int -> ShowS
indent (Int
i forall a. Num a => a -> a -> a
+ Int
2) String
r

indentWithChildren' :: String -> [State Int String] -> State Int String
indentWithChildren' :: String -> [State Int String] -> State Int String
indentWithChildren' String
str [State Int String]
l = do
  Int
i <- forall s (m :: * -> *). MonadState s m => m s
State.get
  let doLine :: State Int String -> State Int String
doLine = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Semigroup a => a -> a -> a
<> String
"\n" forall a. Semigroup a => a -> a -> a
<> Int -> ShowS
indent (Int
i forall a. Num a => a -> a -> a
+ Int
2) String
"") forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s (m :: * -> *). MonadState s m => s -> m ()
State.put (Int
i forall a. Num a => a -> a -> a
+ Int
2) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>)
  forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\State Int String
s State Int String
c -> forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State Int String
s forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> State Int String
c) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ String
str forall a. Semigroup a => a -> a -> a
<> String
" ") forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap State Int String -> State Int String
doLine [State Int String]
l

-- |Two children indentation.
indentWithTwoChildren :: String -> State Int String -> State Int String -> State Int String
indentWithTwoChildren :: String -> State Int String -> State Int String -> State Int String
indentWithTwoChildren String
str State Int String
sl State Int String
sr = do
  Int
i <- forall s (m :: * -> *). MonadState s m => m s
State.get
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
  String
l <- State Int String
sl
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
  String
r <- State Int String
sr
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int -> ShowS
indent Int
i (String
str forall a. Semigroup a => a -> a -> a
<> String
"\n") forall a. Semigroup a => a -> a -> a
<> String
l forall a. Semigroup a => a -> a -> a
<> String
"\n" forall a. Semigroup a => a -> a -> a
<> String
r

indentWithThreeChildren :: String -> State Int String -> State Int String -> State Int String -> State Int String
indentWithThreeChildren :: String
-> State Int String
-> State Int String
-> State Int String
-> State Int String
indentWithThreeChildren String
str State Int String
sa State Int String
sb State Int String
sc = do
  Int
i <- forall s (m :: * -> *). MonadState s m => m s
State.get
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
  String
a <- State Int String
sa
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
  String
b <- State Int String
sb
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ Int
i forall a. Num a => a -> a -> a
+ Int
2
  String
c <- State Int String
sc
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Int -> ShowS
indent Int
i (String
str forall a. Semigroup a => a -> a -> a
<> String
"\n") forall a. Semigroup a => a -> a -> a
<> String
a forall a. Semigroup a => a -> a -> a
<> String
"\n" forall a. Semigroup a => a -> a -> a
<> String
b forall a. Semigroup a => a -> a -> a
<> String
"\n" forall a. Semigroup a => a -> a -> a
<> String
c

-- |`dropUntil p xs` drops leading elements until `p $ head xs` is satisfied.
dropUntil :: (a -> Bool) -> [a] -> [a]
dropUntil :: forall a. (a -> Bool) -> [a] -> [a]
dropUntil a -> Bool
_ [] = []
dropUntil a -> Bool
p x :: [a]
x@(a
x1:[a]
_) =
  if a -> Bool
p a
x1 then [a]
x else forall a. (a -> Bool) -> [a] -> [a]
dropUntil a -> Bool
p (forall a. Int -> [a] -> [a]
drop Int
1 [a]
x)

newtype FragIndex = FragIndex { FragIndex -> Int
unFragIndex :: Int } deriving (FragIndex -> FragIndex -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FragIndex -> FragIndex -> Bool
$c/= :: FragIndex -> FragIndex -> Bool
== :: FragIndex -> FragIndex -> Bool
$c== :: FragIndex -> FragIndex -> Bool
Eq, Int -> FragIndex -> ShowS
[FragIndex] -> ShowS
FragIndex -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FragIndex] -> ShowS
$cshowList :: [FragIndex] -> ShowS
show :: FragIndex -> String
$cshow :: FragIndex -> String
showsPrec :: Int -> FragIndex -> ShowS
$cshowsPrec :: Int -> FragIndex -> ShowS
Show, Eq FragIndex
FragIndex -> FragIndex -> Bool
FragIndex -> FragIndex -> Ordering
FragIndex -> FragIndex -> FragIndex
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FragIndex -> FragIndex -> FragIndex
$cmin :: FragIndex -> FragIndex -> FragIndex
max :: FragIndex -> FragIndex -> FragIndex
$cmax :: FragIndex -> FragIndex -> FragIndex
>= :: FragIndex -> FragIndex -> Bool
$c>= :: FragIndex -> FragIndex -> Bool
> :: FragIndex -> FragIndex -> Bool
$c> :: FragIndex -> FragIndex -> Bool
<= :: FragIndex -> FragIndex -> Bool
$c<= :: FragIndex -> FragIndex -> Bool
< :: FragIndex -> FragIndex -> Bool
$c< :: FragIndex -> FragIndex -> Bool
compare :: FragIndex -> FragIndex -> Ordering
$ccompare :: FragIndex -> FragIndex -> Ordering
Ord, Int -> FragIndex
FragIndex -> Int
FragIndex -> [FragIndex]
FragIndex -> FragIndex
FragIndex -> FragIndex -> [FragIndex]
FragIndex -> FragIndex -> FragIndex -> [FragIndex]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: FragIndex -> FragIndex -> FragIndex -> [FragIndex]
$cenumFromThenTo :: FragIndex -> FragIndex -> FragIndex -> [FragIndex]
enumFromTo :: FragIndex -> FragIndex -> [FragIndex]
$cenumFromTo :: FragIndex -> FragIndex -> [FragIndex]
enumFromThen :: FragIndex -> FragIndex -> [FragIndex]
$cenumFromThen :: FragIndex -> FragIndex -> [FragIndex]
enumFrom :: FragIndex -> [FragIndex]
$cenumFrom :: FragIndex -> [FragIndex]
fromEnum :: FragIndex -> Int
$cfromEnum :: FragIndex -> Int
toEnum :: Int -> FragIndex
$ctoEnum :: Int -> FragIndex
pred :: FragIndex -> FragIndex
$cpred :: FragIndex -> FragIndex
succ :: FragIndex -> FragIndex
$csucc :: FragIndex -> FragIndex
Enum, FragIndex -> ()
forall a. (a -> ()) -> NFData a
rnf :: FragIndex -> ()
$crnf :: FragIndex -> ()
NFData, forall x. Rep FragIndex x -> FragIndex
forall x. FragIndex -> Rep FragIndex x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep FragIndex x -> FragIndex
$cfrom :: forall x. FragIndex -> Rep FragIndex x
Generic)

data FragExpr a
  = ZeroFrag
  | PairFrag (FragExpr a) (FragExpr a)
  | EnvFrag
  | SetEnvFrag (FragExpr a)
  | DeferFrag FragIndex
  | AbortFrag
  | GateFrag (FragExpr a) (FragExpr a)
  | LeftFrag (FragExpr a)
  | RightFrag (FragExpr a)
  | TraceFrag
  | AuxFrag a
  deriving (FragExpr a -> FragExpr a -> Bool
forall a. Eq a => FragExpr a -> FragExpr a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FragExpr a -> FragExpr a -> Bool
$c/= :: forall a. Eq a => FragExpr a -> FragExpr a -> Bool
== :: FragExpr a -> FragExpr a -> Bool
$c== :: forall a. Eq a => FragExpr a -> FragExpr a -> Bool
Eq, FragExpr a -> FragExpr a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (FragExpr a)
forall a. Ord a => FragExpr a -> FragExpr a -> Bool
forall a. Ord a => FragExpr a -> FragExpr a -> Ordering
forall a. Ord a => FragExpr a -> FragExpr a -> FragExpr a
min :: FragExpr a -> FragExpr a -> FragExpr a
$cmin :: forall a. Ord a => FragExpr a -> FragExpr a -> FragExpr a
max :: FragExpr a -> FragExpr a -> FragExpr a
$cmax :: forall a. Ord a => FragExpr a -> FragExpr a -> FragExpr a
>= :: FragExpr a -> FragExpr a -> Bool
$c>= :: forall a. Ord a => FragExpr a -> FragExpr a -> Bool
> :: FragExpr a -> FragExpr a -> Bool
$c> :: forall a. Ord a => FragExpr a -> FragExpr a -> Bool
<= :: FragExpr a -> FragExpr a -> Bool
$c<= :: forall a. Ord a => FragExpr a -> FragExpr a -> Bool
< :: FragExpr a -> FragExpr a -> Bool
$c< :: forall a. Ord a => FragExpr a -> FragExpr a -> Bool
compare :: FragExpr a -> FragExpr a -> Ordering
$ccompare :: forall a. Ord a => FragExpr a -> FragExpr a -> Ordering
Ord, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (FragExpr a) x -> FragExpr a
forall a x. FragExpr a -> Rep (FragExpr a) x
$cto :: forall a x. Rep (FragExpr a) x -> FragExpr a
$cfrom :: forall a x. FragExpr a -> Rep (FragExpr a) x
Generic, forall a. NFData a => FragExpr a -> ()
forall a. (a -> ()) -> NFData a
rnf :: FragExpr a -> ()
$crnf :: forall a. NFData a => FragExpr a -> ()
NFData)
makeBaseFunctor ''FragExpr -- Functorial version FragExprF.
deriveShow1 ''FragExprF
deriveEq1 ''FragExprF

instance Plated (FragExpr a) where
  plate :: Traversal' (FragExpr a) (FragExpr a)
plate FragExpr a -> f (FragExpr a)
f = \case
    PairFrag FragExpr a
a FragExpr a
b -> forall a. FragExpr a -> FragExpr a -> FragExpr a
PairFrag forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FragExpr a -> f (FragExpr a)
f FragExpr a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FragExpr a -> f (FragExpr a)
f FragExpr a
b
    SetEnvFrag FragExpr a
x -> forall a. FragExpr a -> FragExpr a
SetEnvFrag forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FragExpr a -> f (FragExpr a)
f FragExpr a
x
    GateFrag FragExpr a
l FragExpr a
r -> forall a. FragExpr a -> FragExpr a -> FragExpr a
GateFrag forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FragExpr a -> f (FragExpr a)
f FragExpr a
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FragExpr a -> f (FragExpr a)
f FragExpr a
r
    LeftFrag FragExpr a
x   -> forall a. FragExpr a -> FragExpr a
LeftFrag forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FragExpr a -> f (FragExpr a)
f FragExpr a
x
    RightFrag FragExpr a
x  -> forall a. FragExpr a -> FragExpr a
RightFrag forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FragExpr a -> f (FragExpr a)
f FragExpr a
x
    FragExpr a
x            -> forall (f :: * -> *) a. Applicative f => a -> f a
pure FragExpr a
x

showFragAlg :: Show a => (Base (FragExpr a)) (State Int String) -> State Int String
showFragAlg :: forall a.
Show a =>
Base (FragExpr a) (State Int String) -> State Int String
showFragAlg = \case
      Base (FragExpr a) (State Int String)
FragExprF a (State Int String)
ZeroFragF         -> String -> State Int String
sindent String
"ZeroFrag"
      (PairFragF State Int String
sl State Int String
sr) -> String -> State Int String -> State Int String -> State Int String
indentWithTwoChildren String
"PairFrag" State Int String
sl State Int String
sr
      Base (FragExpr a) (State Int String)
FragExprF a (State Int String)
EnvFragF          -> String -> State Int String
sindent String
"EnvFrag"
      (SetEnvFragF State Int String
sx)  -> String -> State Int String -> State Int String
indentWithOneChild String
"SetEnvFrag" State Int String
sx
      (DeferFragF FragIndex
i)    -> String -> State Int String
sindent forall a b. (a -> b) -> a -> b
$ String
"DeferFrag " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show FragIndex
i
      Base (FragExpr a) (State Int String)
FragExprF a (State Int String)
AbortFragF        -> String -> State Int String
sindent String
"AbortFrag"
      (GateFragF State Int String
sx State Int String
sy) -> String -> State Int String -> State Int String -> State Int String
indentWithTwoChildren String
"GateFrag" State Int String
sx State Int String
sy
      (LeftFragF State Int String
sl)    -> String -> State Int String -> State Int String
indentWithOneChild String
"LeftFrag" State Int String
sl
      (RightFragF State Int String
sr)   -> String -> State Int String -> State Int String
indentWithOneChild String
"RightFrag" State Int String
sr
      Base (FragExpr a) (State Int String)
FragExprF a (State Int String)
TraceFragF        -> String -> State Int String
sindent String
"TraceFrag"
      (AuxFragF a
x)      -> String -> State Int String
sindent forall a b. (a -> b) -> a -> b
$ String
"AuxFrag " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show a
x

instance Show a => Show (FragExpr a) where
  show :: FragExpr a -> String
show FragExpr a
fexp = forall s a. State s a -> s -> a
State.evalState (forall t a. Recursive t => (Base t a -> a) -> t -> a
cata forall a.
Show a =>
Base (FragExpr a) (State Int String) -> State Int String
showFragAlg FragExpr a
fexp) Int
0

newtype EIndex = EIndex { EIndex -> Int
unIndex :: Int } deriving (EIndex -> EIndex -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EIndex -> EIndex -> Bool
$c/= :: EIndex -> EIndex -> Bool
== :: EIndex -> EIndex -> Bool
$c== :: EIndex -> EIndex -> Bool
Eq, Int -> EIndex -> ShowS
[EIndex] -> ShowS
EIndex -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EIndex] -> ShowS
$cshowList :: [EIndex] -> ShowS
show :: EIndex -> String
$cshow :: EIndex -> String
showsPrec :: Int -> EIndex -> ShowS
$cshowsPrec :: Int -> EIndex -> ShowS
Show, Eq EIndex
EIndex -> EIndex -> Bool
EIndex -> EIndex -> Ordering
EIndex -> EIndex -> EIndex
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: EIndex -> EIndex -> EIndex
$cmin :: EIndex -> EIndex -> EIndex
max :: EIndex -> EIndex -> EIndex
$cmax :: EIndex -> EIndex -> EIndex
>= :: EIndex -> EIndex -> Bool
$c>= :: EIndex -> EIndex -> Bool
> :: EIndex -> EIndex -> Bool
$c> :: EIndex -> EIndex -> Bool
<= :: EIndex -> EIndex -> Bool
$c<= :: EIndex -> EIndex -> Bool
< :: EIndex -> EIndex -> Bool
$c< :: EIndex -> EIndex -> Bool
compare :: EIndex -> EIndex -> Ordering
$ccompare :: EIndex -> EIndex -> Ordering
Ord)

newtype UnsizedRecursionToken = UnsizedRecursionToken { UnsizedRecursionToken -> Int
unUnsizedRecursionToken :: Int } deriving (UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
$c/= :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
== :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
$c== :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
Eq, Eq UnsizedRecursionToken
UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
UnsizedRecursionToken -> UnsizedRecursionToken -> Ordering
UnsizedRecursionToken
-> UnsizedRecursionToken -> UnsizedRecursionToken
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: UnsizedRecursionToken
-> UnsizedRecursionToken -> UnsizedRecursionToken
$cmin :: UnsizedRecursionToken
-> UnsizedRecursionToken -> UnsizedRecursionToken
max :: UnsizedRecursionToken
-> UnsizedRecursionToken -> UnsizedRecursionToken
$cmax :: UnsizedRecursionToken
-> UnsizedRecursionToken -> UnsizedRecursionToken
>= :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
$c>= :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
> :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
$c> :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
<= :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
$c<= :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
< :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
$c< :: UnsizedRecursionToken -> UnsizedRecursionToken -> Bool
compare :: UnsizedRecursionToken -> UnsizedRecursionToken -> Ordering
$ccompare :: UnsizedRecursionToken -> UnsizedRecursionToken -> Ordering
Ord, Int -> UnsizedRecursionToken -> ShowS
[UnsizedRecursionToken] -> ShowS
UnsizedRecursionToken -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnsizedRecursionToken] -> ShowS
$cshowList :: [UnsizedRecursionToken] -> ShowS
show :: UnsizedRecursionToken -> String
$cshow :: UnsizedRecursionToken -> String
showsPrec :: Int -> UnsizedRecursionToken -> ShowS
$cshowsPrec :: Int -> UnsizedRecursionToken -> ShowS
Show, Int -> UnsizedRecursionToken
UnsizedRecursionToken -> Int
UnsizedRecursionToken -> [UnsizedRecursionToken]
UnsizedRecursionToken -> UnsizedRecursionToken
UnsizedRecursionToken
-> UnsizedRecursionToken -> [UnsizedRecursionToken]
UnsizedRecursionToken
-> UnsizedRecursionToken
-> UnsizedRecursionToken
-> [UnsizedRecursionToken]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: UnsizedRecursionToken
-> UnsizedRecursionToken
-> UnsizedRecursionToken
-> [UnsizedRecursionToken]
$cenumFromThenTo :: UnsizedRecursionToken
-> UnsizedRecursionToken
-> UnsizedRecursionToken
-> [UnsizedRecursionToken]
enumFromTo :: UnsizedRecursionToken
-> UnsizedRecursionToken -> [UnsizedRecursionToken]
$cenumFromTo :: UnsizedRecursionToken
-> UnsizedRecursionToken -> [UnsizedRecursionToken]
enumFromThen :: UnsizedRecursionToken
-> UnsizedRecursionToken -> [UnsizedRecursionToken]
$cenumFromThen :: UnsizedRecursionToken
-> UnsizedRecursionToken -> [UnsizedRecursionToken]
enumFrom :: UnsizedRecursionToken -> [UnsizedRecursionToken]
$cenumFrom :: UnsizedRecursionToken -> [UnsizedRecursionToken]
fromEnum :: UnsizedRecursionToken -> Int
$cfromEnum :: UnsizedRecursionToken -> Int
toEnum :: Int -> UnsizedRecursionToken
$ctoEnum :: Int -> UnsizedRecursionToken
pred :: UnsizedRecursionToken -> UnsizedRecursionToken
$cpred :: UnsizedRecursionToken -> UnsizedRecursionToken
succ :: UnsizedRecursionToken -> UnsizedRecursionToken
$csucc :: UnsizedRecursionToken -> UnsizedRecursionToken
Enum, UnsizedRecursionToken -> ()
forall a. (a -> ()) -> NFData a
rnf :: UnsizedRecursionToken -> ()
$crnf :: UnsizedRecursionToken -> ()
NFData, forall x. Rep UnsizedRecursionToken x -> UnsizedRecursionToken
forall x. UnsizedRecursionToken -> Rep UnsizedRecursionToken x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep UnsizedRecursionToken x -> UnsizedRecursionToken
$cfrom :: forall x. UnsizedRecursionToken -> Rep UnsizedRecursionToken x
Generic)

data RecursionSimulationPieces a
  = NestedSetEnvs UnsizedRecursionToken
  | SizingWrapper UnsizedRecursionToken a
  deriving (RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
forall a.
Eq a =>
RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
$c/= :: forall a.
Eq a =>
RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
== :: RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
$c== :: forall a.
Eq a =>
RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
Eq, RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
RecursionSimulationPieces a
-> RecursionSimulationPieces a -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (RecursionSimulationPieces a)
forall a.
Ord a =>
RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
forall a.
Ord a =>
RecursionSimulationPieces a
-> RecursionSimulationPieces a -> Ordering
forall a.
Ord a =>
RecursionSimulationPieces a
-> RecursionSimulationPieces a -> RecursionSimulationPieces a
min :: RecursionSimulationPieces a
-> RecursionSimulationPieces a -> RecursionSimulationPieces a
$cmin :: forall a.
Ord a =>
RecursionSimulationPieces a
-> RecursionSimulationPieces a -> RecursionSimulationPieces a
max :: RecursionSimulationPieces a
-> RecursionSimulationPieces a -> RecursionSimulationPieces a
$cmax :: forall a.
Ord a =>
RecursionSimulationPieces a
-> RecursionSimulationPieces a -> RecursionSimulationPieces a
>= :: RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
$c>= :: forall a.
Ord a =>
RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
> :: RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
$c> :: forall a.
Ord a =>
RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
<= :: RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
$c<= :: forall a.
Ord a =>
RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
< :: RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
$c< :: forall a.
Ord a =>
RecursionSimulationPieces a -> RecursionSimulationPieces a -> Bool
compare :: RecursionSimulationPieces a
-> RecursionSimulationPieces a -> Ordering
$ccompare :: forall a.
Ord a =>
RecursionSimulationPieces a
-> RecursionSimulationPieces a -> Ordering
Ord, Int -> RecursionSimulationPieces a -> ShowS
forall a. Show a => Int -> RecursionSimulationPieces a -> ShowS
forall a. Show a => [RecursionSimulationPieces a] -> ShowS
forall a. Show a => RecursionSimulationPieces a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RecursionSimulationPieces a] -> ShowS
$cshowList :: forall a. Show a => [RecursionSimulationPieces a] -> ShowS
show :: RecursionSimulationPieces a -> String
$cshow :: forall a. Show a => RecursionSimulationPieces a -> String
showsPrec :: Int -> RecursionSimulationPieces a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> RecursionSimulationPieces a -> ShowS
Show, forall a. NFData a => RecursionSimulationPieces a -> ()
forall a. (a -> ()) -> NFData a
rnf :: RecursionSimulationPieces a -> ()
$crnf :: forall a. NFData a => RecursionSimulationPieces a -> ()
NFData, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x.
Rep (RecursionSimulationPieces a) x -> RecursionSimulationPieces a
forall a x.
RecursionSimulationPieces a -> Rep (RecursionSimulationPieces a) x
$cto :: forall a x.
Rep (RecursionSimulationPieces a) x -> RecursionSimulationPieces a
$cfrom :: forall a x.
RecursionSimulationPieces a -> Rep (RecursionSimulationPieces a) x
Generic, forall a b.
a -> RecursionSimulationPieces b -> RecursionSimulationPieces a
forall a b.
(a -> b)
-> RecursionSimulationPieces a -> RecursionSimulationPieces b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b.
a -> RecursionSimulationPieces b -> RecursionSimulationPieces a
$c<$ :: forall a b.
a -> RecursionSimulationPieces b -> RecursionSimulationPieces a
fmap :: forall a b.
(a -> b)
-> RecursionSimulationPieces a -> RecursionSimulationPieces b
$cfmap :: forall a b.
(a -> b)
-> RecursionSimulationPieces a -> RecursionSimulationPieces b
Functor)

data LocTag
  = DummyLoc
  | Loc Int Int
  deriving (LocTag -> LocTag -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LocTag -> LocTag -> Bool
$c/= :: LocTag -> LocTag -> Bool
== :: LocTag -> LocTag -> Bool
$c== :: LocTag -> LocTag -> Bool
Eq, Int -> LocTag -> ShowS
[LocTag] -> ShowS
LocTag -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LocTag] -> ShowS
$cshowList :: [LocTag] -> ShowS
show :: LocTag -> String
$cshow :: LocTag -> String
showsPrec :: Int -> LocTag -> ShowS
$cshowsPrec :: Int -> LocTag -> ShowS
Show, Eq LocTag
LocTag -> LocTag -> Bool
LocTag -> LocTag -> Ordering
LocTag -> LocTag -> LocTag
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: LocTag -> LocTag -> LocTag
$cmin :: LocTag -> LocTag -> LocTag
max :: LocTag -> LocTag -> LocTag
$cmax :: LocTag -> LocTag -> LocTag
>= :: LocTag -> LocTag -> Bool
$c>= :: LocTag -> LocTag -> Bool
> :: LocTag -> LocTag -> Bool
$c> :: LocTag -> LocTag -> Bool
<= :: LocTag -> LocTag -> Bool
$c<= :: LocTag -> LocTag -> Bool
< :: LocTag -> LocTag -> Bool
$c< :: LocTag -> LocTag -> Bool
compare :: LocTag -> LocTag -> Ordering
$ccompare :: LocTag -> LocTag -> Ordering
Ord, forall x. Rep LocTag x -> LocTag
forall x. LocTag -> Rep LocTag x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep LocTag x -> LocTag
$cfrom :: forall x. LocTag -> Rep LocTag x
Generic, LocTag -> ()
forall a. (a -> ()) -> NFData a
rnf :: LocTag -> ()
$crnf :: LocTag -> ()
NFData)

newtype FragExprUR =
  FragExprUR { FragExprUR
-> Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag
unFragExprUR :: Cofree (FragExprF (RecursionSimulationPieces FragExprUR))
                                      LocTag
             }
  deriving (FragExprUR -> FragExprUR -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FragExprUR -> FragExprUR -> Bool
$c/= :: FragExprUR -> FragExprUR -> Bool
== :: FragExprUR -> FragExprUR -> Bool
$c== :: FragExprUR -> FragExprUR -> Bool
Eq, Int -> FragExprUR -> ShowS
[FragExprUR] -> ShowS
FragExprUR -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FragExprUR] -> ShowS
$cshowList :: [FragExprUR] -> ShowS
show :: FragExprUR -> String
$cshow :: FragExprUR -> String
showsPrec :: Int -> FragExprUR -> ShowS
$cshowsPrec :: Int -> FragExprUR -> ShowS
Show, forall x. Rep FragExprUR x -> FragExprUR
forall x. FragExprUR -> Rep FragExprUR x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep FragExprUR x -> FragExprUR
$cfrom :: forall x. FragExprUR -> Rep FragExprUR x
Generic)
instance NFData FragExprUR where
  -- rnf (FragExprUR (a :< x)) = seq (rnf a) $ rnf x
  rnf :: FragExprUR -> ()
rnf (FragExprUR (LocTag
a :< !FragExprF
  (RecursionSimulationPieces FragExprUR)
  (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag)
x)) = seq :: forall a b. a -> b -> b
seq (forall a. NFData a => a -> ()
rnf LocTag
a) () -- TODO fix if we ever care about proper NFData

type RecursionPieceFrag = RecursionSimulationPieces FragExprUR

type Term1 = Cofree (ParserTermF String String) LocTag
type Term2 = Cofree (ParserTermF () Int) LocTag

-- |Term3 :: Map FragIndex (FragExpr BreakExtras) -> Term3
newtype Term3 = Term3 (Map FragIndex FragExprUR) deriving (Term3 -> Term3 -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term3 -> Term3 -> Bool
$c/= :: Term3 -> Term3 -> Bool
== :: Term3 -> Term3 -> Bool
$c== :: Term3 -> Term3 -> Bool
Eq, Int -> Term3 -> ShowS
[Term3] -> ShowS
Term3 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term3] -> ShowS
$cshowList :: [Term3] -> ShowS
show :: Term3 -> String
$cshow :: Term3 -> String
showsPrec :: Int -> Term3 -> ShowS
$cshowsPrec :: Int -> Term3 -> ShowS
Show, forall x. Rep Term3 x -> Term3
forall x. Term3 -> Rep Term3 x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Term3 x -> Term3
$cfrom :: forall x. Term3 -> Rep Term3 x
Generic, Term3 -> ()
forall a. (a -> ()) -> NFData a
rnf :: Term3 -> ()
$crnf :: Term3 -> ()
NFData)
newtype Term4 = Term4 (Map FragIndex (Cofree (FragExprF Void) LocTag)) deriving (Term4 -> Term4 -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term4 -> Term4 -> Bool
$c/= :: Term4 -> Term4 -> Bool
== :: Term4 -> Term4 -> Bool
$c== :: Term4 -> Term4 -> Bool
Eq, Int -> Term4 -> ShowS
[Term4] -> ShowS
Term4 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term4] -> ShowS
$cshowList :: [Term4] -> ShowS
show :: Term4 -> String
$cshow :: Term4 -> String
showsPrec :: Int -> Term4 -> ShowS
$cshowsPrec :: Int -> Term4 -> ShowS
Show)

type BreakState a b = State (b, FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))

type BreakState' a b = BreakState a b (Cofree (FragExprF a) LocTag)

type IndExpr = ExprA EIndex

instance MonoidEndoFolder IExpr where
  monoidFold :: forall m. Monoid m => (IExpr -> m) -> IExpr -> m
monoidFold IExpr -> m
f IExpr
Zero = IExpr -> m
f IExpr
Zero
  monoidFold IExpr -> m
f (Pair IExpr
a IExpr
b) = forall a. Monoid a => [a] -> a
mconcat [IExpr -> m
f (IExpr -> IExpr -> IExpr
Pair IExpr
a IExpr
b), forall a m. (MonoidEndoFolder a, Monoid m) => (a -> m) -> a -> m
monoidFold IExpr -> m
f IExpr
a, forall a m. (MonoidEndoFolder a, Monoid m) => (a -> m) -> a -> m
monoidFold IExpr -> m
f IExpr
b]
  monoidFold IExpr -> m
f IExpr
Env = IExpr -> m
f IExpr
Env
  monoidFold IExpr -> m
f (SetEnv IExpr
x) = forall a. Monoid a => [a] -> a
mconcat [IExpr -> m
f (IExpr -> IExpr
SetEnv IExpr
x), forall a m. (MonoidEndoFolder a, Monoid m) => (a -> m) -> a -> m
monoidFold IExpr -> m
f IExpr
x]
  monoidFold IExpr -> m
f (Defer IExpr
x) = forall a. Monoid a => [a] -> a
mconcat [IExpr -> m
f (IExpr -> IExpr
Defer IExpr
x), forall a m. (MonoidEndoFolder a, Monoid m) => (a -> m) -> a -> m
monoidFold IExpr -> m
f IExpr
x]
  monoidFold IExpr -> m
f (Gate IExpr
l IExpr
r) = forall a. Monoid a => [a] -> a
mconcat [IExpr -> m
f (IExpr -> IExpr -> IExpr
Gate IExpr
l IExpr
r), forall a m. (MonoidEndoFolder a, Monoid m) => (a -> m) -> a -> m
monoidFold IExpr -> m
f IExpr
l, forall a m. (MonoidEndoFolder a, Monoid m) => (a -> m) -> a -> m
monoidFold IExpr -> m
f IExpr
r]
  monoidFold IExpr -> m
f (PLeft IExpr
x) = forall a. Monoid a => [a] -> a
mconcat [IExpr -> m
f (IExpr -> IExpr
PLeft IExpr
x), forall a m. (MonoidEndoFolder a, Monoid m) => (a -> m) -> a -> m
monoidFold IExpr -> m
f IExpr
x]
  monoidFold IExpr -> m
f (PRight IExpr
x) = forall a. Monoid a => [a] -> a
mconcat [IExpr -> m
f (IExpr -> IExpr
PRight IExpr
x), forall a m. (MonoidEndoFolder a, Monoid m) => (a -> m) -> a -> m
monoidFold IExpr -> m
f IExpr
x]
  monoidFold IExpr -> m
f IExpr
Trace = IExpr -> m
f IExpr
Trace

instance NFData IExpr where
  rnf :: IExpr -> ()
rnf IExpr
Zero         = ()
  rnf (Pair IExpr
e1 IExpr
e2) = forall a. NFData a => a -> ()
rnf IExpr
e1 seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf IExpr
e2
  rnf IExpr
Env          = ()
  rnf (SetEnv  IExpr
e)  = forall a. NFData a => a -> ()
rnf IExpr
e
  rnf (Defer   IExpr
e)  = forall a. NFData a => a -> ()
rnf IExpr
e
  rnf (Gate IExpr
l IExpr
r)   = forall a. NFData a => a -> ()
rnf IExpr
l seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf IExpr
r
  rnf (PLeft   IExpr
e)  = forall a. NFData a => a -> ()
rnf IExpr
e
  rnf (PRight  IExpr
e)  = forall a. NFData a => a -> ()
rnf IExpr
e
  rnf IExpr
Trace        = ()

data RunTimeError
  = AbortRunTime IExpr
  | SetEnvError IExpr
  | GenericRunTimeError String IExpr
  | ResultConversionError String
  deriving (RunTimeError -> RunTimeError -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RunTimeError -> RunTimeError -> Bool
$c/= :: RunTimeError -> RunTimeError -> Bool
== :: RunTimeError -> RunTimeError -> Bool
$c== :: RunTimeError -> RunTimeError -> Bool
Eq, Eq RunTimeError
RunTimeError -> RunTimeError -> Bool
RunTimeError -> RunTimeError -> Ordering
RunTimeError -> RunTimeError -> RunTimeError
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RunTimeError -> RunTimeError -> RunTimeError
$cmin :: RunTimeError -> RunTimeError -> RunTimeError
max :: RunTimeError -> RunTimeError -> RunTimeError
$cmax :: RunTimeError -> RunTimeError -> RunTimeError
>= :: RunTimeError -> RunTimeError -> Bool
$c>= :: RunTimeError -> RunTimeError -> Bool
> :: RunTimeError -> RunTimeError -> Bool
$c> :: RunTimeError -> RunTimeError -> Bool
<= :: RunTimeError -> RunTimeError -> Bool
$c<= :: RunTimeError -> RunTimeError -> Bool
< :: RunTimeError -> RunTimeError -> Bool
$c< :: RunTimeError -> RunTimeError -> Bool
compare :: RunTimeError -> RunTimeError -> Ordering
$ccompare :: RunTimeError -> RunTimeError -> Ordering
Ord)

instance Show RunTimeError where
  show :: RunTimeError -> String
show (AbortRunTime IExpr
a) = String
"Abort: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (IExpr -> String
g2s IExpr
a)
  show (SetEnvError IExpr
e) = String
"Can't SetEnv: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show IExpr
e
  show (GenericRunTimeError String
s IExpr
i) = String
"Generic Runtime Error: " forall a. Semigroup a => a -> a -> a
<> String
s forall a. Semigroup a => a -> a -> a
<> String
" -- " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show IExpr
i
  show (ResultConversionError String
s) = String
"Couldn't convert runtime result to IExpr: " forall a. Semigroup a => a -> a -> a
<> String
s

-- type RunResult = ExceptT RunTimeError IO

class TelomareLike a where
  fromTelomare :: IExpr -> a
  toTelomare :: a -> Maybe IExpr

class TelomareLike a => AbstractRunTime a where
  eval :: a -> a

rootFrag :: Map FragIndex a -> a
rootFrag :: forall a. Map FragIndex a -> a
rootFrag = (forall k a. Ord k => Map k a -> k -> a
Map.! Int -> FragIndex
FragIndex Int
0)

-- TODO get rid of these and use bidirectional pattern matching
zero :: IExpr
zero :: IExpr
zero = IExpr
Zero
pair :: IExpr -> IExpr -> IExpr
pair :: IExpr -> IExpr -> IExpr
pair = IExpr -> IExpr -> IExpr
Pair
var :: IExpr
var :: IExpr
var = IExpr
Env
env :: IExpr
env :: IExpr
env = IExpr
Env
twiddle :: IExpr -> IExpr
twiddle :: IExpr -> IExpr
twiddle IExpr
x = IExpr -> IExpr
setenv (IExpr -> IExpr -> IExpr
pair (IExpr -> IExpr
defer (IExpr -> IExpr -> IExpr
pair (IExpr -> IExpr
pleft (IExpr -> IExpr
pright IExpr
env)) (IExpr -> IExpr -> IExpr
pair (IExpr -> IExpr
pleft IExpr
env) (IExpr -> IExpr
pright (IExpr -> IExpr
pright IExpr
env))))) IExpr
x)
app :: IExpr -> IExpr -> IExpr
app :: IExpr -> IExpr -> IExpr
app IExpr
c IExpr
i = IExpr -> IExpr
setenv (IExpr -> IExpr
setenv (IExpr -> IExpr -> IExpr
pair (IExpr -> IExpr
defer (IExpr -> IExpr -> IExpr
pair (IExpr -> IExpr
pleft (IExpr -> IExpr
pright IExpr
env)) (IExpr -> IExpr -> IExpr
pair (IExpr -> IExpr
pleft IExpr
env) (IExpr -> IExpr
pright (IExpr -> IExpr
pright IExpr
env)))))
                          (IExpr -> IExpr -> IExpr
pair IExpr
i IExpr
c)))
pleft :: IExpr -> IExpr
pleft :: IExpr -> IExpr
pleft = IExpr -> IExpr
PLeft
pright :: IExpr -> IExpr
pright :: IExpr -> IExpr
pright = IExpr -> IExpr
PRight
setenv :: IExpr -> IExpr
setenv :: IExpr -> IExpr
setenv = IExpr -> IExpr
SetEnv
defer :: IExpr -> IExpr
defer :: IExpr -> IExpr
defer = IExpr -> IExpr
Defer
lam :: IExpr -> IExpr
lam :: IExpr -> IExpr
lam IExpr
x = IExpr -> IExpr -> IExpr
pair (IExpr -> IExpr
defer IExpr
x) IExpr
env
-- a form of lambda that does not pull in a surrounding environment
completeLam :: IExpr -> IExpr
completeLam :: IExpr -> IExpr
completeLam IExpr
x = IExpr -> IExpr -> IExpr
pair (IExpr -> IExpr
defer IExpr
x) IExpr
zero
ite :: IExpr -> IExpr -> IExpr -> IExpr
ite :: IExpr -> IExpr -> IExpr -> IExpr
ite IExpr
i IExpr
t IExpr
e = IExpr -> IExpr
setenv (IExpr -> IExpr -> IExpr
pair (IExpr -> IExpr -> IExpr
Gate IExpr
e IExpr
t) IExpr
i)
varN :: Int -> IExpr
varN :: Int -> IExpr
varN Int
n = if Int
n forall a. Ord a => a -> a -> Bool
< Int
0
  then forall a. HasCallStack => String -> a
error (String
"varN invalid debruijin index " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Int
n)
  else IExpr -> IExpr
pleft (forall a. (a -> a) -> a -> [a]
iterate IExpr -> IExpr
pright IExpr
env forall a. [a] -> Int -> a
!! Int
n)

varNF :: Int -> FragExpr a
varNF :: forall a. Int -> FragExpr a
varNF Int
n = if Int
n forall a. Ord a => a -> a -> Bool
< Int
0
  then forall a. HasCallStack => String -> a
error (String
"varN invalid debruijin index " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Int
n)
  else forall a. FragExpr a -> FragExpr a
LeftFrag (forall a. (a -> a) -> a -> [a]
iterate forall a. FragExpr a -> FragExpr a
RightFrag forall a. FragExpr a
EnvFrag forall a. [a] -> Int -> a
!! Int
n)

-- make sure these patterns are in exact correspondence with the shortcut functions above
pattern FirstArg :: IExpr
pattern $bFirstArg :: IExpr
$mFirstArg :: forall {r}. IExpr -> ((# #) -> r) -> ((# #) -> r) -> r
FirstArg = PLeft Env
pattern SecondArg :: IExpr
pattern $bSecondArg :: IExpr
$mSecondArg :: forall {r}. IExpr -> ((# #) -> r) -> ((# #) -> r) -> r
SecondArg = PLeft (PRight Env)
pattern ThirdArg :: IExpr
pattern $mThirdArg :: forall {r}. IExpr -> ((# #) -> r) -> ((# #) -> r) -> r
ThirdArg <- PLeft (PRight (PRight Env))
pattern FourthArg :: IExpr
pattern $mFourthArg :: forall {r}. IExpr -> ((# #) -> r) -> ((# #) -> r) -> r
FourthArg <- PLeft (PRight (PRight (PRight Env)))
pattern Lam :: IExpr -> IExpr
pattern $bLam :: IExpr -> IExpr
$mLam :: forall {r}. IExpr -> (IExpr -> r) -> ((# #) -> r) -> r
Lam x = Pair (Defer x) Env
pattern App :: IExpr -> IExpr -> IExpr
pattern $bApp :: IExpr -> IExpr -> IExpr
$mApp :: forall {r}. IExpr -> (IExpr -> IExpr -> r) -> ((# #) -> r) -> r
App c i = SetEnv (SetEnv (Pair (Defer (Pair (PLeft (PRight Env)) (Pair (PLeft Env) (PRight (PRight Env)))))
                         (Pair i c)))
pattern TwoArgFun :: IExpr -> IExpr
pattern $mTwoArgFun :: forall {r}. IExpr -> (IExpr -> r) -> ((# #) -> r) -> r
TwoArgFun c <- Pair (Defer (Pair (Defer c) Env)) Env
pattern ITE :: IExpr -> IExpr -> IExpr -> IExpr
pattern $bITE :: IExpr -> IExpr -> IExpr -> IExpr
$mITE :: forall {r}.
IExpr -> (IExpr -> IExpr -> IExpr -> r) -> ((# #) -> r) -> r
ITE i t e = SetEnv (Pair (Gate e t) i)
pattern EasyTrace :: IExpr -> IExpr
pattern $bEasyTrace :: IExpr -> IExpr
$mEasyTrace :: forall {r}. IExpr -> (IExpr -> r) -> ((# #) -> r) -> r
EasyTrace x = SetEnv (Pair (Defer Trace) x)

countApps :: Int -> IExpr -> Maybe Int
countApps :: Int -> IExpr -> Maybe Int
countApps Int
x IExpr
FirstArg          = forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
x
countApps Int
x (App IExpr
SecondArg IExpr
c) = Int -> IExpr -> Maybe Int
countApps (Int
x forall a. Num a => a -> a -> a
+ Int
1) IExpr
c
countApps Int
_ IExpr
_                 = forall a. Maybe a
Nothing

pattern ChurchNum :: Int -> IExpr
pattern $mChurchNum :: forall {r}. IExpr -> (Int -> r) -> ((# #) -> r) -> r
ChurchNum x <- TwoArgFun (countApps 0 -> Just x)

pattern ToChurch :: IExpr
pattern $mToChurch :: forall {r}. IExpr -> ((# #) -> r) -> ((# #) -> r) -> r
ToChurch <-
  Lam
    (App
      (App
        FirstArg
        (Lam (Lam (Lam (Lam
          (ITE
            ThirdArg
            (App
              SecondArg
              (App
                (App
                  (App
                    FourthArg
                    (PLeft ThirdArg)
                  )
                  SecondArg
                )
                FirstArg
              )
            )
            FirstArg
          )
        ))))
      )
      (Lam (Lam (Lam FirstArg)))
    )

deferF :: Show a => BreakState' a b -> BreakState' a b
deferF :: forall a b. Show a => BreakState' a b -> BreakState' a b
deferF BreakState' a b
x = do
  bx :: Cofree (FragExprF a) LocTag
bx@(LocTag
anno :< FragExprF a (Cofree (FragExprF a) LocTag)
_) <- BreakState' a b
x
  (b
uri, fi :: FragIndex
fi@(FragIndex Int
i), Map FragIndex (Cofree (FragExprF a) LocTag)
fragMap) <- forall s (m :: * -> *). MonadState s m => m s
State.get
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put (b
uri, Int -> FragIndex
FragIndex (Int
i forall a. Num a => a -> a -> a
+ Int
1), forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert FragIndex
fi Cofree (FragExprF a) LocTag
bx Map FragIndex (Cofree (FragExprF a) LocTag)
fragMap)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragIndex -> FragExprF a r
DeferFragF FragIndex
fi

pairF :: BreakState' a b -> BreakState' a b -> BreakState' a b
pairF :: forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF BreakState' a b
x BreakState' a b
y = do
  bx :: Cofree (FragExprF a) LocTag
bx@(LocTag
anno :< FragExprF a (Cofree (FragExprF a) LocTag)
_) <- BreakState' a b
x
  Cofree (FragExprF a) LocTag
by <- BreakState' a b
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> r -> FragExprF a r
PairFragF Cofree (FragExprF a) LocTag
bx Cofree (FragExprF a) LocTag
by

setEnvF :: BreakState' a b -> BreakState' a b
setEnvF :: forall a b. BreakState' a b -> BreakState' a b
setEnvF BreakState' a b
x = do
  x' :: Cofree (FragExprF a) LocTag
x'@(LocTag
anno :< FragExprF a (Cofree (FragExprF a) LocTag)
_) <- BreakState' a b
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> FragExprF a r
SetEnvFragF Cofree (FragExprF a) LocTag
x'

appF :: (Show a, Enum b, Show b) => BreakState' a b -> BreakState' a b -> BreakState' a b
appF :: forall a b.
(Show a, Enum b, Show b) =>
BreakState' a b -> BreakState' a b -> BreakState' a b
appF BreakState' a b
c BreakState' a b
i =
  let (LocTag
anno :< FragExprF a (Cofree (FragExprF a) LocTag)
_) = forall s a. State s a -> s -> a
State.evalState BreakState' a b
c (forall a. Enum a => Int -> a
toEnum Int
0, Int -> FragIndex
FragIndex Int
1, forall k a. Map k a
Map.empty)
      twiddleF :: BreakState' a b
twiddleF = forall a b. Show a => BreakState' a b -> BreakState' a b
deferF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a -> FragExpr a -> FragExpr a
PairFrag (forall a. FragExpr a -> FragExpr a
LeftFrag (forall a. FragExpr a -> FragExpr a
RightFrag forall a. FragExpr a
EnvFrag))
                                                          (forall a. FragExpr a -> FragExpr a -> FragExpr a
PairFrag (forall a. FragExpr a -> FragExpr a
LeftFrag forall a. FragExpr a
EnvFrag)
                                                                    (forall a. FragExpr a -> FragExpr a
RightFrag (forall a. FragExpr a -> FragExpr a
RightFrag forall a. FragExpr a
EnvFrag)))
  in forall a b. BreakState' a b -> BreakState' a b
setEnvF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. BreakState' a b -> BreakState' a b
setEnvF forall a b. (a -> b) -> a -> b
$ forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF BreakState' a b
twiddleF (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF BreakState' a b
i BreakState' a b
c)

showRunBreakState' :: BreakState' RecursionPieceFrag UnsizedRecursionToken -> String
showRunBreakState' :: BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
-> String
showRunBreakState' BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
bs = forall a. Show a => a -> String
show (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget
  (forall s a. State s a -> s -> a
State.evalState BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
bs (forall a. Enum a => Int -> a
toEnum Int
0, Int -> FragIndex
FragIndex Int
1, forall k a. Map k a
Map.empty)) :: FragExpr RecursionPieceFrag)

lamF :: (Show a, Enum b) => BreakState' a b -> BreakState' a b
lamF :: forall a b. (Show a, Enum b) => BreakState' a b -> BreakState' a b
lamF BreakState' a b
x =
  let (LocTag
anno :< FragExprF a (Cofree (FragExprF a) LocTag)
_) = forall s a. State s a -> s -> a
State.evalState BreakState' a b
x (forall a. Enum a => Int -> a
toEnum Int
0, Int -> FragIndex
FragIndex Int
1, forall k a. Map k a
Map.empty)
  in forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall a b. Show a => BreakState' a b -> BreakState' a b
deferF BreakState' a b
x) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragExprF a r
EnvFragF)

clamF :: (Show a, Enum b) => BreakState' a b -> BreakState' a b
clamF :: forall a b. (Show a, Enum b) => BreakState' a b -> BreakState' a b
clamF BreakState' a b
x =
  let (LocTag
anno :< FragExprF a (Cofree (FragExprF a) LocTag)
_) = forall s a. State s a -> s -> a
State.evalState BreakState' a b
x (forall a. Enum a => Int -> a
toEnum Int
0, Int -> FragIndex
FragIndex Int
1, forall k a. Map k a
Map.empty)
  in forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall a b. Show a => BreakState' a b -> BreakState' a b
deferF BreakState' a b
x) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragExprF a r
ZeroFragF)

innerChurchF :: LocTag -> Int -> BreakState' a b
innerChurchF :: forall a b. LocTag -> Int -> BreakState' a b
innerChurchF LocTag
anno Int
x = if Int
x forall a. Ord a => a -> a -> Bool
< Int
0
  then forall a. HasCallStack => String -> a
error (String
"innerChurchF called with " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Int
x)
  else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
anno forall a b. (a -> b) -> a -> b
$ forall a. (a -> a) -> a -> [a]
iterate forall a. FragExpr a -> FragExpr a
SetEnvFrag forall a. FragExpr a
EnvFrag forall a. [a] -> Int -> a
!! Int
x

gateF :: BreakState' a b -> BreakState' a b -> BreakState' a b
gateF :: forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
gateF BreakState' a b
x BreakState' a b
y = do
  x' :: Cofree (FragExprF a) LocTag
x'@(LocTag
anno :< FragExprF a (Cofree (FragExprF a) LocTag)
_) <- BreakState' a b
x
  Cofree (FragExprF a) LocTag
y' <- BreakState' a b
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> r -> FragExprF a r
GateFragF Cofree (FragExprF a) LocTag
x' Cofree (FragExprF a) LocTag
y'

iteF :: BreakState' a b -> BreakState' a b -> BreakState' a b -> BreakState' a b
iteF :: forall a b.
BreakState' a b
-> BreakState' a b -> BreakState' a b -> BreakState' a b
iteF BreakState' a b
x BreakState' a b
y BreakState' a b
z = forall a b. BreakState' a b -> BreakState' a b
setEnvF (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
gateF BreakState' a b
z BreakState' a b
y) BreakState' a b
x)

-- inside two lambdas, (\f x -> ...)
-- creates and iterates on a function "frame" (rf, (rf, (f', (x, env'))))
-- rf is the function to pull arguments out of the frame, run f', and construct the next frame
-- (f',env') is f (since f may contain a saved environment/closure env we want to use for each iteration)
repeatFunctionF :: (Show a, Enum b) => LocTag -> FragExpr a -> BreakState' a b
repeatFunctionF :: forall a b.
(Show a, Enum b) =>
LocTag -> FragExpr a -> BreakState' a b
repeatFunctionF LocTag
l FragExpr a
repeater =
  let applyF :: FragExpr a
applyF = forall a. FragExpr a -> FragExpr a
SetEnvFrag forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a -> FragExpr a
RightFrag forall a. FragExpr a
EnvFrag
      env' :: FragExpr a
env' = forall a. FragExpr a -> FragExpr a
RightFrag (forall a. FragExpr a -> FragExpr a
RightFrag (forall a. FragExpr a -> FragExpr a
RightFrag forall a. FragExpr a
EnvFrag))
      -- takes (rf, (f', (x, env'))), executes f' with (x, env') and creates a new frame
      rf :: BreakState' a b
rf = forall a b. Show a => BreakState' a b -> BreakState' a b
deferF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
l forall a b. (a -> b) -> a -> b
$
                 forall a. FragExpr a -> FragExpr a -> FragExpr a
PairFrag (forall a. FragExpr a -> FragExpr a
LeftFrag forall a. FragExpr a
EnvFrag)
                          (forall a. FragExpr a -> FragExpr a -> FragExpr a
PairFrag (forall a. FragExpr a -> FragExpr a
LeftFrag forall a. FragExpr a
EnvFrag)
                                    (forall a. FragExpr a -> FragExpr a -> FragExpr a
PairFrag (forall a. FragExpr a -> FragExpr a
LeftFrag (forall a. FragExpr a -> FragExpr a
RightFrag forall a. FragExpr a
EnvFrag))
                                              (forall a. FragExpr a -> FragExpr a -> FragExpr a
PairFrag forall a. FragExpr a
applyF forall a. FragExpr a
env')))
      x :: BreakState' a b
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
l forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a -> FragExpr a
LeftFrag forall a. FragExpr a
EnvFrag
      f' :: BreakState' a b
f' = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
LeftFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
LeftFrag forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a -> FragExpr a
RightFrag forall a. FragExpr a
EnvFrag
      fenv :: BreakState' a b
fenv = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
LeftFrag forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a -> FragExpr a
RightFrag forall a. FragExpr a
EnvFrag
      -- (x, ((f', fenv), 0)) -> (rf, (rf, (f', (x, fenv))))
      frameSetup :: BreakState' a b
frameSetup = BreakState' a b
rf forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Cofree (FragExprF a) LocTag
rf' -> forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall (f :: * -> *) a. Applicative f => a -> f a
pure Cofree (FragExprF a) LocTag
rf') (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall (f :: * -> *) a. Applicative f => a -> f a
pure Cofree (FragExprF a) LocTag
rf') (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF BreakState' a b
f' (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF BreakState' a b
x BreakState' a b
fenv))))
      -- run the iterations x' number of times, then unwrap the result from the final frame
      unwrapFrame :: FragExpr a
unwrapFrame = forall a. FragExpr a -> FragExpr a
LeftFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall a b. (a -> b) -> a -> b
$ FragExpr a
repeater
  in forall a b. (Show a, Enum b) => BreakState' a b -> BreakState' a b
clamF (forall a b. (Show a, Enum b) => BreakState' a b -> BreakState' a b
lamF (forall a b. BreakState' a b -> BreakState' a b
setEnvF (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall a b. Show a => BreakState' a b -> BreakState' a b
deferF (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
l forall a b. (a -> b) -> a -> b
$ FragExpr a
unwrapFrame)) BreakState' a b
frameSetup)))

-- to construct a church numeral (\f x -> f ... (f x))
-- the core is nested setenvs around an env, where the number of setenvs is magnitude of church numeral
i2cF :: (Show a, Enum b) => LocTag -> Int -> BreakState' a b
i2cF :: forall a b. (Show a, Enum b) => LocTag -> Int -> BreakState' a b
i2cF LocTag
l Int
n = forall a b.
(Show a, Enum b) =>
LocTag -> FragExpr a -> BreakState' a b
repeatFunctionF LocTag
l (forall a. (a -> a) -> a -> [a]
iterate forall a. FragExpr a -> FragExpr a
SetEnvFrag forall a. FragExpr a
EnvFrag forall a. [a] -> Int -> a
!! Int
n)

unsizedRecursionWrapper :: UnsizedRecursionToken
                        -> BreakState' RecursionPieceFrag UnsizedRecursionToken
                        -> BreakState' RecursionPieceFrag UnsizedRecursionToken
                        -> BreakState' RecursionPieceFrag UnsizedRecursionToken
                        -> BreakState' RecursionPieceFrag UnsizedRecursionToken
unsizedRecursionWrapper :: UnsizedRecursionToken
-> BreakState'
     (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
-> BreakState'
     (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
-> BreakState'
     (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
-> BreakState'
     (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
unsizedRecursionWrapper UnsizedRecursionToken
urToken BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
t BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
r BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
b =
  let firstArgF :: StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
firstArgF = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
DummyLoc forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a -> FragExpr a
LeftFrag forall a. FragExpr a
EnvFrag
      secondArgF :: StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
secondArgF = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
DummyLoc forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a -> FragExpr a
LeftFrag (forall a. FragExpr a -> FragExpr a
RightFrag forall a. FragExpr a
EnvFrag)
      thirdArgF :: StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
thirdArgF = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
DummyLoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
LeftFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a
EnvFrag
      fourthArgF :: StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
fourthArgF = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
DummyLoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
LeftFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a
EnvFrag
      fifthArgF :: StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
fifthArgF = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
DummyLoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
LeftFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. FragExpr a -> FragExpr a
RightFrag forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a
EnvFrag
      abortToken :: StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
abortToken = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
DummyLoc forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a -> FragExpr a -> FragExpr a
PairFrag forall a. FragExpr a
ZeroFrag forall a. FragExpr a
ZeroFrag
      abortFragF :: StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
abortFragF = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragExprF a r
AbortFragF
      -- b is on the stack when this is called, so args are (i, (b, ...))
      abrt :: BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
abrt = forall a b. (Show a, Enum b) => BreakState' a b -> BreakState' a b
lamF (forall a b. BreakState' a b -> BreakState' a b
setEnvF forall a b. (a -> b) -> a -> b
$ forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall a b. BreakState' a b -> BreakState' a b
setEnvF (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
abortFragF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
abortToken))
                                   (forall a b.
(Show a, Enum b, Show b) =>
BreakState' a b -> BreakState' a b -> BreakState' a b
appF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
secondArgF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
firstArgF))
      wrapU :: BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
-> BreakState'
     (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
wrapU =  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:<) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a r. a -> FragExprF a r
AuxFragF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. UnsizedRecursionToken -> a -> RecursionSimulationPieces a
SizingWrapper UnsizedRecursionToken
urToken forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag
-> FragExprUR
FragExprUR)
      -- \t r b r' i -> if t i then r r' i else b i -- t r b are already on the stack when this is evaluated
      rWrap :: BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
rWrap = forall a b. (Show a, Enum b) => BreakState' a b -> BreakState' a b
lamF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Show a, Enum b) => BreakState' a b -> BreakState' a b
lamF forall a b. (a -> b) -> a -> b
$ forall a b.
BreakState' a b
-> BreakState' a b -> BreakState' a b -> BreakState' a b
iteF (forall a b.
(Show a, Enum b, Show b) =>
BreakState' a b -> BreakState' a b -> BreakState' a b
appF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
fifthArgF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
firstArgF)
                                 (forall a b.
(Show a, Enum b, Show b) =>
BreakState' a b -> BreakState' a b -> BreakState' a b
appF (forall a b.
(Show a, Enum b, Show b) =>
BreakState' a b -> BreakState' a b -> BreakState' a b
appF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
fourthArgF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
secondArgF) forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
firstArgF)
                                 (forall a b.
(Show a, Enum b, Show b) =>
BreakState' a b -> BreakState' a b -> BreakState' a b
appF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
thirdArgF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
firstArgF)
      -- hack to make sure recursion test wrapper can be put in a definite place when sizing
      tWrap :: BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
tWrap = forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall a b. Show a => BreakState' a b -> BreakState' a b
deferF forall a b. (a -> b) -> a -> b
$ forall a b.
(Show a, Enum b, Show b) =>
BreakState' a b -> BreakState' a b -> BreakState' a b
appF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
secondArgF forall {a}.
StateT
  (UnsizedRecursionToken, FragIndex,
   Map
     FragIndex
     (Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag))
  Identity
  (Cofree (FragExprF a) LocTag)
firstArgF) (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragExprF a r
ZeroFragF)
      repeater :: FragExpr (RecursionSimulationPieces FragExprUR)
repeater = forall a. a -> FragExpr a
AuxFrag forall a b. (a -> b) -> a -> b
$ forall a. UnsizedRecursionToken -> RecursionSimulationPieces a
NestedSetEnvs UnsizedRecursionToken
urToken
      churchNum :: BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
churchNum = forall a b.
(Show a, Enum b) =>
LocTag -> FragExpr a -> BreakState' a b
repeatFunctionF LocTag
DummyLoc FragExpr (RecursionSimulationPieces FragExprUR)
repeater
      trb :: BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
trb = forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
b (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
r (forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
tWrap (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag LocTag
DummyLoc forall a b. (a -> b) -> a -> b
$ forall a. FragExpr a
ZeroFrag)))
  in forall a b. BreakState' a b -> BreakState' a b
setEnvF forall b c a. (b -> c) -> (a -> b) -> a -> c
. BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
-> BreakState'
     (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
wrapU forall a b. (a -> b) -> a -> b
$ forall a b. BreakState' a b -> BreakState' a b -> BreakState' a b
pairF (forall a b. Show a => BreakState' a b -> BreakState' a b
deferF forall a b. (a -> b) -> a -> b
$ forall a b.
(Show a, Enum b, Show b) =>
BreakState' a b -> BreakState' a b -> BreakState' a b
appF (forall a b.
(Show a, Enum b, Show b) =>
BreakState' a b -> BreakState' a b -> BreakState' a b
appF BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
churchNum BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
rWrap) BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
abrt) BreakState'
  (RecursionSimulationPieces FragExprUR) UnsizedRecursionToken
trb

nextBreakToken :: (Enum b, Show b) => BreakState a b b
nextBreakToken :: forall b a. (Enum b, Show b) => BreakState a b b
nextBreakToken = do
  (b
token, FragIndex
fi, Map FragIndex (Cofree (FragExprF a) LocTag)
fm) <- forall s (m :: * -> *). MonadState s m => m s
State.get
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put (forall a. Enum a => a -> a
succ b
token, FragIndex
fi, Map FragIndex (Cofree (FragExprF a) LocTag)
fm)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure b
token

buildFragMap :: BreakState' a b -> Map FragIndex (Cofree (FragExprF a) LocTag)
buildFragMap :: forall a b.
BreakState' a b -> Map FragIndex (Cofree (FragExprF a) LocTag)
buildFragMap BreakState' a b
bs = let (Cofree (FragExprF a) LocTag
bf, (b
_,FragIndex
_,Map FragIndex (Cofree (FragExprF a) LocTag)
m)) = forall s a. State s a -> s -> (a, s)
State.runState BreakState' a b
bs (forall a. HasCallStack => a
undefined, Int -> FragIndex
FragIndex Int
1, forall k a. Map k a
Map.empty)
                  in forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Int -> FragIndex
FragIndex Int
0) Cofree (FragExprF a) LocTag
bf Map FragIndex (Cofree (FragExprF a) LocTag)
m

pattern FirstArgA :: ExprA a
pattern $mFirstArgA :: forall {r} {a}. ExprA a -> ((# #) -> r) -> ((# #) -> r) -> r
FirstArgA <- PLeftA (EnvA _) _
pattern SecondArgA :: ExprA a
pattern $mSecondArgA :: forall {r} {a}. ExprA a -> ((# #) -> r) -> ((# #) -> r) -> r
SecondArgA <- PLeftA (PRightA (EnvA _) _) _
pattern ThirdArgA :: ExprA a
pattern $mThirdArgA :: forall {r} {a}. ExprA a -> ((# #) -> r) -> ((# #) -> r) -> r
ThirdArgA <- PLeftA (PRightA (PRightA (EnvA _) _) _) _
pattern FourthArgA :: ExprA a
pattern $mFourthArgA :: forall {r} {a}. ExprA a -> ((# #) -> r) -> ((# #) -> r) -> r
FourthArgA <- PLeftA (PRightA (PRightA (PRightA (EnvA _) _) _) _) _
pattern AppA :: ExprA a -> ExprA a -> ExprA a
pattern $mAppA :: forall {r} {a}.
ExprA a -> (ExprA a -> ExprA a -> r) -> ((# #) -> r) -> r
AppA c i <- SetEnvA (SetEnvA (PairA
                                      (DeferA (PairA
                                               (PLeftA (PRightA (EnvA _) _) _)
                                               (PairA (PLeftA (EnvA _) _) (PRightA (PRightA (EnvA _) _) _) _)
                                               _)
                                       _)
                                      (PairA i c _)
                                      _)
                            _)
                    _
pattern LamA :: ExprA a -> ExprA a
pattern $mLamA :: forall {r} {a}. ExprA a -> (ExprA a -> r) -> ((# #) -> r) -> r
LamA x <- PairA (DeferA x _) (EnvA _) _
pattern TwoArgFunA :: ExprA a -> a -> a -> ExprA a
pattern $mTwoArgFunA :: forall {r} {a}.
ExprA a -> (ExprA a -> a -> a -> r) -> ((# #) -> r) -> r
TwoArgFunA c ana anb <- PairA (DeferA (PairA (DeferA c ana) (EnvA _) _) anb) (EnvA _) _
-- TODO check if these make sense at all. A church type should have two arguments (lamdas), but the inner lambdas
-- for addition/multiplication should be f, f+x rather than m+n
-- no, it does not, in \m n f x -> m f (n f x), m and n are FourthArg and ThirdArg respectively
pattern PlusA :: ExprA a -> ExprA a -> ExprA a
pattern $mPlusA :: forall {r} {a}.
ExprA a -> (ExprA a -> ExprA a -> r) -> ((# #) -> r) -> r
PlusA m n <- LamA (LamA (AppA (AppA m SecondArgA) (AppA (AppA n SecondArgA) FirstArgA)))
pattern MultA :: ExprA a -> ExprA a -> ExprA a
pattern $mMultA :: forall {r} {a}.
ExprA a -> (ExprA a -> ExprA a -> r) -> ((# #) -> r) -> r
MultA m n <- LamA (AppA m (AppA n FirstArgA))

data DataType
  = ZeroType
  | ArrType DataType DataType
  | PairType DataType DataType -- only used when at least one side of a pair is not ZeroType
  deriving (DataType -> DataType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DataType -> DataType -> Bool
$c/= :: DataType -> DataType -> Bool
== :: DataType -> DataType -> Bool
$c== :: DataType -> DataType -> Bool
Eq, Int -> DataType -> ShowS
[DataType] -> ShowS
DataType -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataType] -> ShowS
$cshowList :: [DataType] -> ShowS
show :: DataType -> String
$cshow :: DataType -> String
showsPrec :: Int -> DataType -> ShowS
$cshowsPrec :: Int -> DataType -> ShowS
Show, Eq DataType
DataType -> DataType -> Bool
DataType -> DataType -> Ordering
DataType -> DataType -> DataType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DataType -> DataType -> DataType
$cmin :: DataType -> DataType -> DataType
max :: DataType -> DataType -> DataType
$cmax :: DataType -> DataType -> DataType
>= :: DataType -> DataType -> Bool
$c>= :: DataType -> DataType -> Bool
> :: DataType -> DataType -> Bool
$c> :: DataType -> DataType -> Bool
<= :: DataType -> DataType -> Bool
$c<= :: DataType -> DataType -> Bool
< :: DataType -> DataType -> Bool
$c< :: DataType -> DataType -> Bool
compare :: DataType -> DataType -> Ordering
$ccompare :: DataType -> DataType -> Ordering
Ord)

instance Plated DataType where
  plate :: Traversal' DataType DataType
plate DataType -> f DataType
f = \case
    ArrType DataType
i DataType
o  -> DataType -> DataType -> DataType
ArrType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataType -> f DataType
f DataType
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DataType -> f DataType
f DataType
o
    PairType DataType
a DataType
b -> DataType -> DataType -> DataType
PairType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataType -> f DataType
f DataType
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DataType -> f DataType
f DataType
b
    DataType
x            -> forall (f :: * -> *) a. Applicative f => a -> f a
pure DataType
x

data PartialType
  = ZeroTypeP
  | AnyType
  | TypeVariable LocTag Int
  | ArrTypeP PartialType PartialType
  | PairTypeP PartialType PartialType
  deriving (Int -> PartialType -> ShowS
[PartialType] -> ShowS
PartialType -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PartialType] -> ShowS
$cshowList :: [PartialType] -> ShowS
show :: PartialType -> String
$cshow :: PartialType -> String
showsPrec :: Int -> PartialType -> ShowS
$cshowsPrec :: Int -> PartialType -> ShowS
Show, PartialType -> PartialType -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PartialType -> PartialType -> Bool
$c/= :: PartialType -> PartialType -> Bool
== :: PartialType -> PartialType -> Bool
$c== :: PartialType -> PartialType -> Bool
Eq, Eq PartialType
PartialType -> PartialType -> Bool
PartialType -> PartialType -> Ordering
PartialType -> PartialType -> PartialType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PartialType -> PartialType -> PartialType
$cmin :: PartialType -> PartialType -> PartialType
max :: PartialType -> PartialType -> PartialType
$cmax :: PartialType -> PartialType -> PartialType
>= :: PartialType -> PartialType -> Bool
$c>= :: PartialType -> PartialType -> Bool
> :: PartialType -> PartialType -> Bool
$c> :: PartialType -> PartialType -> Bool
<= :: PartialType -> PartialType -> Bool
$c<= :: PartialType -> PartialType -> Bool
< :: PartialType -> PartialType -> Bool
$c< :: PartialType -> PartialType -> Bool
compare :: PartialType -> PartialType -> Ordering
$ccompare :: PartialType -> PartialType -> Ordering
Ord)

instance Plated PartialType where
  plate :: Traversal' PartialType PartialType
plate PartialType -> f PartialType
f = \case
    ArrTypeP PartialType
i PartialType
o  -> PartialType -> PartialType -> PartialType
ArrTypeP forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PartialType -> f PartialType
f PartialType
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PartialType -> f PartialType
f PartialType
o
    PairTypeP PartialType
a PartialType
b -> PartialType -> PartialType -> PartialType
PairTypeP forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PartialType -> f PartialType
f PartialType
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PartialType -> f PartialType
f PartialType
b
    PartialType
x             -> forall (f :: * -> *) a. Applicative f => a -> f a
pure PartialType
x

mergePairType :: DataType -> DataType
mergePairType :: DataType -> DataType
mergePairType = forall a. Plated a => (a -> a) -> a -> a
transform DataType -> DataType
f where
  f :: DataType -> DataType
f (PairType DataType
ZeroType DataType
ZeroType) = DataType
ZeroType
  f DataType
x                            = DataType
x

mergePairTypeP :: PartialType -> PartialType
mergePairTypeP :: PartialType -> PartialType
mergePairTypeP = forall a. Plated a => (a -> a) -> a -> a
transform PartialType -> PartialType
f where
  f :: PartialType -> PartialType
f (PairTypeP PartialType
ZeroTypeP PartialType
ZeroTypeP) = PartialType
ZeroTypeP
  f PartialType
x                               = PartialType
x

containsFunction :: PartialType -> Bool
containsFunction :: PartialType -> Bool
containsFunction = \case
  ArrTypeP PartialType
_ PartialType
_  -> Bool
True
  PairTypeP PartialType
a PartialType
b -> PartialType -> Bool
containsFunction PartialType
a Bool -> Bool -> Bool
|| PartialType -> Bool
containsFunction PartialType
b
  PartialType
_             -> Bool
False

cleanType :: PartialType -> Bool
cleanType :: PartialType -> Bool
cleanType = \case
  PartialType
ZeroTypeP     -> Bool
True
  PairTypeP PartialType
a PartialType
b -> PartialType -> Bool
cleanType PartialType
a Bool -> Bool -> Bool
&& PartialType -> Bool
cleanType PartialType
b
  PartialType
_             -> Bool
False

g2i :: IExpr -> Int
g2i :: IExpr -> Int
g2i IExpr
Zero       = Int
0
g2i (Pair IExpr
a IExpr
b) = Int
1 forall a. Num a => a -> a -> a
+ IExpr -> Int
g2i IExpr
a forall a. Num a => a -> a -> a
+ IExpr -> Int
g2i IExpr
b
g2i IExpr
x          = forall a. HasCallStack => String -> a
error (String
"g2i " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show IExpr
x)

i2g :: Int -> IExpr
i2g :: Int -> IExpr
i2g Int
0 = IExpr
Zero
i2g Int
n = IExpr -> IExpr -> IExpr
Pair (Int -> IExpr
i2g (Int
n forall a. Num a => a -> a -> a
- Int
1)) IExpr
Zero

ints2g :: [Int] -> IExpr
ints2g :: [Int] -> IExpr
ints2g = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (IExpr -> IExpr -> IExpr
Pair forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IExpr
i2g) IExpr
Zero

g2Ints :: IExpr -> [Int]
g2Ints :: IExpr -> [Int]
g2Ints IExpr
Zero       = []
g2Ints (Pair IExpr
n IExpr
g) = IExpr -> Int
g2i IExpr
n forall a. a -> [a] -> [a]
: IExpr -> [Int]
g2Ints IExpr
g
g2Ints IExpr
x          = forall a. HasCallStack => String -> a
error (String
"g2Ints " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show IExpr
x)

s2g :: String -> IExpr
s2g :: String -> IExpr
s2g = [Int] -> IExpr
ints2g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Int
ord

g2s :: IExpr -> String
g2s :: IExpr -> String
g2s = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Char
chr forall b c a. (b -> c) -> (a -> b) -> a -> c
. IExpr -> [Int]
g2Ints

toChurch :: Int -> IExpr
toChurch :: Int -> IExpr
toChurch Int
x =
  let inner :: t -> IExpr
inner t
0 = IExpr -> IExpr
PLeft IExpr
Env
      inner t
a = IExpr -> IExpr -> IExpr
app (IExpr -> IExpr
PLeft forall a b. (a -> b) -> a -> b
$ IExpr -> IExpr
PRight IExpr
Env) (t -> IExpr
inner (t
a forall a. Num a => a -> a -> a
- t
1))
  in IExpr -> IExpr
lam (IExpr -> IExpr
lam (forall {t}. (Eq t, Num t) => t -> IExpr
inner Int
x))

i2gF :: LocTag ->  Int -> BreakState' a b
i2gF :: forall a b. LocTag -> Int -> BreakState' a b
i2gF LocTag
anno Int
0 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragExprF a r
ZeroFragF
i2gF LocTag
anno Int
n = (\Cofree (FragExprF a) LocTag
x Cofree (FragExprF a) LocTag
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> r -> FragExprF a r
PairFragF Cofree (FragExprF a) LocTag
x Cofree (FragExprF a) LocTag
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. LocTag -> Int -> BreakState' a b
i2gF LocTag
anno (Int
n forall a. Num a => a -> a -> a
- Int
1) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure (LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragExprF a r
ZeroFragF)

ints2gF :: LocTag -> [Int] -> BreakState' a b
ints2gF :: forall a b. LocTag -> [Int] -> BreakState' a b
ints2gF LocTag
anno = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Int
i BreakState' a b
g -> (\Cofree (FragExprF a) LocTag
x Cofree (FragExprF a) LocTag
y -> LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> r -> FragExprF a r
PairFragF Cofree (FragExprF a) LocTag
x Cofree (FragExprF a) LocTag
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. LocTag -> Int -> BreakState' a b
i2gF LocTag
anno Int
i forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BreakState' a b
g) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragExprF a r
ZeroFragF)

s2gF :: LocTag -> String -> BreakState' a b
s2gF :: forall a b. LocTag -> String -> BreakState' a b
s2gF LocTag
anno = forall a b. LocTag -> [Int] -> BreakState' a b
ints2gF LocTag
anno forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Char -> Int
ord

-- convention is numbers are left-nested pairs with zero on right
isNum :: IExpr -> Bool
isNum :: IExpr -> Bool
isNum IExpr
Zero          = Bool
True
isNum (Pair IExpr
n IExpr
Zero) = IExpr -> Bool
isNum IExpr
n
isNum IExpr
_             = Bool
False

nextI :: State EIndex EIndex
nextI :: State EIndex EIndex
nextI = forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
State.state forall a b. (a -> b) -> a -> b
$ \(EIndex Int
n) -> (Int -> EIndex
EIndex Int
n, Int -> EIndex
EIndex (Int
n forall a. Num a => a -> a -> a
+ Int
1))

toIndExpr :: IExpr -> State EIndex IndExpr
toIndExpr :: IExpr -> State EIndex IndExpr
toIndExpr IExpr
Zero       = forall a. a -> ExprA a
ZeroA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State EIndex EIndex
nextI
toIndExpr (Pair IExpr
a IExpr
b) = forall a. ExprA a -> ExprA a -> a -> ExprA a
PairA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> State EIndex IndExpr
toIndExpr IExpr
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IExpr -> State EIndex IndExpr
toIndExpr IExpr
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> State EIndex EIndex
nextI
toIndExpr IExpr
Env        = forall a. a -> ExprA a
EnvA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State EIndex EIndex
nextI
toIndExpr (SetEnv IExpr
x) = forall a. ExprA a -> a -> ExprA a
SetEnvA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> State EIndex IndExpr
toIndExpr IExpr
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> State EIndex EIndex
nextI
toIndExpr (Defer IExpr
x)  = forall a. ExprA a -> a -> ExprA a
DeferA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> State EIndex IndExpr
toIndExpr IExpr
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> State EIndex EIndex
nextI
toIndExpr (Gate IExpr
l IExpr
r) = forall a. ExprA a -> ExprA a -> a -> ExprA a
GateA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> State EIndex IndExpr
toIndExpr IExpr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IExpr -> State EIndex IndExpr
toIndExpr IExpr
r forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> State EIndex EIndex
nextI
toIndExpr (PLeft IExpr
x)  = forall a. ExprA a -> a -> ExprA a
PLeftA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> State EIndex IndExpr
toIndExpr IExpr
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> State EIndex EIndex
nextI
toIndExpr (PRight IExpr
x) = forall a. ExprA a -> a -> ExprA a
PRightA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr -> State EIndex IndExpr
toIndExpr IExpr
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> State EIndex EIndex
nextI
toIndExpr IExpr
Trace      = forall a. a -> ExprA a
TraceA forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State EIndex EIndex
nextI

toIndExpr' :: IExpr -> IndExpr
toIndExpr' :: IExpr -> IndExpr
toIndExpr' IExpr
x = forall s a. State s a -> s -> a
State.evalState (IExpr -> State EIndex IndExpr
toIndExpr IExpr
x) (Int -> EIndex
EIndex Int
0)

instance TelomareLike (ExprT a) where
  fromTelomare :: IExpr -> ExprT a
fromTelomare = \case
    IExpr
Zero     -> forall a. ExprT a
ZeroT
    Pair IExpr
a IExpr
b -> forall a. ExprT a -> ExprT a -> ExprT a
PairT (forall a. TelomareLike a => IExpr -> a
fromTelomare IExpr
a) (forall a. TelomareLike a => IExpr -> a
fromTelomare IExpr
b)
    IExpr
Env      -> forall a. ExprT a
EnvT
    SetEnv IExpr
x -> forall a. ExprT a -> ExprT a
SetEnvT forall a b. (a -> b) -> a -> b
$ forall a. TelomareLike a => IExpr -> a
fromTelomare IExpr
x
    Defer IExpr
x  -> forall a. ExprT a -> ExprT a
DeferT forall a b. (a -> b) -> a -> b
$ forall a. TelomareLike a => IExpr -> a
fromTelomare IExpr
x
    Gate IExpr
l IExpr
r -> forall a. ExprT a -> ExprT a -> ExprT a
GateT (forall a. TelomareLike a => IExpr -> a
fromTelomare IExpr
l) (forall a. TelomareLike a => IExpr -> a
fromTelomare IExpr
r)
    PLeft IExpr
x  -> forall a. ExprT a -> ExprT a
LeftT forall a b. (a -> b) -> a -> b
$ forall a. TelomareLike a => IExpr -> a
fromTelomare IExpr
x
    PRight IExpr
x -> forall a. ExprT a -> ExprT a
RightT forall a b. (a -> b) -> a -> b
$ forall a. TelomareLike a => IExpr -> a
fromTelomare IExpr
x
    IExpr
Trace    -> forall a. ExprT a
TraceT
  toTelomare :: ExprT a -> Maybe IExpr
toTelomare = \case
    ExprT a
ZeroT     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure IExpr
Zero
    PairT ExprT a
a ExprT a
b -> IExpr -> IExpr -> IExpr
Pair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TelomareLike a => a -> Maybe IExpr
toTelomare ExprT a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. TelomareLike a => a -> Maybe IExpr
toTelomare ExprT a
b
    ExprT a
EnvT      -> forall (f :: * -> *) a. Applicative f => a -> f a
pure IExpr
Env
    SetEnvT ExprT a
x -> IExpr -> IExpr
SetEnv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TelomareLike a => a -> Maybe IExpr
toTelomare ExprT a
x
    DeferT ExprT a
x  -> IExpr -> IExpr
Defer forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TelomareLike a => a -> Maybe IExpr
toTelomare ExprT a
x
    ExprT a
AbortT    -> forall a. Maybe a
Nothing
    GateT ExprT a
l ExprT a
r -> IExpr -> IExpr -> IExpr
Gate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TelomareLike a => a -> Maybe IExpr
toTelomare ExprT a
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. TelomareLike a => a -> Maybe IExpr
toTelomare ExprT a
r
    LeftT ExprT a
x   -> IExpr -> IExpr
PLeft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TelomareLike a => a -> Maybe IExpr
toTelomare ExprT a
x
    RightT ExprT a
x  -> IExpr -> IExpr
PRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TelomareLike a => a -> Maybe IExpr
toTelomare ExprT a
x
    ExprT a
TraceT    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure IExpr
Trace
    TagT ExprT a
x a
_  -> forall a. TelomareLike a => a -> Maybe IExpr
toTelomare ExprT a
x -- just elide tags

telomareToFragmap :: IExpr -> Map FragIndex (Cofree (FragExprF a) LocTag)
telomareToFragmap :: forall a. IExpr -> Map FragIndex (Cofree (FragExprF a) LocTag)
telomareToFragmap IExpr
expr = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Int -> FragIndex
FragIndex Int
0) Cofree (FragExprF a) LocTag
bf Map FragIndex (Cofree (FragExprF a) LocTag)
m where
    (Cofree (FragExprF a) LocTag
bf, (FragIndex
_,Map FragIndex (Cofree (FragExprF a) LocTag)
m)) = forall s a. State s a -> s -> (a, s)
State.runState (IExpr
-> StateT
     (FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))
     Identity
     (Cofree (FragExprF a) LocTag)
convert IExpr
expr) (Int -> FragIndex
FragIndex Int
1, forall k a. Map k a
Map.empty)
    convert :: IExpr
-> StateT
     (FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))
     Identity
     (Cofree (FragExprF a) LocTag)
convert = \case
      IExpr
Zero -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragExprF a r
ZeroFragF
      Pair IExpr
a IExpr
b -> (\Cofree (FragExprF a) LocTag
x Cofree (FragExprF a) LocTag
y -> LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> r -> FragExprF a r
PairFragF Cofree (FragExprF a) LocTag
x Cofree (FragExprF a) LocTag
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr
-> StateT
     (FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))
     Identity
     (Cofree (FragExprF a) LocTag)
convert IExpr
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IExpr
-> StateT
     (FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))
     Identity
     (Cofree (FragExprF a) LocTag)
convert IExpr
b
      IExpr
Env -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragExprF a r
EnvFragF
      SetEnv IExpr
x -> (\Cofree (FragExprF a) LocTag
y -> LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> FragExprF a r
SetEnvFragF Cofree (FragExprF a) LocTag
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr
-> StateT
     (FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))
     Identity
     (Cofree (FragExprF a) LocTag)
convert IExpr
x
      Defer IExpr
x -> do
        Cofree (FragExprF a) LocTag
bx <- IExpr
-> StateT
     (FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))
     Identity
     (Cofree (FragExprF a) LocTag)
convert IExpr
x
        (fi :: FragIndex
fi@(FragIndex Int
i), Map FragIndex (Cofree (FragExprF a) LocTag)
fragMap) <- forall s (m :: * -> *). MonadState s m => m s
State.get
        forall s (m :: * -> *). MonadState s m => s -> m ()
State.put (Int -> FragIndex
FragIndex (Int
i forall a. Num a => a -> a -> a
+ Int
1), forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert FragIndex
fi Cofree (FragExprF a) LocTag
bx Map FragIndex (Cofree (FragExprF a) LocTag)
fragMap)
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragIndex -> FragExprF a r
DeferFragF FragIndex
fi
      Gate IExpr
l IExpr
r -> (\Cofree (FragExprF a) LocTag
x Cofree (FragExprF a) LocTag
y -> LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> r -> FragExprF a r
GateFragF Cofree (FragExprF a) LocTag
x Cofree (FragExprF a) LocTag
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr
-> StateT
     (FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))
     Identity
     (Cofree (FragExprF a) LocTag)
convert IExpr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IExpr
-> StateT
     (FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))
     Identity
     (Cofree (FragExprF a) LocTag)
convert IExpr
r
      PLeft IExpr
x -> (\Cofree (FragExprF a) LocTag
y -> LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> FragExprF a r
LeftFragF Cofree (FragExprF a) LocTag
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr
-> StateT
     (FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))
     Identity
     (Cofree (FragExprF a) LocTag)
convert IExpr
x
      PRight IExpr
x -> (\Cofree (FragExprF a) LocTag
y -> LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. r -> FragExprF a r
RightFragF Cofree (FragExprF a) LocTag
y) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IExpr
-> StateT
     (FragIndex, Map FragIndex (Cofree (FragExprF a) LocTag))
     Identity
     (Cofree (FragExprF a) LocTag)
convert IExpr
x
      IExpr
Trace -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LocTag
DummyLoc forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< forall a r. FragExprF a r
TraceFragF

fragmapToTelomare :: Map FragIndex (FragExpr a) -> Maybe IExpr
fragmapToTelomare :: forall a. Map FragIndex (FragExpr a) -> Maybe IExpr
fragmapToTelomare Map FragIndex (FragExpr a)
fragMap = FragExpr a -> Maybe IExpr
convert (forall a. Map FragIndex a -> a
rootFrag Map FragIndex (FragExpr a)
fragMap) where
    convert :: FragExpr a -> Maybe IExpr
convert = \case
      FragExpr a
ZeroFrag      -> forall (f :: * -> *) a. Applicative f => a -> f a
pure IExpr
Zero
      PairFrag FragExpr a
a FragExpr a
b  -> IExpr -> IExpr -> IExpr
Pair forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FragExpr a -> Maybe IExpr
convert FragExpr a
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FragExpr a -> Maybe IExpr
convert FragExpr a
b
      FragExpr a
EnvFrag       -> forall (f :: * -> *) a. Applicative f => a -> f a
pure IExpr
Env
      SetEnvFrag FragExpr a
x  -> IExpr -> IExpr
SetEnv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FragExpr a -> Maybe IExpr
convert FragExpr a
x
      DeferFrag FragIndex
ind -> IExpr -> IExpr
Defer forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FragIndex
ind Map FragIndex (FragExpr a)
fragMap forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FragExpr a -> Maybe IExpr
convert)
      FragExpr a
AbortFrag     -> forall a. Maybe a
Nothing
      GateFrag FragExpr a
l FragExpr a
r  -> IExpr -> IExpr -> IExpr
Gate forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FragExpr a -> Maybe IExpr
convert FragExpr a
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FragExpr a -> Maybe IExpr
convert FragExpr a
r
      LeftFrag FragExpr a
x    -> IExpr -> IExpr
PLeft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FragExpr a -> Maybe IExpr
convert FragExpr a
x
      RightFrag FragExpr a
x   -> IExpr -> IExpr
PRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FragExpr a -> Maybe IExpr
convert FragExpr a
x
      FragExpr a
TraceFrag     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure IExpr
Trace
      AuxFrag a
_     -> forall a. Maybe a
Nothing

forget :: Corecursive a => Cofree (Base a) anno -> a
forget :: forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget = forall t a. Recursive t => (Base t a -> a) -> t -> a
cata (\(anno
_ CofreeT.:< Base a a
z) -> forall t. Corecursive t => Base t t -> t
embed Base a a
z)

tag :: Recursive a => anno -> a -> Cofree (Base a) anno
tag :: forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag anno
anno a
x = anno
anno forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< (forall a anno. Recursive a => anno -> a -> Cofree (Base a) anno
tag anno
anno forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. Recursive t => t -> Base t t
project a
x)

newtype FragExprURSansAnnotation =
  FragExprURSA { FragExprURSansAnnotation
-> FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
unFragExprURSA :: FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
               }
  deriving (FragExprURSansAnnotation -> FragExprURSansAnnotation -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FragExprURSansAnnotation -> FragExprURSansAnnotation -> Bool
$c/= :: FragExprURSansAnnotation -> FragExprURSansAnnotation -> Bool
== :: FragExprURSansAnnotation -> FragExprURSansAnnotation -> Bool
$c== :: FragExprURSansAnnotation -> FragExprURSansAnnotation -> Bool
Eq, Int -> FragExprURSansAnnotation -> ShowS
[FragExprURSansAnnotation] -> ShowS
FragExprURSansAnnotation -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FragExprURSansAnnotation] -> ShowS
$cshowList :: [FragExprURSansAnnotation] -> ShowS
show :: FragExprURSansAnnotation -> String
$cshow :: FragExprURSansAnnotation -> String
showsPrec :: Int -> FragExprURSansAnnotation -> ShowS
$cshowsPrec :: Int -> FragExprURSansAnnotation -> ShowS
Show)

forgetAnnotationFragExprUR :: FragExprUR -> FragExprURSansAnnotation
forgetAnnotationFragExprUR :: FragExprUR -> FragExprURSansAnnotation
forgetAnnotationFragExprUR = FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
-> FragExprURSansAnnotation
FragExprURSA forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Recursive t => (Base t a -> a) -> t -> a
cata Base
  (FragExpr (RecursionSimulationPieces FragExprUR))
  (FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
-> FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
ff forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall anno.
Cofree
  (Base (FragExpr (RecursionSimulationPieces FragExprUR))) anno
-> FragExpr (RecursionSimulationPieces FragExprUR)
forget' forall b c a. (b -> c) -> (a -> b) -> a -> c
. FragExprUR
-> Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag
unFragExprUR where
  forget' :: Cofree (Base (FragExpr (RecursionSimulationPieces FragExprUR))) anno
          -> FragExpr (RecursionSimulationPieces FragExprUR)
  forget' :: forall anno.
Cofree
  (Base (FragExpr (RecursionSimulationPieces FragExprUR))) anno
-> FragExpr (RecursionSimulationPieces FragExprUR)
forget' = forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget
  ff :: Base (FragExpr (RecursionSimulationPieces FragExprUR))
             (FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
     -> FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
  ff :: Base
  (FragExpr (RecursionSimulationPieces FragExprUR))
  (FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
-> FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
ff = \case
    AuxFragF (SizingWrapper UnsizedRecursionToken
ind FragExprUR
x) -> forall a. a -> FragExpr a
AuxFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. UnsizedRecursionToken -> a -> RecursionSimulationPieces a
SizingWrapper UnsizedRecursionToken
ind forall b c a. (b -> c) -> (a -> b) -> a -> c
. FragExprUR -> FragExprURSansAnnotation
forgetAnnotationFragExprUR forall a b. (a -> b) -> a -> b
$ FragExprUR
x
    AuxFragF (NestedSetEnvs UnsizedRecursionToken
t) -> forall a. a -> FragExpr a
AuxFrag forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. UnsizedRecursionToken -> RecursionSimulationPieces a
NestedSetEnvs forall a b. (a -> b) -> a -> b
$ UnsizedRecursionToken
t
    Base
  (FragExpr (RecursionSimulationPieces FragExprUR))
  (FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
FragExprF
  (RecursionSimulationPieces FragExprUR)
  (FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
ZeroFragF -> forall a. FragExpr a
ZeroFrag
    PairFragF FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
a FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
b -> forall a. FragExpr a -> FragExpr a -> FragExpr a
PairFrag FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
a FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
b
    Base
  (FragExpr (RecursionSimulationPieces FragExprUR))
  (FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
FragExprF
  (RecursionSimulationPieces FragExprUR)
  (FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
EnvFragF -> forall a. FragExpr a
EnvFrag
    SetEnvFragF FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
x -> forall a. FragExpr a -> FragExpr a
SetEnvFrag FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
x
    DeferFragF FragIndex
ind -> forall a. FragIndex -> FragExpr a
DeferFrag FragIndex
ind
    Base
  (FragExpr (RecursionSimulationPieces FragExprUR))
  (FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
FragExprF
  (RecursionSimulationPieces FragExprUR)
  (FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
AbortFragF -> forall a. FragExpr a
AbortFrag
    GateFragF FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
l FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
r -> forall a. FragExpr a -> FragExpr a -> FragExpr a
GateFrag FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
l FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
r
    LeftFragF FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
x -> forall a. FragExpr a -> FragExpr a
LeftFrag FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
x
    RightFragF FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
x -> forall a. FragExpr a -> FragExpr a
RightFrag FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
x
    Base
  (FragExpr (RecursionSimulationPieces FragExprUR))
  (FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
FragExprF
  (RecursionSimulationPieces FragExprUR)
  (FragExpr (RecursionSimulationPieces FragExprURSansAnnotation))
TraceFragF -> forall a. FragExpr a
TraceFrag

instance TelomareLike Term3 where
  fromTelomare :: IExpr -> Term3
fromTelomare = Map FragIndex FragExprUR -> Term3
Term3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Cofree (FragExprF (RecursionSimulationPieces FragExprUR)) LocTag
-> FragExprUR
FragExprUR forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IExpr -> Map FragIndex (Cofree (FragExprF a) LocTag)
telomareToFragmap
  toTelomare :: Term3 -> Maybe IExpr
toTelomare (Term3 Map FragIndex FragExprUR
t) = forall a. Map FragIndex (FragExpr a) -> Maybe IExpr
fragmapToTelomare forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map FragExprURSansAnnotation
-> FragExpr (RecursionSimulationPieces FragExprURSansAnnotation)
unFragExprURSA Map FragIndex FragExprURSansAnnotation
fragMap where
    fragMap :: Map FragIndex FragExprURSansAnnotation
fragMap = FragExprUR -> FragExprURSansAnnotation
forgetAnnotationFragExprUR forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map FragIndex FragExprUR
t

instance TelomareLike Term4 where
  fromTelomare :: IExpr -> Term4
fromTelomare = Map FragIndex (Cofree (FragExprF Void) LocTag) -> Term4
Term4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IExpr -> Map FragIndex (Cofree (FragExprF a) LocTag)
telomareToFragmap
  toTelomare :: Term4 -> Maybe IExpr
toTelomare (Term4 Map FragIndex (Cofree (FragExprF Void) LocTag)
fragMap) = forall a. Map FragIndex (FragExpr a) -> Maybe IExpr
fragmapToTelomare (forall a anno. Corecursive a => Cofree (Base a) anno -> a
forget forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map FragIndex (Cofree (FragExprF Void) LocTag)
fragMap)

-- general utility functions

insertAndGetKey :: (Ord e, Enum e) => a -> State (Map e a) e
insertAndGetKey :: forall e a. (Ord e, Enum e) => a -> State (Map e a) e
insertAndGetKey a
v = do
  Map e a
m <- forall s (m :: * -> *). MonadState s m => m s
State.get
  let nextKey :: e
nextKey = case forall a. Set a -> Maybe a
Set.lookupMax forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> Set k
Map.keysSet Map e a
m of
        Maybe e
Nothing -> forall a. Enum a => Int -> a
toEnum Int
0
        Just e
n  -> forall a. Enum a => a -> a
succ e
n
  forall s (m :: * -> *). MonadState s m => s -> m ()
State.put forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert e
nextKey a
v Map e a
m
  forall (f :: * -> *) a. Applicative f => a -> f a
pure e
nextKey

-- abort codes
-- t x = if x <= 1
-- fact1 r x = if x <= 1
--    then 1
--    else x * (r (x - 1))
-- fix fact1
-- (\f x -> f x) fact1 (\_ -> error!) 3 -- error!
-- (\f x -> f (f x)) fact1 (\_ -> error!) 3 -- error!
-- (\f x -> f (f (f x))) fact1 (\_ -> error!) 3 -- 3, happy!
-- setenv env -- church numeral 1
-- setenv (setenv env) -- church numeral 2


pattern AbortRecursion :: IExpr
pattern $bAbortRecursion :: IExpr
$mAbortRecursion :: forall {r}. IExpr -> ((# #) -> r) -> ((# #) -> r) -> r
AbortRecursion = Pair Zero Zero
pattern AbortUser :: IExpr -> IExpr
pattern $bAbortUser :: IExpr -> IExpr
$mAbortUser :: forall {r}. IExpr -> (IExpr -> r) -> ((# #) -> r) -> r
AbortUser m = Pair (Pair Zero Zero) m
pattern AbortAny :: IExpr
pattern $bAbortAny :: IExpr
$mAbortAny :: forall {r}. IExpr -> ((# #) -> r) -> ((# #) -> r) -> r
AbortAny = Pair (Pair (Pair Zero Zero) Zero) Zero
pattern AbortUnsizeable :: IExpr -> IExpr
pattern $bAbortUnsizeable :: IExpr -> IExpr
$mAbortUnsizeable :: forall {r}. IExpr -> (IExpr -> r) -> ((# #) -> r) -> r
AbortUnsizeable t = Pair (Pair (Pair (Pair Zero Zero) Zero) Zero) t

-- |AST for patterns in `case` expressions
data Pattern
  = PatternVar String
  | PatternInt Int
  | PatternString String
  | PatternIgnore
  | PatternPair Pattern Pattern
  deriving (Int -> Pattern -> ShowS
[Pattern] -> ShowS
Pattern -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Pattern] -> ShowS
$cshowList :: [Pattern] -> ShowS
show :: Pattern -> String
$cshow :: Pattern -> String
showsPrec :: Int -> Pattern -> ShowS
$cshowsPrec :: Int -> Pattern -> ShowS
Show, Pattern -> Pattern -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pattern -> Pattern -> Bool
$c/= :: Pattern -> Pattern -> Bool
== :: Pattern -> Pattern -> Bool
$c== :: Pattern -> Pattern -> Bool
Eq, Eq Pattern
Pattern -> Pattern -> Bool
Pattern -> Pattern -> Ordering
Pattern -> Pattern -> Pattern
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Pattern -> Pattern -> Pattern
$cmin :: Pattern -> Pattern -> Pattern
max :: Pattern -> Pattern -> Pattern
$cmax :: Pattern -> Pattern -> Pattern
>= :: Pattern -> Pattern -> Bool
$c>= :: Pattern -> Pattern -> Bool
> :: Pattern -> Pattern -> Bool
$c> :: Pattern -> Pattern -> Bool
<= :: Pattern -> Pattern -> Bool
$c<= :: Pattern -> Pattern -> Bool
< :: Pattern -> Pattern -> Bool
$c< :: Pattern -> Pattern -> Bool
compare :: Pattern -> Pattern -> Ordering
$ccompare :: Pattern -> Pattern -> Ordering
Ord)
makeBaseFunctor ''Pattern

-- |Firstly parsed AST sans location annotations
data UnprocessedParsedTerm
  = VarUP String
  | ITEUP UnprocessedParsedTerm UnprocessedParsedTerm UnprocessedParsedTerm
  | LetUP [(String, UnprocessedParsedTerm)] UnprocessedParsedTerm
  | ListUP [UnprocessedParsedTerm]
  | IntUP Int
  | StringUP String
  | PairUP UnprocessedParsedTerm UnprocessedParsedTerm
  | AppUP UnprocessedParsedTerm UnprocessedParsedTerm
  | LamUP String UnprocessedParsedTerm
  | ChurchUP Int
  | UnsizedRecursionUP UnprocessedParsedTerm UnprocessedParsedTerm UnprocessedParsedTerm
  | LeftUP UnprocessedParsedTerm
  | RightUP UnprocessedParsedTerm
  | TraceUP UnprocessedParsedTerm
  | CheckUP UnprocessedParsedTerm UnprocessedParsedTerm
  | HashUP UnprocessedParsedTerm -- ^ On ad hoc user defined types, this term will be substitued to a unique Int.
  | CaseUP UnprocessedParsedTerm [(Pattern, UnprocessedParsedTerm)]
  deriving (UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
$c/= :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
== :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
$c== :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
Eq, Eq UnprocessedParsedTerm
UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
UnprocessedParsedTerm -> UnprocessedParsedTerm -> Ordering
UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
$cmin :: UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
max :: UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
$cmax :: UnprocessedParsedTerm
-> UnprocessedParsedTerm -> UnprocessedParsedTerm
>= :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
$c>= :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
> :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
$c> :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
<= :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
$c<= :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
< :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
$c< :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Bool
compare :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Ordering
$ccompare :: UnprocessedParsedTerm -> UnprocessedParsedTerm -> Ordering
Ord, Int -> UnprocessedParsedTerm -> ShowS
[UnprocessedParsedTerm] -> ShowS
UnprocessedParsedTerm -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UnprocessedParsedTerm] -> ShowS
$cshowList :: [UnprocessedParsedTerm] -> ShowS
show :: UnprocessedParsedTerm -> String
$cshow :: UnprocessedParsedTerm -> String
showsPrec :: Int -> UnprocessedParsedTerm -> ShowS
$cshowsPrec :: Int -> UnprocessedParsedTerm -> ShowS
Show)
makeBaseFunctor ''UnprocessedParsedTerm -- Functorial version UnprocessedParsedTerm
makePrisms ''UnprocessedParsedTerm
deriveShow1 ''UnprocessedParsedTermF