Core C++

3.3. Unary operators🔗

Definition3.3.1
Group: Values, types and expressions. (12)
Group member previews
Preview
Definition 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

Logical negation requires bool and arithmetic negation requires int. Negation goes through \mathsf{int32}, because the negation of -2^{31} overflows.

\dfrac{\Gamma \vdash e : \mathsf{bool}}{\Gamma \vdash\, !e : \mathsf{bool}}\;\textsf{(T-Not)}

\dfrac{\Gamma \vdash e : \mathsf{int}}{\Gamma \vdash -e : \mathsf{int}}\;\textsf{(T-Neg)}

\dfrac{\rho, \sigma \vdash e \Rightarrow \mathsf{bool}\,b, \sigma'}{\rho, \sigma \vdash\, !e \Rightarrow \mathsf{bool}\,\neg b, \sigma'}\;\textsf{(Not)}

\dfrac{\rho, \sigma \vdash e \Rightarrow \mathsf{int}\,n, \sigma'}{\rho, \sigma \vdash -e \Rightarrow \mathsf{int32}(-n), \sigma'}\;\textsf{(Neg)}

In the code, the case Unary of Eval.expr evaluates the operand and calls Eval.unop.

Some of the implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.

Lean code for Definition3.3.1●4 definitions
  • opaquedefined in CoreCpp/Typing.lean
    complete
    opaque CoreCpp.Typing.expr (p : CoreCpp.Program) (Γ : CoreCpp.TEnv) :
  CoreCpp.Expr → CoreCpp.T CoreCpp.Ty
    opaque CoreCpp.Typing.expr (p : CoreCpp.Program)
  (Γ : CoreCpp.TEnv) :
  CoreCpp.Expr → CoreCpp.T CoreCpp.Ty
    Γ ⊢ e : τ
  • opaquedefined in CoreCpp/Eval.lean
    complete
    opaque CoreCpp.Eval.expr (fs : CoreCpp.FunEnv) (ρ : CoreCpp.Env)
  (σ : CoreCpp.Store) (e : CoreCpp.Expr) :
  CoreCpp.M (CoreCpp.Val × CoreCpp.Store)
    opaque CoreCpp.Eval.expr (fs : CoreCpp.FunEnv)
  (ρ : CoreCpp.Env) (σ : CoreCpp.Store)
  (e : CoreCpp.Expr) :
  CoreCpp.M (CoreCpp.Val × CoreCpp.Store)
    ρ, σ ⊢ e ⇒ v, σ'
  • inductive(2 constructors)defined in CoreCpp/Syntax.lean
    complete
    inductive CoreCpp.UnOp : Type
    inductive CoreCpp.UnOp : Type

    Constructors

    CoreCpp.UnOp.not : CoreCpp.UnOp
    CoreCpp.UnOp.neg : CoreCpp.UnOp
  • defdefined in CoreCpp/Eval.lean
    complete
    def CoreCpp.Eval.unop : CoreCpp.UnOp → CoreCpp.Val → CoreCpp.M CoreCpp.Val
    def CoreCpp.Eval.unop :
  CoreCpp.UnOp →
    CoreCpp.Val → CoreCpp.M CoreCpp.Val
    Unary operators.

```
ρ, σ ⊢ e ⇒ bool b, σ'                    ρ, σ ⊢ e ⇒ int n, σ'
──────────────────────── (Not)           ────────────────────────── (Neg)
ρ, σ ⊢ !e ⇒ bool ¬b, σ'                  ρ, σ ⊢ −e ⇒ int32 (−n), σ'
```