generalize definitions (wip, not transitive)

Juvix/Core/Main/Language/Base.lean

@@ -1,5 +1,6 @@
 
 import Batteries.Data.AssocList
+import Mathlib.Data.Set.Basic
 
 namespace Juvix.Core.Main
 
@@ -44,4 +45,30 @@ def Expr.mk_app (f : Expr) : List Expr → Expr
   | [] => f
   | x :: xs => Expr.mk_app (Expr.app f x) xs
 
+-- The domain of a program is the set of names of its definitions.
+def Program.dom (p : Program) : Set Name :=
+  {x | x ∈ p.defs.toList.map Prod.fst}
+
+-- The domain of an expression is the set of identifiers referenced in the
+-- expression.
+@[simp]
+def Expr.dom (e : Expr) : Set Name :=
+  match e with
+  | Expr.var _ => ∅
+  | Expr.ident n => {n}
+  | Expr.constr _ => ∅
+  | Expr.const _ => ∅
+  | Expr.app f x => f.dom ∪ x.dom
+  | Expr.constr_app c x => c.dom ∪ x.dom
+  | Expr.binop _ x y => x.dom ∪ y.dom
+  | Expr.lambda b => b.dom
+  | Expr.save v b => v.dom ∪ b.dom
+  | Expr.branch _ b n => b.dom ∪ n.dom
+  | Expr.default b => b.dom
+  | Expr.unit => ∅
+
+def Program.dom_ok (p : Program) : Prop :=
+  p.main.dom ⊆ p.dom ∧
+  ∀ (n : Name) (e : Expr), p.defs.find? n = some e → e.dom ⊆ p.dom
+
 end Juvix.Core.Main

Juvix/Core/Main/Language/Context.lean

@@ -35,4 +35,20 @@ def Context.subst (C : Context) (e : Expr) : Expr :=
   | Context.branch_right constr body C' => Expr.branch constr body (C'.subst e)
   | Context.default C' => Expr.default (C'.subst e)
 
+def Context.dom (C : Context) : Set Name :=
+  match C with
+  | Context.hole => ∅
+  | Context.app_left C' e => C'.dom ∪ e.dom
+  | Context.app_right e C' => C'.dom ∪ e.dom
+  | Context.constr_app_left C' e => C'.dom ∪ e.dom
+  | Context.constr_app_right e C' => C'.dom ∪ e.dom
+  | Context.binop_left _ C₁ e => C₁.dom ∪ e.dom
+  | Context.binop_right _ e C₂ => C₂.dom ∪ e.dom
+  | Context.lambda C' => C'.dom
+  | Context.save_left C' e => C'.dom ∪ e.dom
+  | Context.save_right e C' => C'.dom ∪ e.dom
+  | Context.branch_left _ C' e => C'.dom ∪ e.dom
+  | Context.branch_right _ e C' => C'.dom ∪ e.dom
+  | Context.default C' => C'.dom
+
 end Juvix.Core.Main

Juvix/Core/Main/Language/Value.lean

@@ -12,4 +12,45 @@ inductive Value : Type where
 
 abbrev Env : Type := List Value
 
+mutual
+  @[simp]
+  def Value.dom : (v : Value) → Set Name
+    | Value.unit => ∅
+    | Value.const _ => ∅
+    | Value.constr_app _ args_rev => Value.List.dom args_rev
+    | Value.closure env body => Value.List.dom env ∪ body.dom
+
+  @[simp]
+  def Value.List.dom : (vs : List Value) → Set Name
+    | [] => ∅
+    | v :: vs => v.dom ∪ Value.List.dom vs
+end
+
+@[simp]
+def Env.dom : (env : Env) → Set Name :=
+  Value.List.dom
+
+lemma Value.dom_env (v : Value) (env : Env) : v ∈ env → v.dom ⊆ env.dom := by
+  intro h
+  induction env generalizing v
+  case nil =>
+    contradiction
+  case cons hd tl ih =>
+    cases h
+    case head =>
+      simp [Value.dom, Value.List.dom]
+    case tail hm =>
+      simp [Value.dom, Value.List.dom]
+      exact Set.subset_union_of_subset_right (ih v hm) hd.dom
+
+lemma Value.List.dom_append (vs₁ vs₂ : List Value) :
+  Value.List.dom (vs₁ ++ vs₂) = Value.List.dom vs₁ ∪ Value.List.dom vs₂ := by
+  induction vs₁ generalizing vs₂
+  case nil =>
+    simp [Value.List.dom]
+  case cons hd tl ih =>
+    simp [Value.List.dom]
+    rw [ih]
+    rw [Set.union_assoc]
+
 end Juvix.Core.Main