environment machine semantics

eval.lean

inductive Expr where
| Var : String -> Expr
| Abs : String -> Expr -> Expr
| App : Expr -> Expr -> Expr
deriving DecidableEq

-- evaluation contexts
inductive ExprZipper where
| Hole : ExprZipper
| Abs : String -> ExprZipper -> ExprZipper
| AppL : ExprZipper -> Expr -> ExprZipper
| AppR : Expr -> ExprZipper ->  ExprZipper
deriving DecidableEq

def ExprZipper.join (h : ExprZipper) (h2 : ExprZipper) : ExprZipper := match h with
| .Hole => h2
| .Abs x v => .Abs x (v.join h2)
| .AppL a b => .AppL (a.join h2) b
| .AppR a b => .AppR a (b.join h2)

-- this is the type of program states that the source language can describe/the user can express.
abbrev Point := ExprZipper × Expr
abbrev ExprZipper.fill (h : ExprZipper) (e : Expr) : Point := (h, e)

-- environments
inductive Binder where
| Var : String -> Binder
| Tmp : Binder
deriving DecidableEq

inductive Value where
| Lam : String -> List (Binder × Value) -> Point -> Value
abbrev Env := List (Binder × Value)
def Env.lookup (e : Env) (x : Binder) : Option Value :=
  match e with
  | [] => none
  | (b, v)::xs => if x = b then some v else xs.lookup x

-- program states, mapping to the typings of contexts on the source program at each location
structure State where
  caller : Option State
  env : Env
  ip : Point

abbrev At := ExprZipper.fill
inductive HasValue : State -> Value -> Type where
| Var :  env.lookup (.Var x) = some v -> HasValue ⟨k, env, At h (.Var x)⟩  v
| Lam : HasValue ⟨k, env, At h (.Abs x b)⟩ (.Lam x env (At (h.join (.Abs x .Hole)) b))
def Done (env : Env) (e : Expr) (v : Value) := HasValue ⟨none, env, At .Hole e⟩ v

inductive Ret : State -> Value -> State -> Type where
| HaveFunc : Ret ⟨ k, env, (At (ExprZipper.join h (.AppL .Hole a)) f)⟩  fv
  ⟨ k, ((.Tmp, fv)::env), (At (ExprZipper.join h (.AppR f .Hole)) a)⟩ 
| ApplyFunc :
  Ret ⟨k, (.Tmp, (.Lam x env2 p))::env, At (ExprZipper.join h (.AppR f .Hole)) a⟩  av
  ⟨ some ⟨ k, env, At h (.App f a) ⟩,  (.Var x, av)::env2, p⟩ 
| LamBody :
  Ret s v s2 ->
  Ret ⟨some s, _, At (ExprZipper.join h (.Abs x .Hole)) b⟩ v s2

inductive Step : State -> State -> Type where
| App : Step ⟨k, env, At h (.App f a)⟩ ⟨k, env, At (h.join (.AppL .Hole a)) f⟩ 
| Ret :  HasValue s v -> Ret s v s2 -> Step s s2

-- and a direct mapping of the evaluation rules to an interpreter,
-- using the necessary inverse of `join` (and if the language had any nondeterminism, the interpreter would
-- pick an implementation too)

def ExprZipper.leaf : ExprZipper -> (ExprZipper × ExprZipper) :=
  fun v => match v with
  | .Abs _ .Hole | .AppL .Hole _ | .AppR _ .Hole | .Hole => (.Hole, v)
  | .AppL z e => let (z', leaf) := leaf z; (.AppL z' e, leaf)
  | .AppR e z => let (z', leaf) := leaf z; (.AppR e z', leaf)
  | .Abs x z => let (z', leaf) := leaf z; (.Abs x z', leaf)
def result : State -> Option Value
| ⟨_, env, (_, .Var x)⟩ => env.lookup (.Var x)
| ⟨_, env, (h, .Abs x b)⟩ => some (.Lam x env ((h.join (.Abs x .Hole)), b))
| _ => none
def ret (v : Value) (s : State) : Option State :=
  let (cx, leaf) := s.ip.fst.leaf
  match leaf with
  | .AppL .Hole a => some ⟨s.caller, (.Tmp, v)::s.env, (cx.join (.AppR s.ip.snd .Hole), a)⟩
  | .AppR f .Hole => 
    match s.env with
    | (.Tmp, (.Lam x callee_env p))::env' => 
      some ⟨ some ⟨ s.caller, env', (cx, .App f s.ip.snd)⟩, (.Var x, v)::callee_env, p⟩ 
    | _ => none
  | .Abs _ .Hole =>
    match  s with
    | .mk (some k2) _ _ => ret v k2
    | _ => none
  | _ => none
