-- | Type checking and type inference
module L3.Core.DeBruijn (index, index0) where

import Data.Char (isDigit)
import Data.List (intercalate)
import L3.Core.Expr
import L3.Core.Normal
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::DeBruijn"

-- | Given an 'free' index, convert an expression in Right names into Left indexes.
--  This uses DeBruijn indicies.
index :: (Eq a, Enum a, Show a) => Int -> Expr (Either Int a) -> Expr (Either Int a)
index :: Int -> Expr (Either Int a) -> Expr (Either Int a)
index Int
i Expr (Either Int a)
e = String -> Expr (Either Int a) -> Expr (Either Int a)
forall a. String -> a -> a
trace (String
"index " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr (Either Int a) -> String
forall a. Show a => a -> String
show Expr (Either Int a)
e) (Int -> Expr (Either Int a) -> Expr (Either Int a)
forall a.
(Eq a, Enum a, Show a) =>
Int -> Expr (Either Int a) -> Expr (Either Int a)
index' Int
i Expr (Either Int a)
e)

index' :: Int -> Expr (Either Int a) -> Expr (Either Int a)
index' Int
_ (Var Either Int a
v) = Either Int a -> Expr (Either Int a)
forall a. a -> Expr a
Var Either Int a
v
index' Int
i (Lam Either Int a
v Expr (Either Int a)
ta Expr (Either Int a)
b) = Either Int a
-> Expr (Either Int a)
-> Expr (Either Int a)
-> Expr (Either Int a)
forall a. a -> Expr a -> Expr a -> Expr a
Lam (Int -> Either Int a
forall a b. a -> Either a b
Left Int
i) (Int -> Expr (Either Int a) -> Expr (Either Int a)
forall a.
(Eq a, Enum a, Show a) =>
Int -> Expr (Either Int a) -> Expr (Either Int a)
index Int
i Expr (Either Int a)
ta) (Int -> Expr (Either Int a) -> Expr (Either Int a)
forall a.
(Eq a, Enum a, Show a) =>
Int -> Expr (Either Int a) -> Expr (Either Int a)
index (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Expr (Either Int a) -> Expr (Either Int a))
-> Expr (Either Int a) -> Expr (Either Int a)
forall a b. (a -> b) -> a -> b
$ Either Int a
-> Expr (Either Int a)
-> Expr (Either Int a)
-> Expr (Either Int a)
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute Either Int a
v (Either Int a -> Expr (Either Int a)
forall a. a -> Expr a
Var (Either Int a -> Expr (Either Int a))
-> Either Int a -> Expr (Either Int a)
forall a b. (a -> b) -> a -> b
$ Int -> Either Int a
forall a b. a -> Either a b
Left Int
i) Expr (Either Int a)
b)
index' Int
i (Pi Either Int a
v Expr (Either Int a)
ta Expr (Either Int a)
tb) = Either Int a
-> Expr (Either Int a)
-> Expr (Either Int a)
-> Expr (Either Int a)
forall a. a -> Expr a -> Expr a -> Expr a
Pi (Int -> Either Int a
forall a b. a -> Either a b
Left Int
i) (Int -> Expr (Either Int a) -> Expr (Either Int a)
forall a.
(Eq a, Enum a, Show a) =>
Int -> Expr (Either Int a) -> Expr (Either Int a)
index Int
i Expr (Either Int a)
ta) (Int -> Expr (Either Int a) -> Expr (Either Int a)
forall a.
(Eq a, Enum a, Show a) =>
Int -> Expr (Either Int a) -> Expr (Either Int a)
index (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Expr (Either Int a) -> Expr (Either Int a))
-> Expr (Either Int a) -> Expr (Either Int a)
forall a b. (a -> b) -> a -> b
$ Either Int a
-> Expr (Either Int a)
-> Expr (Either Int a)
-> Expr (Either Int a)
forall a. (Eq a, Enum a, Show a) => a -> Expr a -> Expr a -> Expr a
substitute Either Int a
v (Either Int a -> Expr (Either Int a)
forall a. a -> Expr a
Var (Either Int a -> Expr (Either Int a))
-> Either Int a -> Expr (Either Int a)
forall a b. (a -> b) -> a -> b
$ Int -> Either Int a
forall a b. a -> Either a b
Left Int
i) Expr (Either Int a)
tb)
index' Int
i (App Expr (Either Int a)
f Expr (Either Int a)
a) = Expr (Either Int a) -> Expr (Either Int a) -> Expr (Either Int a)
forall a. Expr a -> Expr a -> Expr a
App (Int -> Expr (Either Int a) -> Expr (Either Int a)
forall a.
(Eq a, Enum a, Show a) =>
Int -> Expr (Either Int a) -> Expr (Either Int a)
index Int
i Expr (Either Int a)
f) (Int -> Expr (Either Int a) -> Expr (Either Int a)
forall a.
(Eq a, Enum a, Show a) =>
Int -> Expr (Either Int a) -> Expr (Either Int a)
index Int
i Expr (Either Int a)
a)
index' Int
_ Expr (Either Int a)
Star = Expr (Either Int a)
forall a. Expr a
Star
index' Int
_ Expr (Either Int a)
Box = Expr (Either Int a)
forall a. Expr a
Box

-- | Provide an initial 'free' index of 0 and index an expression.
--  This converts any expression to its DeBruijn indexed form, leaving global
--  names untouched.
index0 :: (Eq a, Enum a, Show a) => Expr a -> Expr (Either Int a)
index0 :: Expr a -> Expr (Either Int a)
index0 Expr a
e = String -> Expr (Either Int a) -> Expr (Either Int a)
forall a. String -> a -> a
trace (String
"index0 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr a -> String
forall a. Show a => a -> String
show 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)

index0' :: Expr a -> Expr (Either Int a)
index0' Expr a
e = Int -> Expr (Either Int a) -> Expr (Either Int a)
forall a.
(Eq a, Enum a, Show a) =>
Int -> Expr (Either Int a) -> Expr (Either Int a)
index Int
0 ((a -> Either Int a) -> Expr a -> Expr (Either Int a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Either Int a
forall a b. b -> Either a b
Right Expr a
e)