-- | Type checking and type inference
module L3.Core.Normal (free, fresh, substitute, normalize, normalize0) where

import Data.Char (isDigit)
import Data.List (intercalate)
import L3.Core.Expr
import L3.Core.Show
import L3.Log
import L3.Util

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

-- | Is a name 'free' in an expression
--  In this context, free v a & v /= v'  =>  substitute v v' a /= a
--  i.e. would a substitution be performed
free :: (Eq a, Show a) => a -> Expr a -> Bool
free :: a -> Expr a -> Bool
free a
v Expr a
e = String -> Bool -> Bool
forall a. String -> a -> a
trace (String
"free " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v 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) (a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free' a
v Expr a
e)

free' :: a -> Expr a -> Bool
free' a
v (Var a
v') = a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v'
free' a
v (Lam a
v' Expr a
ta Expr a
_) | a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v' = a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free a
v Expr a
ta
free' a
v (Lam a
_ Expr a
ta Expr a
b) = a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free a
v Expr a
ta Bool -> Bool -> Bool
|| a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free a
v Expr a
b
free' a
v (Pi a
v' Expr a
ta Expr a
_) | a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v' = a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free a
v Expr a
ta
free' a
v (Pi a
_ Expr a
ta Expr a
tb) = a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free a
v Expr a
ta Bool -> Bool -> Bool
|| a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free a
v Expr a
tb
free' a
v (App Expr a
f Expr a
a) = a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free a
v Expr a
f Bool -> Bool -> Bool
|| a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free a
v Expr a
a
free' a
_ Expr a
_ = Bool
False

fresh :: (Eq a, Enum a, Show a) => a -> Expr a -> a
fresh :: a -> Expr a -> a
fresh a
v Expr a
e = String -> a -> a
forall a. String -> a -> a
trace (String
"fresh " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v 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) (a -> Expr a -> a
forall a. (Eq a, Show a, Enum a) => a -> Expr a -> a
fresh' a
v Expr a
e)

fresh' :: a -> Expr a -> a
fresh' a
from Expr a
expr = a
v
  where
    enums :: t -> [t]
enums t
e = t -> t
forall a. Enum a => a -> a
succ t
e t -> [t] -> [t]
forall a. a -> [a] -> [a]
: t -> [t]
enums (t -> t
forall a. Enum a => a -> a
succ t
e)
    nonfree :: [a]
nonfree = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (a -> Bool) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
`free` Expr a
expr)) (a -> [a]
forall t. Enum t => t -> [t]
enums a
from)
    v :: a
v = [a] -> a
forall a. [a] -> a
head [a]
nonfree

-- | Substitute all occurrences of a variable v with an expression e.
--  substitute v e E  ~  E[v := e]
substitute :: (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute :: a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
e' = String -> Expr a -> Expr a
forall a. String -> a -> a
trace (String
"substitute " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v 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 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') (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute' a
v Expr a
e Expr a
e')

substitute' :: a -> Expr a -> Expr a -> Expr a
substitute' a
v Expr a
e (Var a
v') | a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v' = Expr a
e
substitute' a
v Expr a
e (Lam a
v' Expr a
ta Expr a
b) | a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v' = a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Lam a
v' (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
ta) Expr a
b
substitute' a
v Expr a
e (Lam a
v' Expr a
ta Expr a
b) | a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free a
v' Expr a
e = a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e (a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Lam a
v'' Expr a
ta (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v' (a -> Expr a
forall a. a -> Expr a
Var a
v'') Expr a
b))
  where
    v'' :: a
v'' = a -> Expr a -> a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> a
fresh a
v' Expr a
b
substitute' a
v Expr a
e (Lam a
v' Expr a
ta Expr a
b) = a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Lam a
v' (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
ta) (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
b)
substitute' a
v Expr a
e (Pi a
v' Expr a
ta Expr a
tb) | a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v' = a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Pi a
v' (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
ta) Expr a
tb
substitute' a
v Expr a
e (Pi a
v' Expr a
ta Expr a
tb) | a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free a
v' Expr a
e = a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e (a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Pi a
v'' Expr a
ta (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v' (a -> Expr a
forall a. a -> Expr a
Var a
v'') Expr a
tb))
  where
    v'' :: a
v'' = a -> Expr a -> a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> a
fresh a
v' Expr a
tb
substitute' a
v Expr a
e (Pi a
v' Expr a
ta Expr a
tb) = a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Pi a
v' (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
ta) (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
tb)
substitute' a
v Expr a
e (App Expr a
f Expr a
a) = Expr a -> Expr a -> Expr a
forall a. Expr a -> Expr a -> Expr a
App (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
f) (a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v Expr a
e Expr a
a)
substitute' a
_ Expr a
_ Expr a
e' = Expr a
e'

-- | Given an expression, reduce it one step towards its normal form.
normalize :: (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize :: Expr a -> Expr a
normalize Expr a
e = String -> Expr a -> Expr a
forall a. String -> a -> a
trace (String
"normalize " 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
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize' Expr a
e)

normalize' :: Expr a -> Expr a
normalize' (Lam a
v Expr a
ta Expr a
b) = case Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize Expr a
b of
  App Expr a
vb (Var a
v') | a
v a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
v' Bool -> Bool -> Bool
&& Bool -> Bool
not (a -> Expr a -> Bool
forall a. (Eq a, Show a) => a -> Expr a -> Bool
free a
v Expr a
vb) -> Expr a
vb -- ε-reduction
  Expr a
b' -> a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Lam a
v (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize Expr a
ta) (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize Expr a
b')
normalize' (Pi a
v Expr a
ta Expr a
tb) = a -> Expr a -> Expr a -> Expr a
forall a. a -> Expr a -> Expr a -> Expr a
Pi a
v (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize Expr a
ta) (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize Expr a
tb)
normalize' (App Expr a
f Expr a
a) = case Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize Expr a
f of
  Lam a
v Expr a
_ Expr a
b -> a -> Expr a -> Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute a
v (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize Expr a
a) Expr a
b
  Expr a
f' -> Expr a -> Expr a -> Expr a
forall a. Expr a -> Expr a -> Expr a
App Expr a
f' (Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize Expr a
a)
normalize' Expr a
c = Expr a
c

-- | Given an expression, totally reduce it over all steps towards normal form.
normalize0 :: (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize0 :: Expr a -> Expr a
normalize0 Expr a
e = String -> Expr a -> Expr a
forall a. String -> a -> a
trace (String
"normalize0 " 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
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize0' Expr a
e)

normalize0' :: Expr a -> Expr a
normalize0' Expr a
e = case Expr a -> Expr a
forall a. (Eq a, Enum a, Show a) => Expr a -> Expr a
normalize Expr a
e of
  Expr a
e' | Expr a
e Expr a -> Expr a -> Bool
forall a. Eq a => a -> a -> Bool
== Expr a
e' -> 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'