def step : State -> Option State
| ⟨k, env, (h, (.App f a))⟩ => some ⟨k, env, ((h.join (.AppL .Hole a)), f)⟩ 
| s => do ret (<- result s) s

def result_consistent : result s = some v -> HasValue s v := by
  intro eq
  unfold result at eq
  split at eq
  apply HasValue.Var
  assumption
  simp at eq
  rw [<- eq] at |- 
  clear eq v
  apply HasValue.Lam
  simp at eq
theorem State.eta {s : State} : s = ⟨s.caller, s.env, s.ip⟩ := by 
  cases s
  simp
theorem Pair.eta {s : A × B} : s = (s.fst, s.snd) := by 
  cases s
  simp
theorem join_inv_leaf {e : ExprZipper} : e.leaf = (cx, l) -> cx.join l = e := by
  intro hLeaf
  cases e
  grind [ExprZipper.join, ExprZipper.leaf]
  · unfold ExprZipper.leaf at hLeaf
    split at hLeaf <;> try {next heq => simp at heq}

    · next heq => 
      simp at heq hLeaf
      rw [← hLeaf.left, ← hLeaf.right]
      simp [ExprZipper.join]
    · next heq1 =>
      simp at heq1
      split at hLeaf
      simp at hLeaf
      rw [← hLeaf.left, ← hLeaf.right]
      simp [ExprZipper.join]
      constructor
      exact heq1.left.symm
      apply join_inv_leaf
      rw [heq1.right]
      assumption
  · unfold ExprZipper.leaf at hLeaf
    split at hLeaf <;> try {next heq => simp at heq}
    · next heq =>
      simp at heq hLeaf
      rw [← hLeaf.left, hLeaf.right]
      simp [ExprZipper.join]
    · 
      next heq1 =>
      split at hLeaf
      simp at hLeaf 
      rw [← hLeaf.left, ← hLeaf.right]
      simp [ExprZipper.join]
      simp at heq1
      constructor
      apply join_inv_leaf
      rw [heq1.left]
      assumption
      exact heq1.right.symm
  · unfold ExprZipper.leaf at hLeaf
    split at hLeaf <;> try {next heq => simp at heq}
    · next heq1 =>
      simp at hLeaf
      rw [← hLeaf.left, ← hLeaf.right]
      simp [ExprZipper.join]
    · next heq1 =>
      split at hLeaf
      simp at hLeaf 
      rw [← hLeaf.left, ← hLeaf.right]
      simp [ExprZipper.join]
      simp at heq1
      constructor
      exact heq1.left.symm
      apply join_inv_leaf
      rw [heq1.right]
      assumption
def ret_consistent : ret v s = some s2 -> Ret s v s2 := by
  intro eq
  unfold ret at eq
  split at eq
  · simp at eq
    next heq =>
    generalize hLeaf : s.ip.fst.leaf = pair at *
    generalize hCx : pair.fst = cx at *
    rw [@State.eta s]
    rw [@Pair.eta _ _ s.ip]
    rw [@Pair.eta _ _ pair] at hLeaf
    have h2 := join_inv_leaf hLeaf
    rw [← h2]
    simp [← ExprZipper.fill.eq_def]
    simp [← At.eq_def]
    rw [heq]
    rw [← eq]
    rw [hCx]    
    apply Ret.HaveFunc
  · next at_arg =>
    split at eq
    · simp at eq
      rw [← eq]
      clear eq s2
      generalize h1 : s.ip.fst.leaf.fst = my_h
      generalize h2 : s.ip.snd = my_a
      rw (occs := [1]) [@State.eta s]
      next heq =>
      rw [heq]
      generalize hLeaf : s.ip.fst.leaf = pair at *
      rw [@Pair.eta _ _ pair ] at hLeaf
      have h3 := join_inv_leaf hLeaf
      rw [@Pair.eta _ _ s.ip]
      rw [h2]
      rw [← h3]
      rw [h1]
      rw [at_arg]
      apply Ret.ApplyFunc
    · simp at eq
  · next at_lam =>
    split at eq
    · simp at at_lam
      next ip =>
      rw [@Pair.eta _ _ ip]
      have h5 := @Pair.eta _ _ ip.fst.leaf
      have h4 := join_inv_leaf h5
      rw [← h4]
      rw [at_lam]
      apply Ret.LamBody
      exact ret_consistent eq
    · simp at eq
  · simp at eq
