-- | Syntax and evaluation of terms.
module Glam.Term where

import Data.Function
import Data.List
import Data.Map.Lazy (Map)
import Data.Map.Lazy qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Text.Megaparsec
import Control.Monad.Combinators.Expr

import Glam.Utils

-- | Variables
type Var = String

-- | Substitutions
type Subst = Map Var Term

infixl :<*>:
infixl 9 :$:

-- | Terms of the guarded λ-calculus
data Term = Var Var -- ^ Variables
          | Int Integer | Plus Term Term | Minus Term Term | Times Term Term | Divide Term Term | IntRec -- ^ Integers
          | Unit | Pair Term Term | Fst Term | Snd Term -- ^ Products
          | Abort Term | InL Term | InR Term | Case Term Term Term -- ^ Sums
          | Abs Var Term | Term :$: Term -- ^ Functions
          | Let Subst Term -- ^ Let-bindings
          | Fold Term | Unfold Term | Fix Term -- ^ Guarded recursion
          | Next Term | Prev Term | Term :<*>: Term -- ^ @▸@ operations
          | Box Term | Unbox Term -- ^ @■@ operations
          deriving Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
/= :: Term -> Term -> Bool
Eq

-- * Free variables

freeVars :: Term -> Set Var
freeVars :: Term -> Set Var
freeVars (Var Var
x)        = Var -> Set Var
forall a. a -> Set a
Set.singleton Var
x
freeVars (Int Integer
_)        = Set Var
forall a. Monoid a => a
mempty
freeVars (Plus Term
t1 Term
t2)   = Term -> Set Var
freeVars Term
t1 Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Term -> Set Var
freeVars Term
t2
freeVars (Minus Term
t1 Term
t2)  = Term -> Set Var
freeVars Term
t1 Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Term -> Set Var
freeVars Term
t2
freeVars (Times Term
t1 Term
t2)  = Term -> Set Var
freeVars Term
t1 Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Term -> Set Var
freeVars Term
t2
freeVars (Divide Term
t1 Term
t2) = Term -> Set Var
freeVars Term
t1 Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Term -> Set Var
freeVars Term
t2
freeVars Term
IntRec         = Set Var
forall a. Monoid a => a
mempty
freeVars Term
Unit           = Set Var
forall a. Monoid a => a
mempty
freeVars (Pair Term
t1 Term
t2)   = Term -> Set Var
freeVars Term
t1 Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Term -> Set Var
freeVars Term
t2
freeVars (Fst Term
t)        = Term -> Set Var
freeVars Term
t
freeVars (Snd Term
t)        = Term -> Set Var
freeVars Term
t
freeVars (Abort Term
t)      = Term -> Set Var
freeVars Term
t
freeVars (InL Term
t)        = Term -> Set Var
freeVars Term
t
freeVars (InR Term
t)        = Term -> Set Var
freeVars Term
t
freeVars (Case Term
t Term
t1 Term
t2) = Term -> Set Var
freeVars Term
t Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Term -> Set Var
freeVars Term
t1 Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Term -> Set Var
freeVars Term
t2
freeVars (Abs Var
x Term
t)      = Var -> Set Var -> Set Var
forall a. Ord a => a -> Set a -> Set a
Set.delete Var
x (Term -> Set Var
freeVars Term
t)
freeVars (Term
t1 :$: Term
t2)    = Term -> Set Var
freeVars Term
t1 Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Term -> Set Var
freeVars Term
t2
freeVars (Let Subst
s Term
t)      = (Term -> Set Var) -> Subst -> Set Var
forall m a. Monoid m => (a -> m) -> Map Var a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term -> Set Var
freeVars Subst
s Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> (Term -> Set Var
freeVars Term
t Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Subst -> Set Var
forall k a. Map k a -> Set k
Map.keysSet Subst
s)
freeVars (Fold Term
t)       = Term -> Set Var
freeVars Term
t
freeVars (Unfold Term
t)     = Term -> Set Var
freeVars Term
t
freeVars (Fix Term
t)        = Term -> Set Var
freeVars Term
t
freeVars (Next Term
t)       = Term -> Set Var
freeVars Term
t
freeVars (Prev Term
t)       = Term -> Set Var
freeVars Term
t
freeVars (Term
t1 :<*>: Term
t2)  = Term -> Set Var
freeVars Term
t1 Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Term -> Set Var
freeVars Term
t2
freeVars (Box Term
t)        = Term -> Set Var
freeVars Term
t
freeVars (Unbox Term
t)      = Term -> Set Var
freeVars Term
t

