# MIT License, Copyright (c) 2023 Marvin Borner
# utilities for meta programming with quoted terms

:import std/Logic .
:import std/Combinator .
:import std/Number/Unary .
:import std/List .

# constructor of meta abstraction
abs [[[[0 3]]]] ⧗ Meta → Meta

:test (abs `0) (`[0])

# true if abstraction
abs? [0 [false] [[false]] [true]] ⧗ Meta → Bool

:test (abs? `[0]) (true)
:test (abs? `([0] [0])) (false)
:test (abs? `0) (false)

# extracts meta term from meta abstraction
abs! [0 0 0 [0]] ⧗ Meta → Meta

:test (abs! `[[0]]) (`[0])

# constructor of meta application
app [[[[[1 4 3]]]]] ⧗ Meta → Meta → Meta

:test (app `[[1]] `[0]) (`([[1]] [0]))

# true if application
app? [0 [false] [[true]] [false]] ⧗ Meta → Bool

:test (app? `[0]) (false)
:test (app? `([0] [0])) (true)
:test (app? `0) (false)

# extracts both meta terms from meta application
app! [0 0 cons 0] ⧗ Meta → (Pair Meta Meta)

:test (app! `([[1]] [[0]])) (`[[1]] : `[[0]])

# extracts lhs meta term from meta application
app-lhs! ^‣ ∘ app! ⧗ Meta → Meta

:test (app-lhs! `([[1]] [[0]])) (`[[1]])

# extracts rhs meta term from meta application
app-rhs! ~‣ ∘ app! ⧗ Meta → Meta

:test (app-rhs! `([[1]] [[0]])) (`[[0]])

# constructor of meta variable/index
idx [[[[2 3]]]] ⧗ Unary → Meta

:test (idx (+0u)) (`0)

# true if variable/index
idx? [0 [true] [[false]] [false]] ⧗ Meta → Bool

:test (idx? `[0]) (false)
:test (idx? `([0] [0])) (false)
:test (idx? `0) (true)

# extracts index from meta index
idx! [0 [0] 0 0] ⧗ Meta → Unary

:test (idx! `0) ((+0u))
:test (idx! `3) ((+3u))

# traverses meta term
fold y [[[[[rec]]]]] ⧗ (Unary → a) → (a → a → a) → (a → a) → Meta → a
	rec 0 case-idx case-app case-abs
		case-idx 3
		case-app ψ 2 (4 3 2 1)
		case-abs 1 ∘ (4 3 2 1)

# calculates blc length of meta term
length fold idx-cb app-cb abs-cb ⧗ Meta → Unary
	idx-cb add (+2u)
	app-cb (add (+2u)) ∘∘ add
	abs-cb add (+2u)

:test (length `[0]) ((+4u))
:test (length `[[1 1]]) ((+12u))

# true bit
blc1 [[0]] ⧗ LcBit

# false bit
blc0 [[1]] ⧗ LcBit

# converts meta term to blc list
blc fold idx-cb app-cb abs-cb ⧗ Meta → (List LcBit)
	idx-cb [++0 (cons blc1) {}blc0]
	app-cb (cons blc0) ∘ (cons blc1) ∘∘ append
	abs-cb (cons blc0) ∘ (cons blc0)

:test (blc `[0]) (blc0 : (blc0 : (blc1 : {}blc0)))
:test (blc `[[1 1]]) (blc0 : (blc0 : (blc0 : (blc0 : (blc0 : (blc1 : (blc1 : (blc1 : (blc0 : (blc1 : (blc1 : {}blc0)))))))))))

α-eq? y [[[rec]]] ⧗ Meta → Meta → Bool
	rec 1 case-idx case-app case-abs
		case-idx [(idx? 1) (0 =? (idx! 1)) false]
		case-app [[(app? 2) (app! 2 [[(6 3 1) ⋀? (6 2 0)]]) false]]
		case-abs [(abs? 1) (3 (abs! 1) 0) false]

