RSAPredict Goal Parsing

Recognize comparison goal forms and extract RSA config/utterance/world arguments from L1, L1_latent, and S1 policy expressions.

def Linglib.Tactics.RSAPredict.unfoldToPolicy (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Try to unfold an expression to RationalAction.policy ra s a.

Equations

• One or more equations did not get rendered due to their size.

def Linglib.Tactics.RSAPredict.parseL1Policy (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Extract RSA config and arguments from a policy expression. Returns (cfg, u, w) where the expression is cfg.L1 u w.

Equations

• One or more equations did not get rendered due to their size.

def Linglib.Tactics.RSAPredict.parseL0Policy (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))

Extract RSA config and arguments from a policy expression. Returns (cfg, l, u, w) where the expression is cfg.L0 l u w.

Equations

• One or more equations did not get rendered due to their size.

def Linglib.Tactics.RSAPredict.parseS1Policy (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))

Extract RSA config and arguments from a policy expression. Returns (cfg, l, w, u) where the expression is cfg.S1 l w u.

Equations

• One or more equations did not get rendered due to their size.

def Linglib.Tactics.RSAPredict.parseS2Utility (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Try to parse an expression as d.S2Utility w u. Returns (d, w, u) where the expression is RSAConfigData.S2Utility d w u.

Equations

• One or more equations did not get rendered due to their size.

def Linglib.Tactics.RSAPredict.parseS2Policy (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Extract RSA config and arguments from an S2 policy expression. Returns (cfg, w, u) where the expression is cfg.S2 w u.

Equations

• One or more equations did not get rendered due to their size.

inductive Linglib.Tactics.RSAPredict.GoalForm : Type

Parsed goal forms that rsa_predict can handle.

• l1Compare (cfg u w₁ w₂ : Lean.Expr) : GoalForm

  cfg.L1 u w₁ > cfg.L1 u w₂

• l1Marginal (cfg u : Lean.Expr) (ws₁ ws₂ : Array Lean.Expr) : GoalForm

  (ws₁.map (cfg.L1 u)).sum > (ws₂.map (cfg.L1 u)).sum (marginal)

• l1Latent (cfg u l₁ l₂ : Lean.Expr) : GoalForm

  cfg.L1_latent u l₁ > cfg.L1_latent u l₂

• l1CrossUtterance (cfg u₁ : Lean.Expr) (ws₁ : Array Lean.Expr) (u₂ : Lean.Expr) (ws₂ : Array Lean.Expr) : GoalForm

  (ws₁.map (cfg.L1 u₁)).sum > (ws₂.map (cfg.L1 u₂)).sum (cross-utterance)

• l1CrossConfig (cfg₁ u₁ : Lean.Expr) (ws₁ : Array Lean.Expr) (cfg₂ u₂ : Lean.Expr) (ws₂ : Array Lean.Expr) : GoalForm

  (ws₁.map (cfg₁.L1 u₁)).sum > (ws₂.map (cfg₂.L1 u₂)).sum (cross-config)

• s1Compare (cfg l w u₁ u₂ : Lean.Expr) : GoalForm

  cfg.S1 l w u₁ > cfg.S1 l w u₂

• s2Compare (cfg w₁ w₂ u : Lean.Expr) : GoalForm

  cfg.S2 w₁ u > cfg.S2 w₂ u

• s2UtilityCompare (d w u₁ u₂ : Lean.Expr) : GoalForm

  d.S2Utility w u₁ > d.S2Utility w u₂

• l0Compare (cfg l u w₁ w₂ : Lean.Expr) : GoalForm

  cfg.L0 l u w₁ > cfg.L0 l u w₂

• l0Marginal (cfg l u : Lean.Expr) (ws₁ ws₂ : Array Lean.Expr) : GoalForm

  (ws₁.map (cfg.L0 l u)).sum > (ws₂.map (cfg.L0 l u)).sum (L0 marginal)

def Linglib.Tactics.RSAPredict.parseL1Marginal (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Array Lean.Expr))

Try to parse an expression as cfg.L1_marginal u P. If successful, evaluates P w for each w : W at meta level, returning (cfg, u, #[w₁, w₂,...]) for matching worlds.

Equations

• One or more equations did not get rendered due to their size.

def Linglib.Tactics.RSAPredict.parseL0Marginal (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × Array Lean.Expr))

Try to parse an expression as cfg.L0_marginal l u P. If successful, evaluates P w for each w : W at meta level, returning (cfg, l, u, #[w₁, w₂,...]) for matching worlds.

Equations

• One or more equations did not get rendered due to their size.

def Linglib.Tactics.RSAPredict.parseL1Latent (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Try to unfold an expression to cfg.L1_latent u l.

Equations

• One or more equations did not get rendered due to their size.

partial def Linglib.Tactics.RSAPredict.collectL1Summands (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Array Lean.Expr))

Collect L1 policy summands from an expression. Returns (cfg, u, ws) where ws are the world arguments, or none. Handles Finset.sum, List.sum of map, and nested HAdd of L1 terms.

partial def Linglib.Tactics.RSAPredict.collectL1SummandsAnyU (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Array (Lean.Expr × Array Lean.Expr)))

Collect L1 summands allowing different utterances on each side. Returns (cfg, u, ws) pairs. For cross-utterance goals, the two sides may have different u values.

partial def Linglib.Tactics.RSAPredict.collectL0Summands (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × Array Lean.Expr))

Collect L0 policy summands from an expression. Returns (cfg, l, u, ws) where ws are the world arguments, or none. Handles L0_marginal, single L0 terms, nested HAdd, and Finset.sum.

def Linglib.Tactics.RSAPredict.parseGoalForm (lhs rhs : Lean.Expr) : Lean.MetaM GoalForm

Parse the goal into a GoalForm.

Equations

• One or more equations did not get rendered due to their size.