def step_consistent : step s = some s2 -> Step s s2 := by
  intro h1
  unfold step at h1
  split at h1
  simp at h1
  rw [← h1]
  apply Step.App
  simp [Option.bind] at h1
  split at h1
  simp at h1
  simp at h1
  apply Step.Ret
  apply result_consistent
  assumption
  apply ret_consistent
  assumption

theorem join_empty {e1 e2 : ExprZipper} : e1.join e2 = ExprZipper.Hole -> e2 = ExprZipper.Hole := by
  intro h

  cases e1
  · simp [ExprZipper.join] at h
    assumption
  · simp [ExprZipper.join] at h
  · simp [ExprZipper.join] at h
  · simp [ExprZipper.join] at h

theorem leaf_lift {e1 e2 : ExprZipper} : e2 ≠ .Hole -> e2.leaf = (.Hole, e2) -> (e1.join e2).leaf = (e1, e2) := by
  intro hneq h
  induction e1
  · simp [ExprZipper.join]
    assumption
  · simp [ExprZipper.join]
    unfold ExprZipper.leaf
    split <;> try next heq => simp at heq
    · next heq =>
      simp at heq

      exfalso
      obtain ⟨_, h1⟩ := heq
      have h2 := join_empty h1
      contradiction
    · split
      simp
      grind
  · simp [ExprZipper.join]
    unfold ExprZipper.leaf
    split <;> try next heq => simp at heq
    · simp
      next heq =>
      simp at heq
      have h1 := join_empty heq.left
      contradiction
    · grind
  · simp [ExprZipper.join]
    unfold ExprZipper.leaf
    split <;> try next heq => simp at heq
    · next heq =>
      simp at heq
      have h2 := join_empty heq.right
      contradiction
    · grind
