Meta.bruijn

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

:import std/Logic .
:import std/Combinator .
:import std/List .
:import std/Number/Unary .
:import std/Number/Pairing .
:import std/Number/Conversion .
:import std/Pair P

# 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 blc index to meta index + rest
blc→unary+rest y [[[rec]]] (+0u) ⧗ (List LcBit) → (Pair Meta (List LcBit))
	rec 0 [[1 case-end case-rec]]
		case-rec 4 ++3 0
		case-end (idx --3) : 0

:test (blc→unary+rest (blc1 : {}blc0)) (`0 : [[0]])
:test (blc→unary+rest (blc1 : (blc1 : {}blc0))) (`1 : [[0]])
:test (blc→unary+rest (blc1 : (blc1 : (blc1 : {}blc0)))) (`2 : [[0]])
:test (blc→unary+rest (blc1 : (blc1 : (blc1 : (blc0 : {}blc1))))) (`2 : {}blc1)

# converts blc list to meta term
# TODO: use CSP instead?
blc→meta+rest y [[rec]] ⧗ (List LcBit) → (Pair Meta (List LcBit))
	rec 0 [[1 case-0 case-1]]
		case-0 ^0 case-00 case-01 
			case-00 3 ~0 [[(abs 1) : 0]]
			case-01 3 ~0 [[5 0 [[(app 3 1) : 0]]]]
		case-1 blc→unary+rest 2

blc→meta head ∘ blc→meta+rest ⧗ (List LcBit) → Meta

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

# converts meta term to blc list
meta→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 (meta→blc `[0]) (blc0 : (blc0 : (blc1 : {}blc0)))
:test (meta→blc `[[1 1]]) (blc0 : (blc0 : (blc0 : (blc0 : (blc0 : (blc1 : (blc1 : (blc1 : (blc0 : (blc1 : (blc1 : {}blc0)))))))))))
:test (blc→meta (meta→blc `meta→blc)) (`meta→blc)

α-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]]] &Ω ⧗ (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 ∘ meta→blc ⧗ Meta → a

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

!‣ eval

: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])

# set lhs of meta application
lhs [[1 i [[[[1 4 2]]]]]] ⧗ Meta → Meta → Meta

:test (lhs `(1 0) `0) (`(0 0))

# set rhs of meta application
rhs [[1 i [[[[1 3 4]]]]]] ⧗ Meta → Meta → Meta

:test (rhs `(0 1) `0) (`(0 0))

# swap terms of meta application
swap [0 i [[[[1 2 3]]]]] ⧗ Meta → Meta

:test (swap `(1 0)) (`(0 1))

# applies a function to the body of a meta term
map [[0 case-idx case-app case-abs]] ⧗ (Meta → Meta) → Meta → Meta
	case-idx [idx (2 0)]
	case-app [[app (3 1 0)]]
	case-abs [abs (2 0)]

:test (map swap `[0 1]) (`[1 0])
:test (map inc `0) (`1)
:test (map (map inc) `[0]) (`[1])

# encodes meta terms as ternary number
# inspired by Helmut Brandl's and Steve Goguen's work
# uses ternary for lower space complexity
encode fold idx-cb app-cb abs-cb ⧗ Meta → Number
	idx-cb (pair-ternary (+0)) ∘ unary→ternary
	app-cb (pair-ternary (+1)) ∘∘ pair-ternary
	abs-cb pair-ternary (+2)

:test (ternary→unary (encode `0)) ((+0u))
:test (ternary→unary (encode `1)) ((+1u))
:test (ternary→unary (encode `(0 0))) ((+3u))
:test (ternary→unary (encode `[1])) ((+7u))
:test (ternary→unary (encode `[0])) ((+8u))

# decodes ternary encoding back to meta term
# TODO: improve performance (maybe with different unpairing function or better sqrt)
decode y [[unpair-ternary 0 go]] ⧗ Number → Meta
	go [[(case-idx : (case-app : {}case-abs)) !! 1 0]]
		case-idx idx ∘ ternary→unary
		case-app [unpair-ternary 0 (app ⋔ 4)]
		case-abs abs ∘ 3

:test (decode (+0)) (`0)
:test (decode (+1)) (`1)
:test (decode (+3)) (`(0 0))
:test (decode (+7)) (`[1])
:test (decode (+8)) (`[0])