freeIn :: Var -> Term -> Bool
Var
x freeIn :: Var -> Term -> Bool
`freeIn` Term
t = Var
x Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Term -> Set Var
freeVars Term
t

-- * Evaluation

-- | Values are basically destructor-free terms, with abstractions represented
-- in a higher-order way.
data Value = VInt !Integer
           | VUnit | VPair Value Value
           | VInL Value | VInR Value
           | VAbs (Value -> Value)
           | VFold Value
           | VNext Value
           | VBox Value

intrec :: (a -> a) -> a -> (a -> a) -> Integer -> a
intrec :: forall a. (a -> a) -> a -> (a -> a) -> Integer -> a
intrec a -> a
p a
z a -> a
s = Integer -> a
forall {t}. (Ord t, Num t, Enum t) => t -> a
go where
    go :: t -> a
go t
n = case t -> t -> Ordering
forall a. Ord a => a -> a -> Ordering
compare t
n t
0 of
        Ordering
LT -> a -> a
p (t -> a
go (t -> t
forall a. Enum a => a -> a
succ t
n))
        Ordering
EQ -> a
z
        Ordering
GT -> a -> a
s (t -> a
go (t -> t
forall a. Enum a => a -> a
pred t
n))

-- | Evaluate a term in the given environment.
eval :: Map Var Value -> Term -> Value
eval :: Map Var Value -> Term -> Value
eval Map Var Value
s (Var Var
x)          = Map Var Value
s Map Var Value -> Var -> Value
forall k a. Ord k => Map k a -> k -> a
Map.! Var
x
eval Map Var Value
_ (Int Integer
i)          = Integer -> Value
VInt Integer
i
eval Map Var Value
s (Plus Term
t1 Term
t2)     = case (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t1, Map Var Value -> Term -> Value
eval Map Var Value
s Term
t2) of ~(VInt Integer
i1, VInt Integer
i2) -> Integer -> Value
VInt (Integer
i1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i2)
eval Map Var Value
s (Minus Term
t1 Term
t2)    = case (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t1, Map Var Value -> Term -> Value
eval Map Var Value
s Term
t2) of ~(VInt Integer
i1, VInt Integer
i2) -> Integer -> Value
VInt (Integer
i1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
i2)
eval Map Var Value
s (Times Term
t1 Term
t2)    = case (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t1, Map Var Value -> Term -> Value
eval Map Var Value
s Term
t2) of ~(VInt Integer
i1, VInt Integer
i2) -> Integer -> Value
VInt (Integer
i1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
i2)
eval Map Var Value
s (Divide Term
t1 Term
t2)   = case (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t1, Map Var Value -> Term -> Value
eval Map Var Value
s Term
t2) of ~(VInt Integer
i1, VInt Integer
i2) -> Integer -> Value
VInt (Integer
i1 Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
i2)
eval Map Var Value
_ Term
IntRec           = (Value -> Value) -> Value
VAbs \(VAbs Value -> Value
p) -> (Value -> Value) -> Value
VAbs \Value
z -> (Value -> Value) -> Value
VAbs \(VAbs Value -> Value
s) -> (Value -> Value) -> Value
VAbs \(VInt Integer
n) -> (Value -> Value) -> Value -> (Value -> Value) -> Integer -> Value
forall a. (a -> a) -> a -> (a -> a) -> Integer -> a
intrec Value -> Value
p Value
z Value -> Value
s Integer
n
eval Map Var Value
_ Term
Unit             = Value
VUnit
eval Map Var Value
s (Pair Term
t1 Term
t2)     = Value -> Value -> Value
VPair (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t1) (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t2)
eval Map Var Value
s (Fst Term
t)          = case Map Var Value -> Term -> Value
eval Map Var Value
s Term
t of ~(VPair Value
t1 Value
_) -> Value
t1
eval Map Var Value
s (Snd Term
t)          = case Map Var Value -> Term -> Value
eval Map Var Value
s Term
t of ~(VPair Value
_ Value
t2) -> Value
t2
eval Map Var Value
_ (Abort Term
_)        = Value
forall a. HasCallStack => a
undefined
eval Map Var Value
s (InL Term
t)          = Value -> Value
VInL (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t)
eval Map Var Value
s (InR Term
t)          = Value -> Value
VInR (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t)
eval Map Var Value
s (Case Term
t ~(Abs Var
x1 Term
t1) ~(Abs Var
x2 Term
t2)) = case Map Var Value -> Term -> Value
eval Map Var Value
s Term
t of
    VInL Value
