From f55b0d51dc6eff5f2dc7a8204444ca1d4bb1a974 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Mon, 16 Dec 2024 19:13:07 +0100
Subject: [PATCH] Big-step operational semantics

---
 Juvix/Core/Main/Language/Base.lean  |  61 +++++++++--------
 Juvix/Core/Main/Language/Value.lean |   2 +-
 Juvix/Core/Main/Semantics.lean      | 102 ++++++++++++++++++++++++++--
 3 files changed, 132 insertions(+), 33 deletions(-)

diff --git a/Juvix/Core/Main/Language/Base.lean b/Juvix/Core/Main/Language/Base.lean
index 74032e4..6307748 100644
--- a/Juvix/Core/Main/Language/Base.lean
+++ b/Juvix/Core/Main/Language/Base.lean
@@ -1,40 +1,45 @@
 
+import Lean.Data.AssocList
+
 namespace Juvix.Core.Main
 
+open Lean
+
 abbrev Name : Type := String
 
 inductive Constant : Type where
   | int : Int → Constant
   | string : String → Constant
-  deriving Inhabited, DecidableEq
-
-inductive BuiltinOp : Type where
-  | add_int : BuiltinOp
-  | sub_int : BuiltinOp
-  | mul_int : BuiltinOp
-  | div_int : BuiltinOp
-  deriving Inhabited, DecidableEq
-
-mutual
-  inductive Expr : Type where
-    | var : Nat → Expr
-    | ident : Name → Expr
-    | const : Constant → Expr
-    | app : Expr → Expr → Expr
-    | builtin_app : (oper : BuiltinOp) → (args : List Expr) → Expr
-    | constr_app : (constr : Name) → (args : List Expr) → Expr
-    | lambda : (body : Expr) → Expr
-    | let : (value : Expr) → (body : Expr) → Expr
-    | case : (value : Expr) → (branches : List CaseBranch) → Expr
-    | unit : Expr
-    deriving Inhabited
-
-  structure CaseBranch where
-    constr : Name
-    body : Expr
-end
+  deriving Inhabited, BEq, DecidableEq
+
+inductive BinaryOp : Type where
+  | add_int : BinaryOp
+  | sub_int : BinaryOp
+  | mul_int : BinaryOp
+  | div_int : BinaryOp
+  deriving Inhabited, BEq, DecidableEq
+
+inductive Expr : Type where
+  | var : Nat → Expr
+  | ident : Name → Expr
+  | constr : Name → Expr
+  | const : Constant → Expr
+  | app : Expr → Expr → Expr
+  | constr_app : Expr → Expr → Expr
+  | binop : (oper : BinaryOp) → (arg₁ arg₂ : Expr) → Expr
+  | lambda : (body : Expr) → Expr
+  | save : (value : Expr) → (body : Expr) → Expr
+  | branch : (constr : Name) → (body : Expr) → (next : Expr) → Expr
+  | default : (body : Expr) → Expr
+  | unit : Expr
+  deriving Inhabited, BEq, DecidableEq
 
 structure Program where
-  defs : List Expr
+  defs : AssocList Name Expr
+  main : Expr
+
+def Expr.mk_app (f : Expr) : List Expr → Expr
+  | [] => f
+  | x :: xs => Expr.mk_app (Expr.app f x) xs
 
 end Juvix.Core.Main
diff --git a/Juvix/Core/Main/Language/Value.lean b/Juvix/Core/Main/Language/Value.lean
index dd5f8a6..230e512 100644
--- a/Juvix/Core/Main/Language/Value.lean
+++ b/Juvix/Core/Main/Language/Value.lean
@@ -5,7 +5,7 @@ namespace Juvix.Core.Main
 
 inductive Value : Type where
   | const : Constant → Value
-  | constr_app : (constr : Name) → (args : List Value) → Value
+  | constr_app : (constr : Name) → (args_rev : List Value) → Value
   | closure : (ctx : List Value) → (value : Expr) → Value
   | unit : Value
   deriving Inhabited
diff --git a/Juvix/Core/Main/Semantics.lean b/Juvix/Core/Main/Semantics.lean
index 0cb9714..3042fb6 100644
--- a/Juvix/Core/Main/Semantics.lean
+++ b/Juvix/Core/Main/Semantics.lean
@@ -1,11 +1,105 @@
 
 import Juvix.Core.Main.Language
+import Mathlib.Tactic.CC
 
 namespace Juvix.Core.Main
 
