Merge pull request #1 from anoma/core-main-semantics

Big-step operational semantics for Core.Main

Juvix/Core/Main.lean

@@ -1,3 +1,4 @@
 
 import Juvix.Core.Main.Language
 import Juvix.Core.Main.Semantics
+import Juvix.Core.Main.Evaluator

Juvix/Core/Main/Evaluator.lean

@@ -0,0 +1,38 @@
+
+import Juvix.Core.Main.Language
+import Juvix.Core.Main.Semantics
+
+namespace Juvix.Core.Main
+
+partial def eval (P : Program) (ctx : Context) : Expr -> Value
+  | Expr.var idx => ctx.get! idx
+  | Expr.ident name => match P.defs.find? name with
+    | some expr => eval P [] expr
+    | none => panic! "undefined identifier"
+  | Expr.constr name => Value.constr_app name []
+  | Expr.const c => Value.const c
+  | Expr.app f arg => match eval P ctx f with
+    | Value.closure ctx' body => eval P (eval P ctx arg :: ctx') body
+    | _ => panic! "expected closure"
+  | Expr.constr_app ctr arg => match eval P ctx ctr with
+    | Value.constr_app ctr_name ctr_args_rev => Value.constr_app ctr_name (eval P ctx arg :: ctr_args_rev)
+    | _ => panic! "expected constructor application"
+  | Expr.binop op arg₁ arg₂ => match eval P ctx arg₁, eval P ctx arg₂ with
+    | Value.const (Constant.int val₁), Value.const (Constant.int val₂) =>
+      Value.const (Constant.int (eval_binop_int op val₁ val₂))
+    | _, _ => panic! "expected integer constants"
+  | Expr.lambda body => Value.closure ctx body
+  | Expr.save value body => eval P (eval P ctx value :: ctx) body
+  | Expr.branch name body next => match ctx with
+    | Value.constr_app name' args_rev :: ctx' =>
+      if name = name' then
+        eval P (args_rev ++ ctx') body
+      else
+        eval P ctx next
+    | _ => panic! "expected constructor application"
+  | Expr.default body => match ctx with
+    | _ :: ctx' => eval P ctx' body
+    | _ => panic! "expected constructor application"
+  | Expr.unit => Value.unit
+
+end Juvix.Core.Main

Juvix/Core/Main/Language/Base.lean

@@ -1,40 +1,45 @@
 
+import Batteries.Data.AssocList
+
 namespace Juvix.Core.Main
 
+open Batteries
+
 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

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

Juvix/Core/Main/Semantics.lean

@@ -1,11 +1,135 @@
 
 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
+
+notation "[" P "] " ctx " ⊢ " e " ↦ " v:40 => Eval P ctx e v
+
+-- The evaluation relation is deterministic.
+theorem Eval.deterministic {P ctx e v₁ v₂} (h₁ : [P] ctx ⊢ e ↦ v₁) (h₂ : [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
+
+-- The termination predicate for values. It is too strong for higher-order
+-- functions -- requires termination for all function arguments, even
+-- non-terminating ones.
+inductive Value.Terminating (P : Program) : Value → Prop where
+  | const {c} : Value.Terminating P (Value.const c)
+  | constr_app {ctr_name args_rev} :
+    Value.Terminating P (Value.constr_app ctr_name args_rev)
+  | closure {ctx body} :
+    (∀ v v',
+      [P] v :: ctx ⊢ body ↦ v' →
+      Value.Terminating P v') →
+    Value.Terminating P (Value.closure ctx body)
+  | unit : Value.Terminating P Value.unit
+
+def Expr.Terminating (P : Program) (ctx : Context) (e : Expr) : Prop :=
+  (∃ v, [P] ctx ⊢ e ↦ v ∧ Value.Terminating P v)
+
+def Program.Terminating (P : Program) : Prop :=
+  Expr.Terminating P [] P.main
+
+lemma Eval.Expr.Terminating {P ctx e v} :
+  Expr.Terminating P ctx e → [P] ctx ⊢ e ↦ v → Value.Terminating P v := by
+  intro h₁ h₂
+  rcases h₁ with ⟨v', hval, hterm⟩
+  rewrite [Eval.deterministic h₂ hval]
+  assumption
 
 end Juvix.Core.Main

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "07b2399c02d91a83fc030d165d734dca8d92a806",
+   "rev": "bb0575e329e059f7ec31c43337a2094282f6be3c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "74dffd1a83cdd2969a31c9892b0517e7c6f50668",
+   "rev": "9e583efcea920afa13ee2a53069821a2297a94c0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",