verified-purescript/TranspilerFinal.lean at main · straylight-software/verified-purescript · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
import Lean
open Lean

inductive PSExpr where
  | Var : String → PSExpr
  | Lam : String → PSExpr → PSExpr
  | App : PSExpr → PSExpr → PSExpr
  deriving Repr, BEq

def prettyPS : PSExpr → String
  | .Var n => n
  | .Lam arg body => s!"\\{arg} -> {prettyPS body}"
  | .App f arg =>
      let fStr := prettyPS f
      let argStr := prettyPS arg
      s!"{fStr} ({argStr})"

def identity : PSExpr :=
  PSExpr.Lam "x" (PSExpr.Var "x")

def compose : PSExpr :=
  PSExpr.Lam "f" (PSExpr.Lam "g" (PSExpr.Lam "x"
    (PSExpr.App (PSExpr.Var "f") (PSExpr.App (PSExpr.Var "g") (PSExpr.Var "x")))))

def churchTrue : PSExpr :=
  PSExpr.Lam "t" (PSExpr.Lam "f" (PSExpr.Var "t"))

def churchFalse : PSExpr :=
  PSExpr.Lam "f" (PSExpr.Lam "t" (PSExpr.Var "t"))

def churchAnd : PSExpr :=
  PSExpr.Lam "p" (PSExpr.Lam "q"
    (PSExpr.App (PSExpr.Var "p") (PSExpr.App (PSExpr.Var "q") churchFalse)))

-- Y combinator: λf. (λx. f (x x)) (λx. f (x x))
def Y : PSExpr :=
  let inner := PSExpr.Lam "x"
    (PSExpr.App (PSExpr.Var "f")
      (PSExpr.App (PSExpr.Var "x") (PSExpr.Var "x")))
  PSExpr.Lam "f" (PSExpr.App inner inner)

-- S combinator: λf. λg. λx. f x (g x)
def S : PSExpr :=
  PSExpr.Lam "f" (PSExpr.Lam "g" (PSExpr.Lam "x"
    (PSExpr.App
      (PSExpr.App (PSExpr.Var "f") (PSExpr.Var "x"))
      (PSExpr.App (PSExpr.Var "g") (PSExpr.Var "x")))))

-- K combinator: λx. λy. x
def K : PSExpr :=
  PSExpr.Lam "x" (PSExpr.Lam "_" (PSExpr.Var "x"))

-- I combinator: λx. x
def I : PSExpr :=
  PSExpr.Lam "x" (PSExpr.Var "x")

-- B combinator (composition): λf. λg. λx. f (g x)
def B : PSExpr :=
  PSExpr.Lam "f" (PSExpr.Lam "g" (PSExpr.Lam "x"
    (PSExpr.App (PSExpr.Var "f") (PSExpr.App (PSExpr.Var "g") (PSExpr.Var "x")))))

-- C combinator (flip): λf. λx. λy. f y x
def C : PSExpr :=
  PSExpr.Lam "f" (PSExpr.Lam "x" (PSExpr.Lam "y"
    (PSExpr.App (PSExpr.App (PSExpr.Var "f") (PSExpr.Var "y")) (PSExpr.Var "x"))))

-- ω (omega): λx. x x
def omega : PSExpr :=
  PSExpr.Lam "x" (PSExpr.App (PSExpr.Var "x") (PSExpr.Var "x"))

-- Proofs
theorem identity_structure : identity = PSExpr.Lam "x" (PSExpr.Var "x") := rfl

theorem compose_is_B : compose = B := rfl

def main : IO Unit := do
  IO.println "\n=== LEAN 4 TO PURESCRIPT TRANSPILER ===\n"
  IO.println "PureScript AST (PSExpr inductive type)"
  IO.println "Idiomatic pretty printer"
  IO.println ""
  IO.println "--- Lambda Calculus Combinators ---"
  IO.println s!"I = {prettyPS I}"
  IO.println s!"K = {prettyPS K}"
  IO.println s!"S = {prettyPS S}"
  IO.println s!"B = {prettyPS B}"
  IO.println s!"C = {prettyPS C}"
  IO.println s!"Y = {prettyPS Y}"
  IO.println s!"ω = {prettyPS omega}"
  IO.println ""
  IO.println "--- Church Encodings ---"
  IO.println s!"true  = {prettyPS churchTrue}"
  IO.println s!"false = {prettyPS churchFalse}"
  IO.println s!"and   = {prettyPS churchAnd}"
  IO.println ""
  IO.println "--- Examples ---"
  IO.println s!"identity = {prettyPS identity}"
  IO.println s!"compose  = {prettyPS compose}"
  IO.println ""
  IO.println "--- rfl Proofs ---"
  IO.println "✓ identity_structure : identity = Lam \"x\" (Var \"x\")"
  IO.println "✓ compose_is_B : compose = B"

#eval main