-- @[simp]
theorem leaf_appl {e1 : ExprZipper} : (e1.join (.AppL a b)).leaf.snd = (ExprZipper.AppL a b).leaf.snd := by
  induction e1
  simp [ExprZipper.join, ExprZipper.leaf]
  · simp [ExprZipper.join, ExprZipper.leaf]
    rw (occs := [1]) [ExprZipper.leaf.eq_def]
    split <;> try next heq => simp at heq
    · next heq => 
      simp at heq
      have h2 := join_empty heq.right
      simp at h2
    · next heq  =>
      split
      simp
      simp at heq
      next b' _ _ _  _ heq2 =>
      rw [← Prod.eta b'.leaf] at heq2
      simp at heq2
      rw [← heq2.right]
      next ih _ _ _ _ _ _ =>

      rw [← heq.right]
      rw [ih]
  · next ih =>
    
    simp [ExprZipper.join]
    rw (occs := [1]) [ExprZipper.leaf.eq_def]
    split <;> try next heq => simp at heq
    · simp
      next heq =>
      simp at heq
      have h2 := join_empty heq.left
      simp at h2
    · next heq =>
      simp at heq
      split
      simp
      next zz _ _ _ _ _ heq2 =>
      rw [← Prod.eta zz.leaf] at heq2
      simp at heq2
      rw [← heq2.right]
      rw [← heq.left]
      assumption
  · next ih =>
    simp [ExprZipper.join]
    
    rw (occs := [1]) [ExprZipper.leaf.eq_def]
    split <;> try next heq => simp at heq
    · simp
      next heq =>
      simp at heq
      have h2 := join_empty heq.right
      simp at h2
    · next heq =>
      simp at heq
      split
      simp
      next zz _ _ _ _ heq2 =>
      rw [← Prod.eta zz.leaf] at heq2
      simp at heq2
      rw [← heq2.right]
      rw [← heq.right]
      assumption
    





theorem result_complete : HasValue s v -> result s = some v := by
  intro h
  cases h
  simp [result]
  assumption
  simp [result]
theorem ret_complete : Ret s v s2  -> ret v s = some s2  := by
  intro h
  cases h
  · unfold ret
    split
    · simp
      generalize h1 : ExprZipper.Hole.AppL _ = focus 
      next h _ _ _ _ _ =>
      have h2 : (h.join focus).leaf = (_, _) := leaf_lift (by grind) (by rw [← h1]; simp [ExprZipper.leaf])
      rw [h2]
      simp
      next heq =>
      simp at heq
      rw [h1, h2, ← h1] at heq
      simp at heq
      symm
      assumption
    · next h a _ _ _  heq =>
      simp at heq

      exfalso
      revert heq
      simp
      rw [leaf_lift _ _]
      simp
      simp
      simp [ExprZipper.leaf]
    · 
      next h _ _ _ _  heq1 =>
      simp at heq1
      rw [leaf_appl] at heq1
      simp [ExprZipper.leaf] at heq1
    · simp
      sorry
  · sorry
  · sorry
  
  
def decidableAnd (av : Decidable a) (bv : Decidable b) : Decidable (a ∧ b) :=
  instDecidableAnd
infix:40 " AND " => decidableAnd
def test (A : Prop) [i : Decidable A] : Decidable A := i
mutual
instance  : DecidableEq Value := fun 
| .Lam x1 e1 t1, .Lam x2 e2 t2 =>
    match test (x1 = x2 ∧ t1 = t2) AND (decidableEqEnv e1 e2) with
    | .isTrue p => .isTrue (by grind)
    | .isFalse p => .isFalse (by grind)

def decidableEqEnv (a b : Env) : Decidable (a = b) := 
  match a, b with
  | [], [] => .isTrue (by grind)
  | (b1, x)::xs, (b2, y)::ys => 
    match test (b1 = b2) AND (decidableEqEnv xs ys AND @instDecidableEqValue x y) with
    | .isTrue _ => .isTrue (by grind)
    | .isFalse _ => .isFalse (by grind)
  | _::_, [] | [], _::_ => .isFalse (by grind)
end



-- def b  := fun k => ((Step.Ret (HasValue.Var _) (Ret.LamBody ))
--       : Step ⟨k, [(.Var "x", (.Lam "v" [] (At (.Abs "v" .Hole) (.Var "v"))))], At (.AppL .Hole (.Var "y")) (.Var "x")⟩ _)
---
-- -- compression for `Point`s: this `Point` definition is isomorphic to the EC + Expr
-- inductive NodePath : Expr -> Type where
-- | Here : NodePath a
-- | InBody : NodePath b -> NodePath (.Abs x b)
-- | InFun : NodePath a -> NodePath (.App a b)
-- | InArg : NodePath b -> NodePath (.App a b)
-- abbrev Point := (e : Expr) × NodePath e
-- def ExprZipper.fill (h : ExprZipper) (e : Expr) : Point := match h with
--   | .Hole => ⟨e, .Here⟩ 
--   | .Abs x b => let ⟨b', p⟩ := b.fill e; ⟨.Abs x b', p.InBody⟩ 
--   | .AppL a b => let ⟨a', p⟩ := a.fill e; ⟨.App a' b, p.InFun⟩ 
--   | .AppR a b => let ⟨b', p⟩ := b.fill e; ⟨.App a b', p.InArg⟩ 

inductive LinearExprNode where
| Var : String -> LinearExprNode
| Abs : String -> Nat -> LinearExprNode
| App : Nat -> Nat -> LinearExprNode

abbrev Code := List LinearExprNode

inductive EncodedExpr : Nat -> Code -> Expr -> Prop where
| Var : c[n]'h = (.Var s) -> EncodedExpr n c (.Var s)
| Abs : c[n]'h = (.Abs x b) -> EncodedExpr b c b' -> EncodedExpr n c (.Abs x b')
| App : c[n]'h = (.App a b) -> EncodedExpr a c a' -> EncodedExpr b c b' -> EncodedExpr n c (.App a' b')

-- def EncodedPoint : Nat -> Nat -> Code -> Prop

sketching out the raw judgements

expr ::= x | e e | \x. e
context ::= \x. context | context e | e context | _
binder ::= x | temp
point ::= (context, expr)
value ::= lam x env point
env ::= (binder := value);*

caller ::= () | state
state ::= (caller, env, point)

judgement ::= join context context context
axiom ::= join _ E E
axiom ::= join E1 E2 E3 -> join (\x E1) E2 (\x E3)
axiom ::= join E1 E2 E3 -> join (e E1) E2 (e E3)
axiom ::= join E1 E2 E3 -> join (E1 e) E2 (E3 e)
judgement ::= env[x] -> value
axiom ::= E, b := v[b] ~> v
axiom ::= b != b2 -> E[b2] ~> v -> E, b := _[b2] ~> v
judgement ::= state returns value
axiom ::= env[x] ~> v -> (k, env, E, x) returns v
axiom ::= 
    join E (\x _) E' ->
    (k, env, E, \x e) returns lam x env (E', e)
judgement ::= state # value ~> state
axiom ::=
    join E (_ a) EL ->
    join E (f _) ER ->
    (k, env, EL, f) # fv ~> (k, env; temp := fv, ER, a)
axiom ::=
    join E (f _) EL ->
    (k, env; temp := lam x capt CE ce, ER, a) # av
        ~> ((k, env, E, f a), capt; x := av, CE, ce)
judgement ::= state ~> state