Skip to content

Commit 2a00051

Browse files
lukaszczlukaszcz
committed
Big-step operational semantics for Core.Main (#1)
1 parent 33737f0 commit 2a00051

File tree

7 files changed

+207
-39
lines changed

7 files changed

+207
-39
lines changed

‎Juvix/Core/Main.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11

22
import Juvix.Core.Main.Language
33
import Juvix.Core.Main.Semantics
4+
import Juvix.Core.Main.Evaluator

‎Juvix/Core/Main/Evaluator.lean

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
2+
import Juvix.Core.Main.Language
3+
import Juvix.Core.Main.Semantics
4+
5+
namespace Juvix.Core.Main
6+
7+
partial def eval (P : Program) (ctx : Context) : Expr -> Value
8+
| Expr.var idx => ctx.get! idx
9+
| Expr.ident name => match P.defs.find? name with
10+
| some expr => eval P [] expr
11+
| none => panic! "undefined identifier"
12+
| Expr.constr name => Value.constr_app name []
13+
| Expr.const c => Value.const c
14+
| Expr.app f arg => match eval P ctx f with
15+
| Value.closure ctx' body => eval P (eval P ctx arg :: ctx') body
16+
| _ => panic! "expected closure"
17+
| Expr.constr_app ctr arg => match eval P ctx ctr with
18+
| Value.constr_app ctr_name ctr_args_rev => Value.constr_app ctr_name (eval P ctx arg :: ctr_args_rev)
19+
| _ => panic! "expected constructor application"
20+
| Expr.binop op arg₁ arg₂ => match eval P ctx arg₁, eval P ctx arg₂ with
21+
| Value.const (Constant.int val₁), Value.const (Constant.int val₂) =>
22+
Value.const (Constant.int (eval_binop_int op val₁ val₂))
23+
| _, _ => panic! "expected integer constants"
24+
| Expr.lambda body => Value.closure ctx body
25+
| Expr.save value body => eval P (eval P ctx value :: ctx) body
26+
| Expr.branch name body next => match ctx with
27+
| Value.constr_app name' args_rev :: ctx' =>
28+
if name = name' then
29+
eval P (args_rev ++ ctx') body
30+
else
31+
eval P ctx next
32+
| _ => panic! "expected constructor application"
33+
| Expr.default body => match ctx with
34+
| _ :: ctx' => eval P ctx' body
35+
| _ => panic! "expected constructor application"
36+
| Expr.unit => Value.unit
37+
38+
end Juvix.Core.Main

‎Juvix/Core/Main/Language/Base.lean

Lines changed: 33 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,40 +1,45 @@
11

2+
import Batteries.Data.AssocList
3+
24
namespace Juvix.Core.Main
35

6+
open Batteries
7+
48
abbrev Name : Type := String
59

610
inductive Constant : Type where
711
| int : Int → Constant
812
| string : String → Constant
9-
deriving Inhabited, DecidableEq
10-
11-
inductive BuiltinOp : Type where
12-
| add_int : BuiltinOp
13-
| sub_int : BuiltinOp
14-
| mul_int : BuiltinOp
15-
| div_int : BuiltinOp
16-
deriving Inhabited, DecidableEq
17-
18-
mutual
19-
inductive Expr : Type where
20-
| var : Nat → Expr
21-
| ident : Name → Expr
22-
| const : Constant → Expr
23-
| app : Expr → Expr → Expr
24-
| builtin_app : (oper : BuiltinOp) → (args : List Expr) → Expr
25-
| constr_app : (constr : Name) → (args : List Expr) → Expr
26-
| lambda : (body : Expr) → Expr
27-
| let : (value : Expr) → (body : Expr) → Expr
28-
| case : (value : Expr) → (branches : List CaseBranch) → Expr
29-
| unit : Expr
30-
deriving Inhabited
31-
32-
structure CaseBranch where
33-
constr : Name
34-
body : Expr
35-
end
13+
deriving Inhabited, BEq, DecidableEq
14+
15+
inductive BinaryOp : Type where
16+
| add_int : BinaryOp
17+
| sub_int : BinaryOp
18+
| mul_int : BinaryOp
19+
| div_int : BinaryOp
20+
deriving Inhabited, BEq, DecidableEq
21+
22+
inductive Expr : Type where
23+
| var : Nat → Expr
24+
| ident : Name → Expr
25+
| constr : Name → Expr
26+
| const : Constant → Expr
27+
| app : Expr → Expr → Expr
28+
| constr_app : Expr → Expr → Expr
29+
| binop : (oper : BinaryOp) → (arg₁ arg₂ : Expr) → Expr
30+
| lambda : (body : Expr) → Expr
31+
| save : (value : Expr) → (body : Expr) → Expr
32+
| branch : (constr : Name) → (body : Expr) → (next : Expr) → Expr
33+
| default : (body : Expr) → Expr
34+
| unit : Expr
35+
deriving Inhabited, BEq, DecidableEq
3636

3737
structure Program where
38-
defs : List Expr
38+
defs : AssocList Name Expr
39+
main : Expr
40+
41+
def Expr.mk_app (f : Expr) : List Expr → Expr
42+
| [] => f
43+
| x :: xs => Expr.mk_app (Expr.app f x) xs
3944

4045
end Juvix.Core.Main

‎Juvix/Core/Main/Language/Value.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ namespace Juvix.Core.Main
55

66
inductive Value : Type where
77
| const : Constant → Value
8-
| constr_app : (constr : Name) → (args : List Value) → Value
8+
| constr_app : (constr : Name) → (args_rev : List Value) → Value
99
| closure : (ctx : List Value) → (value : Expr) → Value
1010
| unit : Value
1111
deriving Inhabited

‎Juvix/Core/Main/Semantics.lean

Lines changed: 128 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,135 @@
11

22
import Juvix.Core.Main.Language
3+
import Mathlib.Tactic.CC
34

45
namespace Juvix.Core.Main
56

6-
def f : Expr -> Expr := λ e =>
7-
match e with
8-
| Expr.lambda (body := e) => e
9-
| _ => Expr.lambda (body := e)
7+
def eval_binop_int (op : BinaryOp) (i₁ i₂ : Int) : Int :=
8+
match op with
9+
| BinaryOp.add_int => i₁ + i₂
10+
| BinaryOp.sub_int => i₁ - i₂
11+
| BinaryOp.mul_int => i₁ * i₂
12+
| BinaryOp.div_int => i₁ / i₂
13+
14+
inductive Eval (P : Program) : Context → Expr → Value → Prop where
15+
| eval_var {ctx idx val} :
16+
ctx.get? idx = some val →
17+
Eval P ctx (Expr.var idx) val
18+
| eval_ident {ctx name expr val} :
19+
P.defs.find? name = some expr →
20+
Eval P [] expr val →
21+
Eval P ctx (Expr.ident name) val
22+
| eval_const {ctx c} :
23+
Eval P ctx (Expr.const c) (Value.const c)
24+
| eval_app {ctx ctx' f body arg val val'} :
25+
Eval P ctx f (Value.closure ctx' body) →
26+
Eval P ctx arg val →
27+
Eval P (val :: ctx') body val' →
28+
Eval P ctx (Expr.app f arg) val'
29+
| eval_constr_app {ctx ctr ctr_name ctr_args_rev arg val} :
30+
Eval P ctx ctr (Value.constr_app ctr_name ctr_args_rev) →
31+
Eval P ctx arg val →
32+
Eval P ctx (Expr.constr_app ctr arg) (Value.constr_app ctr_name (val :: ctr_args_rev))
33+
| eval_binop {ctx op arg₁ arg₂ val₁ val₂} :
34+
Eval P ctx arg₁ (Value.const (Constant.int val₁)) →
35+
Eval P ctx arg₂ (Value.const (Constant.int val₂)) →
36+
Eval P ctx (Expr.binop op arg₁ arg₂) (Value.const (Constant.int (eval_binop_int op val₁ val₂)))
37+
| eval_lambda {ctx body} :
38+
Eval P ctx (Expr.lambda body) (Value.closure ctx body)
39+
| eval_save {ctx value body val val'} :
40+
Eval P ctx value val →
41+
Eval P (val :: ctx) body val' →
42+
Eval P ctx (Expr.save value body) val'
43+
| eval_branch_matches {ctx name args_rev body val} :
44+
Eval P (args_rev ++ ctx) body val →
45+
Eval P (Value.constr_app name args_rev :: ctx) (Expr.branch name body _) val
46+
| eval_branch_fails {ctx name name' next val} :
47+
name ≠ name' →
48+
Eval P ctx next val →
49+
Eval P (Value.constr_app name _ :: ctx) (Expr.branch name' _ next) val
50+
| eval_default {ctx body val} :
51+
Eval P ctx body val →
52+
Eval P (_ :: ctx) (Expr.default body) val
53+
| eval_unit {ctx} :
54+
Eval P ctx Expr.unit Value.unit
55+
56+
notation "[" P "] " ctx " ⊢ " e " ↦ " v:40 => Eval P ctx e v
57+
58+
-- The evaluation relation is deterministic.
59+
theorem Eval.deterministic {P ctx e v₁ v₂} (h₁ : [P] ctx ⊢ e ↦ v₁) (h₂ : [P] ctx ⊢ e ↦ v₂) : v₁ = v₂ := by
60+
induction h₁ generalizing v₂ with
61+
| eval_var =>
62+
cases h₂ <;> cc
63+
| eval_ident _ _ ih =>
64+
specialize (@ih v₂)
65+
cases h₂ <;> cc
66+
| eval_const =>
67+
cases h₂ <;> cc
68+
| eval_app _ _ _ ih ih' aih =>
69+
cases h₂ with
70+
| eval_app hval harg =>
71+
apply aih
72+
specialize (ih hval)
73+
specialize (ih' harg)
74+
simp_all
75+
| eval_constr_app _ _ ih ih' =>
76+
cases h₂ with
77+
| eval_constr_app hctr harg =>
78+
specialize (ih hctr)
79+
specialize (ih' harg)
80+
simp_all
81+
| eval_binop _ _ ih₁ ih₂ =>
82+
cases h₂ with
83+
| eval_binop h₁ h₂ =>
84+
specialize (ih₁ h₁)
85+
specialize (ih₂ h₂)
86+
simp_all
87+
| eval_lambda =>
88+
cases h₂ <;> cc
89+
| eval_save _ _ ih ih' =>
90+
cases h₂ with
91+
| eval_save hval hbody =>
92+
specialize (ih hval)
93+
rw [<- ih] at hbody
94+
specialize (ih' hbody)
95+
simp_all
96+
| eval_branch_matches _ ih =>
97+
specialize (@ih v₂)
98+
cases h₂ <;> cc
99+
| eval_branch_fails _ _ ih =>
100+
specialize (@ih v₂)
101+
cases h₂ <;> cc
102+
| eval_default _ ih =>
103+
specialize (@ih v₂)
104+
cases h₂ <;> cc
105+
| eval_unit =>
106+
cases h₂ <;> cc
107+
108+
-- The termination predicate for values. It is too strong for higher-order
109+
-- functions -- requires termination for all function arguments, even
110+
-- non-terminating ones.
111+
inductive Value.Terminating (P : Program) : Value → Prop where
112+
| const {c} : Value.Terminating P (Value.const c)
113+
| constr_app {ctr_name args_rev} :
114+
Value.Terminating P (Value.constr_app ctr_name args_rev)
115+
| closure {ctx body} :
116+
(∀ v v',
117+
[P] v :: ctx ⊢ body ↦ v' →
118+
Value.Terminating P v') →
119+
Value.Terminating P (Value.closure ctx body)
120+
| unit : Value.Terminating P Value.unit
121+
122+
def Expr.Terminating (P : Program) (ctx : Context) (e : Expr) : Prop :=
123+
(∃ v, [P] ctx ⊢ e ↦ v ∧ Value.Terminating P v)
124+
125+
def Program.Terminating (P : Program) : Prop :=
126+
Expr.Terminating P [] P.main
127+
128+
lemma Eval.Expr.Terminating {P ctx e v} :
129+
Expr.Terminating P ctx e → [P] ctx ⊢ e ↦ v → Value.Terminating P v := by
130+
intro h₁ h₂
131+
rcases h₁ with ⟨v', hval, hterm⟩
132+
rewrite [Eval.deterministic h₂ hval]
133+
assumption
10134

11135
end Juvix.Core.Main

‎README.md

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
1-
# Juvix Lean formalization library
1+
# Juvix library for Lean 4
22

33
The Juvix Lean library provides primitives for verifying the correctness of Juvix compiler runs, i.e., proving that the semantics of a particular Juvix program is preserved by the compilation process.
44

5-
The major components of the library include:
6-
- formalization of Juvix compiler internal representations and their semantics,
7-
- proof-producing metaprograms for verifying that individual Juvix compiler transformations preserve the semantics.
5+
The library includes:
6+
- formalization of Juvix compiler internal representations (IRs) and their semantics,
7+
- proof-producing metaprograms for verifying that Juvix compiler transformations preserve the semantics of concrete IR programs.

‎lake-manifest.json

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover-community",
8-
"rev": "07b2399c02d91a83fc030d165d734dca8d92a806",
8+
"rev": "bb0575e329e059f7ec31c43337a2094282f6be3c",
99
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "master",
@@ -75,7 +75,7 @@
7575
"type": "git",
7676
"subDir": null,
7777
"scope": "leanprover-community",
78-
"rev": "74dffd1a83cdd2969a31c9892b0517e7c6f50668",
78+
"rev": "9e583efcea920afa13ee2a53069821a2297a94c0",
7979
"name": "batteries",
8080
"manifestFile": "lake-manifest.json",
8181
"inputRev": "main",

0 commit comments

Comments
 (0)