-def f : Expr -> Expr := λ e =>
-  match e with
-  | Expr.lambda (body := e) => e
-  | _ => Expr.lambda (body := e)
+def eval_binop_int (op : BinaryOp) (i₁ i₂ : Int) : Int :=
+  match op with
+  | BinaryOp.add_int => i₁ + i₂
+  | BinaryOp.sub_int => i₁ - i₂
+  | BinaryOp.mul_int => i₁ * i₂
+  | BinaryOp.div_int => i₁ / i₂
+
+inductive Eval (P : Program) : Context → Expr → Value → Prop where
+  | eval_var {ctx idx val} :
+    ctx.get? idx = some val →
+    Eval P ctx (Expr.var idx) val
+  | eval_ident {ctx name expr val} :
+    P.defs.find? name = some expr →
+    Eval P [] expr val →
+    Eval P ctx (Expr.ident name) val
+  | eval_const {ctx c} :
+    Eval P ctx (Expr.const c) (Value.const c)
+  | eval_app {ctx ctx' f body arg val val'} :
+    Eval P ctx f (Value.closure ctx' body) →
+    Eval P ctx arg val →
+    Eval P (val :: ctx') body val' →
+    Eval P ctx (Expr.app f arg) val'
+  | eval_constr_app {ctx ctr ctr_name ctr_args_rev arg val} :
+    Eval P ctx ctr (Value.constr_app ctr_name ctr_args_rev) →
+    Eval P ctx arg val →
+    Eval P ctx (Expr.constr_app ctr arg) (Value.constr_app ctr_name (val :: ctr_args_rev))
+  | eval_binop {ctx op arg₁ arg₂ val₁ val₂} :
+    Eval P ctx arg₁ (Value.const (Constant.int val₁)) →
+    Eval P ctx arg₂ (Value.const (Constant.int val₂)) →
+    Eval P ctx (Expr.binop op arg₁ arg₂) (Value.const (Constant.int (eval_binop_int op val₁ val₂)))
+  | eval_lambda {ctx body} :
+    Eval P ctx (Expr.lambda body) (Value.closure ctx body)
+  | eval_save {ctx value body val val'} :
+    Eval P ctx value val →
+    Eval P (val :: ctx) body val' →
+    Eval P ctx (Expr.save value body) val'
+  | eval_branch_matches {ctx name args_rev body val} :
+    Eval P (args_rev ++ ctx) body val →
+    Eval P (Value.constr_app name args_rev :: ctx) (Expr.branch name body _) val
+  | eval_branch_fails {ctx name name' next val} :
+    name ≠ name' →
+    Eval P ctx next val →
+    Eval P (Value.constr_app name _ :: ctx) (Expr.branch name' _ next) val
+  | eval_default {ctx body val} :
+    Eval P ctx body val →
+    Eval P (_ :: ctx) (Expr.default body) val
+  | eval_unit {ctx} :
+    Eval P ctx Expr.unit Value.unit
+
+theorem Eval.deterministic {P ctx e v₁ v₂} (h₁ : Eval P ctx e v₁) (h₂ : Eval P ctx e v₂) : v₁ = v₂ := by
+  induction h₁ generalizing v₂ with
+  | eval_var =>
+    cases h₂ <;> cc
+  | eval_ident _ _ ih =>
+    specialize (@ih v₂)
+    cases h₂ <;> cc
+  | eval_const =>
+    cases h₂ <;> cc
+  | eval_app _ _ _ ih ih' aih =>
+    cases h₂ with
+    | eval_app hval harg =>
+      apply aih
+      specialize (ih hval)
+      specialize (ih' harg)
+      simp_all
+  | eval_constr_app _ _ ih ih' =>
+    cases h₂ with
+    | eval_constr_app hctr harg =>
+      specialize (ih hctr)
+      specialize (ih' harg)
+      simp_all
+  | eval_binop _ _ ih₁ ih₂ =>
+    cases h₂ with
+    | eval_binop h₁ h₂ =>
+      specialize (ih₁ h₁)
+      specialize (ih₂ h₂)
+      simp_all
+  | eval_lambda =>
+    cases h₂ <;> cc
+  | eval_save _ _ ih ih' =>
+    cases h₂ with
+    | eval_save hval hbody =>
+      specialize (ih hval)
+      rw [<- ih] at hbody
+      specialize (ih' hbody)
+      simp_all
+  | eval_branch_matches _ ih =>
+    specialize (@ih v₂)
+    cases h₂ <;> cc
+  | eval_branch_fails _ _ ih =>
+    specialize (@ih v₂)
+    cases h₂ <;> cc
+  | eval_default _ ih =>
+    specialize (@ih v₂)
+    cases h₂ <;> cc
+  | eval_unit =>
+    cases h₂ <;> cc
 
 end Juvix.Core.Main