-- | Type checking and type inference
module L3.Core.Eq (alphaEq, betaEq) where

import Data.Char (isDigit)
import Data.List (intercalate)
import L3.Core.DeBruijn
import L3.Core.Expr
import L3.Core.Normal
import L3.Log.Logging
import L3.Util

trace :: String -> a -> a
trace = String -> String -> a -> a
forall a. String -> String -> a -> a
traceU String
"Core::Eq"

-- | Deduce whether two expressions are equivalent by converting to indexed form
--  and checking for exact equality. This does not apply normalisation, so
--  represents only alpha-equivalence of expressions.
alphaEq :: (Eq a, Enum a, Show a) => Expr a -> Expr a -> Bool
alphaEq :: Expr a -> Expr a -> Bool
alphaEq Expr a
e Expr a
e' = String -> Bool -> Bool
forall a. String -> a -> a
trace (String
"alphaEq " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
forall a. Show a => a -> String
show Expr a
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
forall a. Show a => a -> String
show Expr a
e') (Expr a -> Expr a -> Bool
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a -> Bool
alphaEq' Expr a
e Expr a
e')

alphaEq' :: Expr a -> Expr a -> Bool
alphaEq' Expr a
e Expr a
e' = Expr a -> Expr (Either Int a)
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr (Either Int a)
index0 Expr a
e Expr (Either Int a) -> Expr (Either Int a) -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a -> Expr (Either Int a)
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr (Either Int a)
index0 Expr a
e'

-- | Deduce whether two expressions are equivalent by converting to indexed form
--  and checking for exact equality. This does apply normalisation, so represents
--  beta-equivalence (and implicitly alpha-equivalence) of expressions.
betaEq :: (Eq a, Enum a, Show a) => Expr a -> Expr a -> Bool
betaEq :: Expr a -> Expr a -> Bool
betaEq Expr a
e Expr a
e' = String -> Bool -> Bool
forall a. String -> a -> a
trace (String
"betaEq " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
forall a. Show a => a -> String
show Expr a
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
forall a. Show a => a -> String
show Expr a
e') (Expr a -> Expr a -> Bool
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a -> Bool
betaEq' Expr a
e Expr a
e')

betaEq' :: Expr a -> Expr a -> Bool
betaEq' Expr a
e Expr a
e' = Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize0 Expr a
e Expr a -> Expr a -> Bool
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a -> Bool
`alphaEq` Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize0 Expr a
e'