l -> Map Var Value -> Term -> Value
eval (Var -> Value -> Map Var Value -> Map Var Value
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
x1 Value
l Map Var Value
s) Term
t1
    VInR Value
r -> Map Var Value -> Term -> Value
eval (Var -> Value -> Map Var Value -> Map Var Value
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
x2 Value
r Map Var Value
s) Term
t2
    Value
_ -> Value
forall a. HasCallStack => a
undefined
eval Map Var Value
s (Abs Var
x Term
t)        = (Value -> Value) -> Value
VAbs (\ Value
v -> Map Var Value -> Term -> Value
eval (Var -> Value -> Map Var Value -> Map Var Value
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
x Value
v Map Var Value
s) Term
t)
eval Map Var Value
s (Term
t1 :$: Term
t2)      = case Map Var Value -> Term -> Value
eval Map Var Value
s Term
t1 of ~(VAbs Value -> Value
f) -> Value -> Value
f (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t2)
eval Map Var Value
s (Let Subst
s' Term
t)       = Map Var Value -> Term -> Value
eval (Map Var Value -> Map Var Value -> Map Var Value
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Map Var Value -> Term -> Value
eval Map Var Value
s (Term -> Value) -> Subst -> Map Var Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Subst
s') Map Var Value
s) Term
t
eval Map Var Value
s (Fold Term
t)         = Value -> Value
VFold (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t)
eval Map Var Value
s (Unfold Term
t)       = case Map Var Value -> Term -> Value
eval Map Var Value
s Term
t of ~(VFold Value
t) -> Value
t
eval Map Var Value
s (Fix ~(Abs Var
x Term
t)) = (Value -> Value) -> Value
forall a. (a -> a) -> a
fix \ Value
self -> Map Var Value -> Term -> Value
eval (Var -> Value -> Map Var Value -> Map Var Value
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
x (Value -> Value
VNext Value
self) Map Var Value
s) Term
t
eval Map Var Value
s (Next Term
t)         = Value -> Value
VNext (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t)
eval Map Var Value
s (Prev Term
t)         = case Map Var Value -> Term -> Value
eval Map Var Value
s Term
t of ~(VNext Value
t) -> Value
t
eval Map Var Value
s (Term
t1 :<*>: Term
t2)    = case (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t1, Map Var Value -> Term -> Value
eval Map Var Value
s Term
t2) of ~(VNext (VAbs Value -> Value
f), VNext Value
t2) -> Value -> Value
VNext (Value -> Value
f Value
t2)
eval Map Var Value
s (Box Term
t)          = Value -> Value
VBox (Map Var Value -> Term -> Value
eval Map Var Value
s Term
t)
eval Map Var Value
s (Unbox Term
t)        = case Map Var Value -> Term -> Value
eval Map Var Value
s Term
t of ~(VBox Value
t) -> Value
t