:test (α-eq? `0 `1) (false)
:test (α-eq? `1 `1) (true)
:test (α-eq? `(0 0) `1) (false)
:test (α-eq? `(0 0) `(1 0)) (false)
:test (α-eq? `(0 0) `(0 0)) (true)
:test (α-eq? `(0 1) `(0 1)) (true)
:test (α-eq? `[0] `[1]) (false)
:test (α-eq? `[0] `[0]) (true)
:test (α-eq? `α-eq? `α-eq?) (true)

# modified Tromp 232 bit universal machine
eval-blc y [[[rec]]] [0 Ω] ⧗ (List LcBit) → a
	rec 0 [[0 [2 case-0 case-1]]]
		case-0 5 [1 case-00 case-01]
			case-00 5 [[2 (0 : 1)]]
			case-01 6 [6 [2 0 (1 0)]]
		case-1 0 case-10 case-11
			case-10 4 head
			case-11 [6 [6 [1 ~0]] 2]

eval eval-blc ∘ blc ⧗ Meta → Meta

# self interpreter for meta encoding
eval y [[[rec]]] [0 Ω] ⧗ Meta → a
	rec 0 case-idx case-app case-abs
		case-idx [2 [head (1 tail 0)]]
		case-app 2 [3 [3 [2 0 (1 0)]]]
		case-abs 2 [2 [[2 (0 : 1)]]]

:test (eval `[(α-eq? `α-eq? `α-eq?)]) (true)

:test (!`(α-eq? `α-eq? `α-eq?)) (true)
:test (!`((+21u) + (+21u))) ((+42u))

# increments indices reaching out of their abstraction depth
κ y [[[rec]]] ⧗ Meta → Unary → Meta
	rec 1 case-idx case-app case-abs
		case-idx [idx ((1 >? 0) 0 ++0)]
		case-app [[app (4 1 2) (4 0 2)]]
		case-abs [abs (3 0 ++1)]

:test (κ `0 (+1u)) (`0)
:test (κ `0 (+0u)) (`1)
:test (κ `1 (+0u)) (`2)
:test (κ `[0] (+0u)) (`[0])
:test (κ `[1] (+0u)) (`[2])
:test (κ `[2] (+1u)) (`[3])
:test (κ `(1 0) (+1u)) (`(2 0))

# substitutes term based on unary abstraction depth
σ y [[[[rec]]]] ⧗ Meta → Meta → Unary → Meta
	rec 2 case-idx case-app case-abs
		case-idx [compare-case case-eq case-lt case-gt 1 0]
			case-eq 2
			case-lt idx 0
			case-gt idx --0
		case-app [[app (5 1 3 2) (5 0 3 2)]]
		case-abs [abs (4 0 (κ 2 (+0u)) ++1)]

:test (σ `0 `2 (+0u)) (`2)
:test (σ `[1] `2 (+0u)) (`[3])
:test (σ `[[4 0]] `2 (+1u)) (`[[3 0]])
:test (σ `[[3] [3]] `0 (+0u)) (`[[2] [2]])

# reduces given term to its normal form
β* y [[rec]] ⧗ Meta → Meta
	rec 0 case-idx case-app case-abs
		case-idx idx
		case-app [[(3 1) case-idx case-app case-abs]]
			case-idx [app (idx 0) (4 1)]
			case-app [[app (app 1 0) (5 2)]]
			case-abs [4 (σ 0 1 (+0u))]
		case-abs [abs (2 0)]

:test (β* `0) (`0)
:test (β* `[0]) (`[0])
:test (β* `([0] [0])) (`[0])
:test (β* `(++(+2u))) (`(+3u))

# single-pass beta reduction
β y [[rec]] ⧗ Meta → Meta
	rec 0 case-idx case-app case-abs
		case-idx idx
		case-app [[abs? 1 redex normal]]
			redex σ (abs! 1) 0 (+0u)
			normal app 1 (3 0)
		case-abs [abs (2 0)]
		case-ass abs ∘ 2

:test (β `0) (`0)
:test (β `[0]) (`[0])
:test (β `([0] [0])) (`[0])

# TODO!
test [`(0 + (+1u))]

# :test (!(test (+3u))) ((+4u))