Commit fe406700 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' of gitlab.mpi-sws.org:iris/tutorial-popl20

parents e7409376 810f6a9f
From solutions Require Export sem_typed sem_operators. From exercises Require Export sem_typed sem_operators.
(** * Compatibility lemmas *) (** * Compatibility lemmas *)
(** We prove that the logical relations, i.e., the semantic typing judgment, (** We prove that the logical relations, i.e., the semantic typing judgment,
......
From solutions Require Import language. From exercises Require Import language.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import adequacy. From iris.heap_lang Require Import adequacy.
......
From solutions Require Export typed compatibility interp. From exercises Require Export typed compatibility interp.
(** * The fundamental theorem of logical relations *) (** * The fundamental theorem of logical relations *)
(** The fundamental theorem of logical relations says that any syntactically (** The fundamental theorem of logical relations says that any syntactically
......
From solutions Require Export sem_typed sem_type_formers types. From exercises Require Export sem_typed sem_type_formers types.
(** * Interpretation of syntactic types *) (** * Interpretation of syntactic types *)
(** We use semantic type formers to define the interpretation [⟦ τ ⟧ : sem_ty] (** We use semantic type formers to define the interpretation [⟦ τ ⟧ : sem_ty]
......
From solutions Require Export safety. From exercises Require Export safety.
(** * Parametricity *) (** * Parametricity *)
Section parametricity. Section parametricity.
......
From solutions Require Export language. From exercises Require Export language.
(** * Polymorphism and existential types in HeapLang *) (** * Polymorphism and existential types in HeapLang *)
(** In order to define a type system for HeapLang (in the file [typed.v]), we (** In order to define a type system for HeapLang (in the file [typed.v]), we
......
From iris.heap_lang Require Export adequacy. From iris.heap_lang Require Export adequacy.
From solutions Require Export fundamental. From exercises Require Export fundamental.
(** * Semantic and syntactic type safety *) (** * Semantic and syntactic type safety *)
(** We prove *semantic type safety*, which says that any _closed_ expression (** We prove *semantic type safety*, which says that any _closed_ expression
......
From solutions Require Export sem_typed. From exercises Require Export sem_typed.
(** Semantic operator typing *) (** Semantic operator typing *)
Class SemTyUnboxed `{!heapG Σ} (A : sem_ty Σ) := Class SemTyUnboxed `{!heapG Σ} (A : sem_ty Σ) :=
......
From solutions Require Export sem_types. From exercises Require Export sem_types.
(** * Semantic type formers *) (** * Semantic type formers *)
(** For all of the type formers in the syntactic type system, we now define (** For all of the type formers in the syntactic type system, we now define
......
From solutions Require Export sem_type_formers. From exercises Require Export sem_type_formers.
(** * The semantic typing judgment *) (** * The semantic typing judgment *)
......
From solutions Require Export polymorphism. From exercises Require Export polymorphism.
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.
......
From solutions Require Export types polymorphism. From exercises Require Export types polymorphism.
(** * Syntactic typing for HeapLang *) (** * Syntactic typing for HeapLang *)
(** In this file, we define a syntactic type system for HeapLang. We do this (** In this file, we define a syntactic type system for HeapLang. We do this
......
From solutions Require Export language. From exercises Require Export language.
(** * Syntactic types for HeapLang *) (** * Syntactic types for HeapLang *)
(** The inductive type [ty] defines the syntactic types for HeapLang. We make (** The inductive type [ty] defines the syntactic types for HeapLang. We make
......
From solutions Require Export sem_typed. From exercises Require Export sem_typed.
From solutions Require Import symbol_ghost two_state_ghost. From exercises Require Import symbol_ghost two_state_ghost.
Section unsafe. Section unsafe.
Context `{!heapG Σ}. Context `{!heapG Σ}.
......
...@@ -7,6 +7,7 @@ REMOVEPRF_RE='s/\(\*\s*REMOVE\s*\*\)\s*Proof.\s*.*?\s*Qed\.\R/Proof. (* FILL IN ...@@ -7,6 +7,7 @@ REMOVEPRF_RE='s/\(\*\s*REMOVE\s*\*\)\s*Proof.\s*.*?\s*Qed\.\R/Proof. (* FILL IN
REMOVE_RE='s/\(\*\s*REMOVE\s*\*\)\s*(.*?)\s*:=.*?\.\R/\1. (* FILL IN HERE *) Admitted.\n/gms' REMOVE_RE='s/\(\*\s*REMOVE\s*\*\)\s*(.*?)\s*:=.*?\.\R/\1. (* FILL IN HERE *) Admitted.\n/gms'
STRONGHIDE_RE='s/\(\*\s*STRONGHIDE\s*\*\)\s*(.*?)\(\*\s*ENDSTRONGHIDE\s*\*\)\R?//gms' STRONGHIDE_RE='s/\(\*\s*STRONGHIDE\s*\*\)\s*(.*?)\(\*\s*ENDSTRONGHIDE\s*\*\)\R?//gms'
HIDE_RE='s/\(\*\s*HIDE\s*\*\)\s*(.*?)\(\*\s*ENDHIDE\s*\*\)/Definition hole := remove_this_line.\n(* ANSWER THE QUESTION AND REMOVE THE LINE ABOVE *)/gms' HIDE_RE='s/\(\*\s*HIDE\s*\*\)\s*(.*?)\(\*\s*ENDHIDE\s*\*\)/Definition hole := remove_this_line.\n(* ANSWER THE QUESTION AND REMOVE THE LINE ABOVE *)/gms'
IMPORT_RE='s/^From solutions/From exercises/gms'
# run replacement on all source files # run replacement on all source files
mkdir -p exercises mkdir -p exercises
...@@ -16,5 +17,6 @@ for FILE in solutions/*.v; do ...@@ -16,5 +17,6 @@ for FILE in solutions/*.v; do
| $REPLACE "$REMOVEPRF_RE" \ | $REPLACE "$REMOVEPRF_RE" \
| $REPLACE "$REMOVE_RE" \ | $REPLACE "$REMOVE_RE" \
| $REPLACE "$STRONGHIDE_RE" \ | $REPLACE "$STRONGHIDE_RE" \
| $REPLACE "$HIDE_RE" > "$DST" | $REPLACE "$HIDE_RE" \
| $REPLACE "$IMPORT_RE" > "$DST"
done done
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