-- * Printing

showSubst :: Map Var a -> Var
showSubst Map Var a
s = Var -> [Var] -> Var
forall a. [a] -> [[a]] -> [a]
intercalate Var
"; " [Var
v Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
" = " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ a -> Var
forall a. Show a => a -> Var
show a
t | (Var
v, a
t) <- Map Var a -> [(Var, a)]
forall k a. Map k a -> [(k, a)]
Map.assocs Map Var a
s]

pad :: Var -> Var
pad Var
"" = Var
""
pad Var
s = Var
" " Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
s Var -> Var -> Var
forall a. [a] -> [a] -> [a]
++ Var
" "

appPrec :: a
appPrec = a
10
plusPrec :: a
plusPrec = a
6

instance Show Term where
    showsPrec :: Int -> Term -> Var -> Var
showsPrec Int
_ (Var Var
x) = Var -> Var -> Var
showString Var
x
    showsPrec Int
_ (Int Integer
i) = Integer -> Var -> Var
forall a. Show a => a -> Var -> Var
shows Integer
i
    showsPrec Int
d (Term
t1 `Plus` Term
t2) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
plusPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec Int
forall {a}. Num a => a
plusPrec Term
t1 (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
" + " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
plusPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t2
    showsPrec Int
d (Term
t1 `Minus` Term
t2) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
plusPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec Int
forall {a}. Num a => a
plusPrec Term
t1 (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
" - " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
plusPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t2
    showsPrec Int
d (Term
t1 `Times` Term
t2) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
plusPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec Int
forall {a}. Num a => a
plusPrec Term
t1 (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
" * " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
plusPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t2
    showsPrec Int
d (Term
t1 `Divide` Term
t2) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
plusPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec Int
forall {a}. Num a => a
plusPrec Term
t1 (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
" / " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
plusPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t2
    showsPrec Int
_ Term
IntRec = Var -> Var -> Var
showString Var
"intrec"
    showsPrec Int
_ Term
Unit = Var -> Var -> Var
showString Var
"()"
    showsPrec Int
d (Pair Term
t1 Term
t2) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Term -> Var -> Var
forall a. Show a => a -> Var -> Var
shows Term
t1 (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
", " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (-Int
1) Term
t2
    showsPrec Int
d (Fst Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"fst " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t
    showsPrec Int
d (Snd Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"snd " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t
    showsPrec Int
d (Abort Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"abort " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t
    showsPrec Int
d (InL Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"left " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t
    showsPrec Int
d (InR Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"right " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t
    showsPrec Int
d (Case Term
t ~(Abs Var
x1 Term
t1) ~(Abs Var
x2 Term
t2)) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"case " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Var -> Var
forall a. Show a => a -> Var -> Var
shows Term
t (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
" of { left "
            (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
x1 (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
". " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Var -> Var
forall a. Show a => a -> Var -> Var
shows Term
t1
            (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
"; right "
            (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
x2 (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
". " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Var -> Var
forall a. Show a => a -> Var -> Var
shows Term
t2
            (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
" }"
    showsPrec Int
d (Abs Var
x Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Char -> Var -> Var
showChar Char
'\\' (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
x (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
". " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Var -> Var
forall a. Show a => a -> Var -> Var
shows Term
t
    showsPrec Int
d (Term
t1 :$: Term
t2) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec Int
forall {a}. Num a => a
appPrec Term
t1 (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Var -> Var
showChar Char
' ' (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t2
    showsPrec Int
d (Let Subst
s Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"let {" (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString (Var -> Var
pad (Subst -> Var
forall {a}. Show a => Map Var a -> Var
showSubst Subst
s)) (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
"} in " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Var -> Var
forall a. Show a => a -> Var -> Var
shows Term
t
    showsPrec Int
d (Fold Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"fold " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t
    showsPrec Int
d (Unfold Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"unfold " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t
    showsPrec Int
d (Fix ~(Abs Var
x Term
t)) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"fix " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
x (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
". " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Var -> Var
forall a. Show a => a -> Var -> Var
shows Term
t
    showsPrec Int
d (Next Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"next " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t
    showsPrec Int
d (Prev Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"prev " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t
    showsPrec Int
d (Term
t1 :<*>: Term
t2) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
prec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec Int
forall {a}. Num a => a
prec Term
t1 (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
" <*> " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
prec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t2
        where prec :: a
prec = a
4
    showsPrec Int
d (Box Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"box " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t
    showsPrec Int
d (Unbox Term
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"unbox " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Term
t

instance Show Value where
    showsPrec :: Int -> Value -> Var -> Var
showsPrec Int
_ (VInt Integer
i) = Integer -> Var -> Var
forall a. Show a => a -> Var -> Var
shows Integer
i
    showsPrec Int
_ Value
VUnit = Var -> Var -> Var
showString Var
"()"
    showsPrec Int
d (VPair Value
t1 Value
t2) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Value -> Var -> Var
forall a. Show a => a -> Var -> Var
shows Value
t1 (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Var -> Var
showString Var
", " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Value -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (-Int
1) Value
t2
    showsPrec Int
d (VInL Value
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"left " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Value -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Value
t
    showsPrec Int
d (VInR Value
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"right " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Value -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Value
t
    showsPrec Int
_ (VAbs Value -> Value
_) = Var -> Var -> Var
showString Var
"<function>"
    showsPrec Int
d (VFold Value
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"fold " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Value -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Value
t
    showsPrec Int
d (VNext Value
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"next " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Value -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Value
t
    showsPrec Int
d (VBox Value
t) = Bool -> (Var -> Var) -> Var -> Var
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
forall {a}. Num a => a
appPrec) ((Var -> Var) -> Var -> Var) -> (Var -> Var) -> Var -> Var
forall a b. (a -> b) -> a -> b
$
        Var -> Var -> Var
showString Var
"box " (Var -> Var) -> (Var -> Var) -> Var -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Value -> Var -> Var
forall a. Show a => Int -> a -> Var -> Var
showsPrec (Int
forall {a}. Num a => a
appPrec Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Value
t

-- * Parsing

variable :: Parser Var
variable :: Parser Var
variable = [Var] -> Parser Var
mkIdentifier
    [Var
"intrec", Var
"fst", Var
"snd", Var
"left", Var
"right", Var
"case", Var
"of", Var
"let", Var
"fold", Var
"unfold",
     Var
"fix", Var
"next", Var
"prev", Var
"box", Var
"unbox", Var
"in", Var
"type"]

term :: Parser Term
term :: Parser Term
term = [Parser Term] -> Parser Term
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice [Parser Term
abs_, Parser Term
fix_, Parser Term
case_, Parser Term
letIn, Parser Term
-> [[Operator (ReaderT IndentRef (Parsec Void Var)) Term]]
-> Parser Term
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser Parser Term
base [[Operator (ReaderT IndentRef (Parsec Void Var)) Term]]
ops] Parser Term -> Var -> Parser Term
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> Var -> m a
<?> Var
"term"
    where
    abs_ :: Parser Term
abs_ = (Term -> [Var] -> Term) -> [Var] -> Term -> Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Var -> Term -> Term) -> Term -> [Var] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var -> Term -> Term
Abs) ([Var] -> Term -> Term)
-> Parser Var
-> ReaderT IndentRef (Parsec Void Var) ([Var] -> Term -> Term)
forall a b.
a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser Var
lambda ReaderT IndentRef (Parsec Void Var) ([Var] -> Term -> Term)
-> ReaderT IndentRef (Parsec Void Var) [Var]
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term)
forall a b.
ReaderT IndentRef (Parsec Void Var) (a -> b)
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Var -> ReaderT IndentRef (Parsec Void Var) [Var]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser Var
variable ReaderT IndentRef (Parsec Void Var) (Term -> Term)
-> Parser Var -> ReaderT IndentRef (Parsec Void Var) (Term -> Term)
forall a b.
ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Var
dot ReaderT IndentRef (Parsec Void Var) (Term -> Term)
-> Parser Term -> Parser Term
forall a b.
ReaderT IndentRef (Parsec Void Var) (a -> b)
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Term
term
    fix_ :: Parser Term
fix_ = Term -> Term
Fix (Term -> Term) -> Parser Term -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term -> [Var] -> Term) -> [Var] -> Term -> Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Var -> Term -> Term) -> Term -> [Var] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var -> Term -> Term
Abs) ([Var] -> Term -> Term)
-> Parser Var
-> ReaderT IndentRef (Parsec Void Var) ([Var] -> Term -> Term)
forall a b.
a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser Var
"fix" ReaderT IndentRef (Parsec Void Var) ([Var] -> Term -> Term)
-> ReaderT IndentRef (Parsec Void Var) [Var]
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term)
forall a b.
ReaderT IndentRef (Parsec Void Var) (a -> b)
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Var -> ReaderT IndentRef (Parsec Void Var) [Var]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser Var
variable ReaderT IndentRef (Parsec Void Var) (Term -> Term)
-> Parser Var -> ReaderT IndentRef (Parsec Void Var) (Term -> Term)
forall a b.
ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Var
dot ReaderT IndentRef (Parsec Void Var) (Term -> Term)
-> Parser Term -> Parser Term
forall a b.
ReaderT IndentRef (Parsec Void Var) (a -> b)
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Term
term)
    case_ :: Parser Term
case_ = do
        Parser Var
"case"; Term
t <- Parser Term
term; Parser Var
"of"
        Parser Term -> Parser Term
forall a. Parser a -> Parser a
braces do
            Parser Var
"left"; Var
x1 <- Parser Var
variable; Parser Var
dot; Term
t1 <- Parser Term
term
            Parser Var
semicolon
            Parser Var
"right"; Var
x2 <- Parser Var
variable; Parser Var
dot; Term
t2 <- Parser Term
term
            pure $ Term -> Term -> Term -> Term
Case Term
t (Var -> Term -> Term
Abs Var
x1 Term
t1) (Var -> Term -> Term
Abs Var
x2 Term
t2)
    letIn :: Parser Term
letIn = Subst -> Term -> Term
Let (Subst -> Term -> Term)
-> Parser Var
-> ReaderT IndentRef (Parsec Void Var) (Subst -> Term -> Term)
forall a b.
a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser Var
"let" ReaderT IndentRef (Parsec Void Var) (Subst -> Term -> Term)
-> ReaderT IndentRef (Parsec Void Var) Subst
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term)
forall a b.
ReaderT IndentRef (Parsec Void Var) (a -> b)
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT IndentRef (Parsec Void Var) Subst
-> ReaderT IndentRef (Parsec Void Var) Subst
forall a. Parser a -> Parser a
braces ReaderT IndentRef (Parsec Void Var) Subst
subst ReaderT IndentRef (Parsec Void Var) (Term -> Term)
-> Parser Var -> ReaderT IndentRef (Parsec Void Var) (Term -> Term)
forall a b.
ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Var
"in" ReaderT IndentRef (Parsec Void Var) (Term -> Term)
-> Parser Term -> Parser Term
forall a b.
ReaderT IndentRef (Parsec Void Var) (a -> b)
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Term
term
    base :: Parser Term
base =  Var -> Term
Var (Var -> Term) -> Parser Var -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Var
variable
        Parser Term -> Parser Term -> Parser Term
forall a.
ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Integer -> Term
Int (Integer -> Term)
-> ReaderT IndentRef (Parsec Void Var) Integer -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT IndentRef (Parsec Void Var) Integer
number
        Parser Term -> Parser Term -> Parser Term
forall a.
ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term
IntRec Term -> Parser Var -> Parser Term
forall a b.
a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser Var
"intrec"
        Parser Term -> Parser Term -> Parser Term
forall a.
ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Term -> Parser Term
forall a. Parser a -> Parser a
parens ([Term] -> Term
tuple ([Term] -> Term)
-> ReaderT IndentRef (Parsec Void Var) [Term] -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
term Parser Term
-> Parser Var -> ReaderT IndentRef (Parsec Void Var) [Term]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser Var
comma)
    tuple :: [Term] -> Term
tuple [] = Term
Unit
    tuple [Term
t] = Term
t
    tuple (Term
t : [Term]
ts) = Term -> Term -> Term
Pair Term
t ([Term] -> Term
tuple [Term]
ts)
    unaries :: [(a, Term -> Term)]
unaries = [(a
"fst", Term -> Term
Fst), (a
"snd", Term -> Term
Snd), (a
"abort", Term -> Term
Abort), (a
"left", Term -> Term
InL), (a
"right", Term -> Term
InR),
               (a
"fold", Term -> Term
Fold), (a
"unfold", Term -> Term
Unfold), (a
"next", Term -> Term
Next), (a
"prev", Term -> Term
Prev),
               (a
"box", Term -> Term
Box), (a
"unbox", Term -> Term
Unbox)]
    unary :: ReaderT IndentRef (Parsec Void Var) (Term -> Term)
unary = [ReaderT IndentRef (Parsec Void Var) (Term -> Term)]
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term)
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice [Term -> Term
f (Term -> Term)
-> Parser Var -> ReaderT IndentRef (Parsec Void Var) (Term -> Term)
forall a b.
a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser Var -> Parser Var
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
hidden (Var -> Parser Var
keyword Var
w) | (Var
w, Term -> Term
f) <- [(Var, Term -> Term)]
forall {a}. IsString a => [(a, Term -> Term)]
unaries]
    ops :: [[Operator (ReaderT IndentRef (Parsec Void Var)) Term]]
ops = [ [ ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
-> Operator (ReaderT IndentRef (Parsec Void Var)) Term
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL ((Term -> Term -> Term)
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
forall a. a -> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term -> Term -> Term
(:$:))
            , ReaderT IndentRef (Parsec Void Var) (Term -> Term)
-> Operator (ReaderT IndentRef (Parsec Void Var)) Term
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (((Term -> Term) -> (Term -> Term) -> Term -> Term)
-> [Term -> Term] -> Term -> Term
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ([Term -> Term] -> Term -> Term)
-> ReaderT IndentRef (Parsec Void Var) [Term -> Term]
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT IndentRef (Parsec Void Var) (Term -> Term)
-> ReaderT IndentRef (Parsec Void Var) [Term -> Term]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some ReaderT IndentRef (Parsec Void Var) (Term -> Term)
unary) ]
          , [ ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
-> Operator (ReaderT IndentRef (Parsec Void Var)) Term
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL (Term -> Term -> Term
Plus (Term -> Term -> Term)
-> Parser Var
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
forall a b.
a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> Parser Var
symbol Var
"+"), ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
-> Operator (ReaderT IndentRef (Parsec Void Var)) Term
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL (Term -> Term -> Term
Minus (Term -> Term -> Term)
-> Parser Var
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
forall a b.
a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> Parser Var
symbol Var
"-")
            , ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
-> Operator (ReaderT IndentRef (Parsec Void Var)) Term
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL (Term -> Term -> Term
Times (Term -> Term -> Term)
-> Parser Var
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
forall a b.
a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> Parser Var
symbol Var
"*"), ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
-> Operator (ReaderT IndentRef (Parsec Void Var)) Term
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL (Term -> Term -> Term
Divide (Term -> Term -> Term)
-> Parser Var
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
forall a b.
a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> Parser Var
symbol Var
"/") ]
          , [ ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
-> Operator (ReaderT IndentRef (Parsec Void Var)) Term
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL (Term -> Term -> Term
(:<*>:)        (Term -> Term -> Term)
-> Parser Var
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
forall a b.
a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (Var -> Parser Var
symbol Var
"<*>" Parser Var -> Parser Var -> Parser Var
forall a.
ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Var -> Parser Var
symbol Var
"⊛"))
            , ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
-> Operator (ReaderT IndentRef (Parsec Void Var)) Term
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL (Term -> Term -> Term
(:<*>:) (Term -> Term -> Term) -> (Term -> Term) -> Term -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
Next (Term -> Term -> Term)
-> Parser Var
-> ReaderT IndentRef (Parsec Void Var) (Term -> Term -> Term)
forall a b.
a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Var -> Parser Var
symbol Var
"<$>") ] ]

binding :: Parser (Var, Term)
binding :: Parser (Var, Term)
binding = ReaderT IndentRef (Parsec Void Var) (Term -> (Var, Term))
-> ReaderT IndentRef (Parsec Void Var) (Term -> (Var, Term))
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Var -> [Var] -> Term -> (Var, Term)
forall {t :: * -> *}.
Foldable t =>
Var -> t Var -> Term -> (Var, Term)
mkBinding (Var -> [Var] -> Term -> (Var, Term))
-> Parser Var
-> ReaderT
     IndentRef (Parsec Void Var) ([Var] -> Term -> (Var, Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Var
variable ReaderT IndentRef (Parsec Void Var) ([Var] -> Term -> (Var, Term))
-> ReaderT IndentRef (Parsec Void Var) [Var]
-> ReaderT IndentRef (Parsec Void Var) (Term -> (Var, Term))
forall a b.
ReaderT IndentRef (Parsec Void Var) (a -> b)
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Var -> ReaderT IndentRef (Parsec Void Var) [Var]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Var
variable ReaderT IndentRef (Parsec Void Var) (Term -> (Var, Term))
-> Parser Var
-> ReaderT IndentRef (Parsec Void Var) (Term -> (Var, Term))
forall a b.
ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
-> ReaderT IndentRef (Parsec Void Var) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Var
equal) ReaderT IndentRef (Parsec Void Var) (Term -> (Var, Term))
-> Parser Term -> Parser (Var, Term)
forall a b.
ReaderT IndentRef (Parsec Void Var) (a -> b)
-> ReaderT IndentRef (Parsec Void Var) a
-> ReaderT IndentRef (Parsec Void Var) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Term
term
    where
    mkBinding :: Var -> t Var -> Term -> (Var, Term)
mkBinding Var
x t Var
ys Term
t = (Var
x, Var -> Term -> Term
autoFix Var
x ((Var -> Term -> Term) -> Term -> t Var -> Term
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Var -> Term -> Term
Abs Term
t t Var
ys))
    autoFix :: Var -> Term -> Term
autoFix Var
x Term
t | Var
x Var -> Term -> Bool
`freeIn` Term
t = Term -> Term
Fix (Var -> Term -> Term
Abs Var
x Term
t)
                | Bool
otherwise    = Term
t

subst :: Parser Subst
subst :: ReaderT IndentRef (Parsec Void Var) Subst
subst = [(Var, Term)] -> Subst
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Var, Term)] -> Subst)
-> ReaderT IndentRef (Parsec Void Var) [(Var, Term)]
-> ReaderT IndentRef (Parsec Void Var) Subst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Var, Term)
binding Parser (Var, Term)
-> Parser Var -> ReaderT IndentRef (Parsec Void Var) [(Var, Term)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser Var
semicolon