Data Types à la Carte for lean4

ALaCarte-safe.lean

-- ==========================================
-- 1. 基础架构：W-类型 (MLTT 核心)
-- ==========================================

inductive W (A : Type) (B : A → Type) where
  | mk (a : A) (f : B a → W A B) : W A B

def wInd {A : Type} {B : A → Type} {p : W A B → Type}
  (step : (a : A) → (f : B a → W A B) → (∀ (b : B a), p (f b)) → p (W.mk a f))
    (t : W A B) : p t :=
  match t with
  | W.mk a f => step a f (fun b => wInd step (f b))

def wFold {A : Type} {B : A → Type} {α : Type}
  (alg : (a : A) → (B a → α) → α) (t : W A B) : α :=
  match t with
  | W.mk a f => alg a (fun b => wFold alg (f b))

-- ==========================================
-- 2. 蓝图：PFunctor
-- ==========================================

structure PFunctor where
  A : Type
  B : A → Type

def sumOfP (p1 p2 : PFunctor) : PFunctor where
  A := p1.A ⊕ p2.A
  B := fun x => match x with
    | Sum.inl a1 => p1.B a1
    | Sum.inr a2 => p2.B a2

infixr:1 " :+: " => sumOfP

-- 使用 abbrev 以便在类型类搜索时自动展开
abbrev Fix (P : PFunctor) := W P.A P.B

-- ==========================================
-- 3. 子类型化与注入
-- ==========================================

structure Equiv (α β : Type) where
  to : α → β
  inv : β → α

class SubP (sub sup : PFunctor) where
  injA : sub.A → sup.A
  injB : (a : sub.A) → Equiv (sup.B (injA a)) (sub.B a)

infixr:1 " :<: " => SubP

instance subSelf (P : PFunctor) : P :<: P where
  injA := id
  injB _ := ⟨id, id⟩

instance subLeft (P Q : PFunctor) : P :<: (P :+: Q) where
  injA a := Sum.inl a
  injB _ := ⟨id, id⟩

instance subRight [h : P :<: Q] : P :<: (R :+: Q) where
  injA a := Sum.inr (h.injA a)
  injB a := h.injB a
-- 优先级：右递归 > 左匹配 > 自身

def inject (sub : PFunctor) {sup : PFunctor} [h : sub :<: sup]
  (a : sub.A) (f : sub.B a → Fix sup) : Fix sup :=
  W.mk (h.injA a) (fun b_sup => f ((h.injB a).to b_sup))

-- ==========================================
-- 4. 独立组件
-- ==========================================

def LitP : PFunctor := { A := Int, B := fun _ => Empty }
def AddP : PFunctor := { A := Unit, B := fun _ => Bool }
def MultP : PFunctor := { A := Unit, B := fun _ => Bool }

-- --- 智能构造器 ---

def lit {P : PFunctor} [h : LitP :<: P] (n : Int) : Fix P :=
  -- W.mk (h.injA n) (fun b => nomatch (h.injB n).to b)
  inject LitP n (fun e => nomatch e)

def add {P : PFunctor} [h : AddP :<: P] (e1 e2 : Fix P) : Fix P :=
  /-
  let a_sub : Unit := ()
  let equiv := h.injB a_sub
  W.mk (h.injA a_sub) (fun b_sup =>
    match equiv.to b_sup with
    | true => e1
    | false => e2)
  -/
  inject AddP () (fun b => match b with | true => e1 | false => e2)

def mult {P : PFunctor} [h : MultP :<: P] (e1 e2 : Fix P) : Fix P :=
  inject MultP () (fun b => match b with | true => e1 | false => e2)

-- ==========================================
-- 5. 求值逻辑
-- ==========================================

class EvalP (P : PFunctor) where
  evalAlg : (a : P.A) → (P.B a → Int) → Int

def eval {P : PFunctor} [h : EvalP P] (t : Fix P) : Int :=
  wFold h.evalAlg t

instance [h1 : EvalP P] [h2 : EvalP Q] : EvalP (P :+: Q) where
  evalAlg a f := match a with
    | Sum.inl a1 => h1.evalAlg a1 f
    | Sum.inr a2 => h2.evalAlg a2 f

instance : EvalP LitP where
  evalAlg n _ := n
instance : EvalP AddP where
  evalAlg _ f := f true + f false
instance : EvalP MultP where
  evalAlg _ f := f true * f false

-- ==========================================
-- 6. 最终验证
-- ==========================================

-- 关键：必须用 abbrev，否则 SubP 和 EvalP 无法找到实例

def myExpr : Fix (AddP :+: LitP :+: MultP) :=
  mult (add (lit 5) (lit 6)) (lit 2)

#eval eval myExpr  -- 结果：22

def simpleExpr : Fix (AddP :+: LitP) := add (lit 10) (lit 20)
#eval eval simpleExpr -- 结果：30
#reduce simpleExpr

---- add name

def NameP : PFunctor := { A := String, B := fun _ => Empty }

def name {P : PFunctor} [h : NameP :<: P] (n : String) : Fix P :=
  inject NameP n (fun e => nomatch e)

instance : EvalP NameP where
  evalAlg n _ :=
    match String.toInt? n with
    | none => 0
    | some n => n

def myExpr' : Fix (AddP :+: LitP :+: MultP :+: NameP) :=
  mult (add (lit 5) (lit 6)) (name "2")

#eval eval myExpr'

-- add minus

def MinusP : PFunctor := { A := Unit, B := fun _ => Bool }

def minus {P : PFunctor} [h : MinusP :<: P] (e1 e2 : Fix P) : Fix P :=
  inject MinusP () (fun b => match b with | true => e1 | false => e2)

instance : EvalP MinusP where
  evalAlg _ f := f true - f false

def myExpr'' : Fix (AddP :+: LitP :+: MultP :+: NameP :+: MinusP) :=
  minus (lit 20) $ mult (add (lit 5) (lit 6)) (name "2")

#eval eval myExpr''

-- add inc (++)

def IncP : PFunctor := { A := Unit, B := fun _ => Unit }

def inc {P : PFunctor} [h : IncP :<: P] (e : Fix P) : Fix P :=
  inject IncP () (fun _ => e)

instance : EvalP IncP where
  evalAlg _ f := f () + 1

def myExpr''' : Fix (AddP :+: LitP :+: MultP :+: NameP :+: MinusP :+: IncP) :=
  inc $ minus (lit 20) $ mult (add (lit 5) (lit 6)) (name "2")

#eval eval myExpr'''

-- add method tostring

class ToStringP (P : PFunctor) where
  tostrAlg : (a : P.A) → (P.B a → String) → String

instance : ToStringP LitP where
  tostrAlg n _ :=  toString (α := Int) n -- α cannot infer

instance : ToStringP AddP where
  tostrAlg _ f := "(" ++ f true ++ " + " ++ f false ++ ")"

instance : ToStringP MultP where
  tostrAlg _ f := "(" ++ f true ++ " * " ++ f false ++ ")"

instance [h1 : ToStringP P] [h2 : ToStringP Q] : ToStringP (P :+: Q) where
  tostrAlg a f := match a with
    | Sum.inl a1 => h1.tostrAlg a1 f
    | Sum.inr a2 => h2.tostrAlg a2 f

def tostring {P : PFunctor} [h : ToStringP P] (t : Fix P) : String :=
  wFold h.tostrAlg t

#eval tostring myExpr

instance : ToStringP NameP where
  tostrAlg n _ := n

#eval tostring myExpr'

instance : ToStringP MinusP where
  tostrAlg _ f := "(" ++ f true ++ " - " ++ f false ++ ")"
#eval tostring myExpr''

instance : ToStringP IncP where
  tostrAlg _ f := "inc " ++ f ()
#eval tostring myExpr'''

-- add n op, sum

def sumP : PFunctor := { A := Nat, B := fun n => Fin n}


def sum {P : PFunctor} [h : sumP :<: P] (es : List (Fix P)) : Fix P :=
  inject sumP es.length (fun b => es.get b)

instance : EvalP sumP where
  evalAlg n f := List.sum (List.map f (List.finRange n))

def myExprSum : Fix (AddP :+: LitP :+: sumP) :=
  sum [lit 1, lit 2, lit 3, add (lit 4) (lit 5)]

#eval eval myExprSum  -- 15