evaluator function & Terminating predicate

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,9 +1,9 @@
 
-import Lean.Data.AssocList
+import Batteries.Data.AssocList
 
 namespace Juvix.Core.Main
 
-open Lean
+open Batteries
 
 abbrev Name : Type := String
 

Juvix/Core/Main/Semantics.lean

@@ -1,6 +1,7 @@
 
 import Juvix.Core.Main.Language
 import Mathlib.Tactic.CC
+import Aesop
 
 namespace Juvix.Core.Main
 
@@ -102,4 +103,31 @@ theorem Eval.deterministic {P ctx e v₁ v₂} (h₁ : Eval P ctx e v₁) (h₂
   | 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',
+      Eval 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, Eval 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 → Eval 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