Commit aae79b93 authored by Amin Timany's avatar Amin Timany
Browse files

coqdoc for sem_typed.v

parent 29cb84fa
...@@ -32,3 +32,4 @@ Makefile.coq* ...@@ -32,3 +32,4 @@ Makefile.coq*
build-dep build-dep
_opam _opam
.lia.cache .lia.cache
/html
From tutorial_popl20 Require Export sem_type_formers. From tutorial_popl20 Require Export sem_type_formers.
(* The semantic typing judgment *) (** * Here we define the semantic typing judgment. *)
(** We define the judgment [Γ ⊨ e : A] for semantic typing of the
expression [e] at semantic type [A], assuming that free variables
in [e] belong to the semantic types described by [Γ]. This notion
is defined as follows:
- We define the semantic typing relation [env_sem_typed] for
typing contexts: An environments (mappings from free variables
to values) [vs] is in the semantic type for a typing context
[Γ], [env_sem_typed Γ vs], if for any free variable [x], [vs(x)]
is in the semantic type [Γ(x)].
- The semantic typing judgment [Γ ⊨ e : A] holds if for any
environment [vs] such that [env_sem_typed Γ vs] we have that
[subst_map vs e] is an expression in the semantics of type [A],
i.e., [WP subst_map vs e {{ A }}] holds. *)
(** The semantic type for the typing context (environment). *)
Definition env_sem_typed `{heapG Σ} (Γ : gmap string (sem_ty Σ)) Definition env_sem_typed `{heapG Σ} (Γ : gmap string (sem_ty Σ))
(vs : gmap string val) : iProp Σ := (vs : gmap string val) : iProp Σ :=
([ map] i A;v Γ; vs, sem_ty_car A v)%I. ([ map] i A;v Γ; vs, sem_ty_car A v)%I.
Instance: Params (@env_sem_typed) 2 := {}. Instance: Params (@env_sem_typed) 2 := {}.
(** The semantics typing judgment. *)
Definition sem_typed `{heapG Σ} Definition sem_typed `{heapG Σ}
(Γ : gmap string (sem_ty Σ)) (e : expr) (A : sem_ty Σ) : iProp Σ := (Γ : gmap string (sem_ty Σ)) (e : expr) (A : sem_ty Σ) : iProp Σ :=
tc_opaque ( vs, env_sem_typed Γ vs - WP subst_map vs e {{ A }})%I. tc_opaque ( vs, env_sem_typed Γ vs - WP subst_map vs e {{ A }})%I.
...@@ -12,6 +33,9 @@ Instance: Params (@sem_typed) 2 := {}. ...@@ -12,6 +33,9 @@ Instance: Params (@sem_typed) 2 := {}.
Notation "Γ ⊨ e : A" := (sem_typed Γ e A) Notation "Γ ⊨ e : A" := (sem_typed Γ e A)
(at level 100, e at next level, A at level 200). (at level 100, e at next level, A at level 200).
(** A few useful lemmas about the semantic typing judgment. The first
few lemmas involving [Proper]ness are boilerplate required for supporting setoid
rewriting. *)
Section sem_typed. Section sem_typed.
Context `{heapG Σ}. Context `{heapG Σ}.
Implicit Types A B : sem_ty Σ. Implicit Types A B : sem_ty Σ.
......
...@@ -2,17 +2,14 @@ From tutorial_popl20 Require Export base. ...@@ -2,17 +2,14 @@ From tutorial_popl20 Require Export base.
From iris.heap_lang Require Export proofmode. From iris.heap_lang Require Export proofmode.
From iris.base_logic.lib Require Export invariants. From iris.base_logic.lib Require Export invariants.
(** (** * The domain of semantics types. *)
* The domain of semantics types.
*)
(** Here we define the domain of semantics types as persistent iris (** Here we define the domain of semantics types as persistent iris
predicates over values. That is, to capture the semantics of a predicates over values. That is, to capture the semantics of a
type [τ], we need to define what programs are belong to the type [τ], we need to define what programs are belong to the
semantics of [τ]. We do this in two steps: semantics of [τ]. We do this in two steps:
(1) We define what values semantically belong to type [τ] - We define what values semantically belong to type [τ]
(2) We define the expressions that semantically belong to [τ]. An - We define the expressions that semantically belong to [τ]. An
expression [e] semantically belongs to type [τ] if [e] is expression [e] semantically belongs to type [τ] if [e] is
_safe_, and whenever it evaluates to a value [v], [v] _safe_, and whenever it evaluates to a value [v], [v]
semantically belongs to [τ]. semantically belongs to [τ].
...@@ -26,8 +23,7 @@ From iris.base_logic.lib Require Export invariants. ...@@ -26,8 +23,7 @@ From iris.base_logic.lib Require Export invariants.
opposed to substructural type systems, e.g., affine type systems) opposed to substructural type systems, e.g., affine type systems)
allows values to be used multiple times. Hence, the fact that a allows values to be used multiple times. Hence, the fact that a
value belongs to the semantics of a type must be duplicable which value belongs to the semantics of a type must be duplicable which
is guaranteed by persistence. is guaranteed by persistence. *)
*)
(* The domain of semantic types: persistent Iris predicates over values *) (* The domain of semantic types: persistent Iris predicates over values *)
Record sem_ty Σ := SemTy { Record sem_ty Σ := SemTy {
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment