Commit 94216199 authored by Robbert Krebbers's avatar Robbert Krebbers

Give the project a top-level name so it can be make installed.

Thanks to Amin Timany for the suggestion.
parent d72200d0
Pipeline #301 passed with stage
-Q . ""
-Q . iris
prelude/option.v
prelude/fin_map_dom.v
prelude/bsets.v
......
From algebra Require Export cmra.
From algebra Require Import upred.
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
Local Hint Extern 10 (_ _) => omega.
Record agree (A : Type) : Type := Agree {
......
From algebra Require Export excl.
From algebra Require Import upred.
From iris.algebra Require Export excl.
From iris.algebra Require Import upred.
Local Arguments valid _ _ !_ /.
Local Arguments validN _ _ _ !_ /.
......
From mathcomp Require Export ssreflect.
From prelude Require Export prelude.
From iris.prelude Require Export prelude.
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
Ltac done := prelude.tactics.done.
\ No newline at end of file
From algebra Require Export cofe.
From iris.algebra Require Export cofe.
Class Core (A : Type) := core : A A.
Instance: Params (@core) 2.
......
From algebra Require Export cmra.
From prelude Require Import gmap.
From iris.algebra Require Export cmra.
From iris.prelude Require Import gmap.
Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
match xs with [] => | x :: xs => x big_op xs end.
......
From algebra Require Export cmra.
From algebra Require Import cmra_big_op.
From iris.algebra Require Export cmra.
From iris.algebra Require Import cmra_big_op.
(** * Simple solver for validity and inclusion by reflection *)
Module ra_reflection. Section ra_reflection.
......
From algebra Require Export base.
From iris.algebra Require Export base.
(** This files defines (a shallow embedding of) the category of COFEs:
Complete ordered families of equivalences. This is a cartesian closed
......
From algebra Require Export cofe.
From iris.algebra Require Export cofe.
Record solution (F : cFunctor) := Solution {
solution_car :> cofeT;
......
From algebra Require Export cmra.
From iris.algebra Require Export cmra.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
......
From algebra Require Export cmra.
From iris.algebra Require Export cmra.
(** From disjoint pcm *)
Record validity {A} (P : A Prop) : Type := Validity {
......
From algebra Require Export cmra.
From algebra Require Import upred.
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
......
From algebra Require Export cmra option.
From prelude Require Export gmap.
From algebra Require Import upred.
From iris.algebra Require Export cmra option.
From iris.prelude Require Export gmap.
From iris.algebra Require Import upred.
Section cofe.
Context `{Countable K} {A : cofeT}.
......
From Coq.QArith Require Import Qcanon.
From algebra Require Export cmra.
From algebra Require Import upred.
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments div _ _ !_ !_ /.
......
From algebra Require Export cmra.
From algebra Require Import upred.
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
(** * Indexed product *)
(** Need to put this in a definition to make canonical structures to work. *)
......
From algebra Require Export cmra.
From algebra Require Import upred.
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
(* COFE *)
Section cofe.
......
From prelude Require Export sets.
From algebra Require Export cmra.
From algebra Require Import dra.
From iris.prelude Require Export sets.
From iris.algebra Require Export cmra.
From iris.algebra Require Import dra.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments core _ _ !_ /.
......
From algebra Require Export cmra.
From iris.algebra Require Export cmra.
Local Hint Extern 1 (_ _) => etrans; [eassumption|].
Local Hint Extern 1 (_ _) => etrans; [|eassumption].
Local Hint Extern 10 (_ _) => omega.
......
From algebra Require Export upred.
From prelude Require Import gmap fin_collections.
From iris.algebra Require Export upred.
From iris.prelude Require Import gmap fin_collections.
Import uPred.
(** * Big ops over lists *)
......
From algebra Require Export upred.
From algebra Require Export upred_big_op.
From iris.algebra Require Export upred.
From iris.algebra Require Export upred_big_op.
Import uPred.
Module uPred_reflection. Section uPred_reflection.
......
From heap_lang Require Export notation.
From iris.heap_lang Require Export notation.
Definition newbarrier : val := λ: <>, ref #0.
Definition signal : val := λ: "x", '"x" <- #1.
......
From barrier Require Import proof.
From heap_lang Require Import par.
From program_logic Require Import auth sts saved_prop hoare ownership.
From iris.barrier Require Import proof.
From iris.heap_lang Require Import par.
From iris.program_logic Require Import auth sts saved_prop hoare ownership.
Import uPred.
Definition worker (n : Z) : val :=
......
From prelude Require Import functions.
From algebra Require Import upred_big_op.
From program_logic Require Import sts saved_prop tactics.
From heap_lang Require Export heap wp_tactics.
From barrier Require Export barrier.
From barrier Require Import protocol.
From iris.prelude Require Import functions.
From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Import sts saved_prop tactics.
From iris.heap_lang Require Export heap wp_tactics.
From iris.barrier Require Export barrier.
From iris.barrier Require Import protocol.
Import uPred.
(** The CMRAs we need. *)
......
From algebra Require Export sts.
From program_logic Require Import ghost_ownership.
From iris.algebra Require Export sts.
From iris.program_logic Require Import ghost_ownership.
(** The STS describing the main barrier protocol. Every state has an index-set
associated with it. These indices are actually [gname], because we use them
......
From program_logic Require Export hoare.
From barrier Require Export barrier.
From barrier Require Import proof.
From iris.program_logic Require Export hoare.
From iris.barrier Require Export barrier.
From iris.barrier Require Import proof.
Import uPred.
Section spec.
......
From heap_lang Require Export lifting.
From iris.heap_lang Require Export lifting.
Import uPred.
(** Define some derived forms, and derived lemmas about them. *)
......
From heap_lang Require Export lifting.
From algebra Require Import upred_big_op frac dec_agree.
From program_logic Require Export invariants ghost_ownership.
From program_logic Require Import ownership auth.
From iris.heap_lang Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
Import uPred.
(* TODO: The entire construction could be generalized to arbitrary languages that have
a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
......
From program_logic Require Export language.
From prelude Require Export strings.
From prelude Require Import gmap.
From iris.program_logic Require Export language.
From iris.prelude Require Export strings.
From iris.prelude Require Import gmap.
Module heap_lang.
Open Scope Z_scope.
......
From program_logic Require Export weakestpre.
From heap_lang Require Export lang.
From program_logic Require Import lifting.
From program_logic Require Import ownership. (* for ownP *)
From heap_lang Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.program_logic Require Import lifting.
From iris.program_logic Require Import ownership. (* for ownP *)
From iris.heap_lang Require Import tactics.
Import uPred.
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
......
From heap_lang Require Export derived.
From iris.heap_lang Require Export derived.
Export heap_lang.
Arguments wp {_ _} _ _%E _.
......
From heap_lang Require Export heap spawn.
From heap_lang Require Import wp_tactics notation.
From iris.heap_lang Require Export heap spawn.
From iris.heap_lang Require Import wp_tactics notation.
Import uPred.
Definition par : val :=
......
From program_logic Require Export global_functor.
From heap_lang Require Export heap.
From heap_lang Require Import wp_tactics notation.
From iris.program_logic Require Export global_functor.
From iris.heap_lang Require Export heap.
From iris.heap_lang Require Import wp_tactics notation.
Import uPred.
Definition spawn : val :=
......
From heap_lang Require Export lang.
From iris.heap_lang Require Export lang.
Import heap_lang.
(** The tactic [simpl_subst] performs substitutions in the goal. Its behavior
......
From heap_lang Require Export substitution.
From prelude Require Import fin_maps.
From iris.heap_lang Require Export substitution.
From iris.prelude Require Import fin_maps.
Import heap_lang.
(** The tactic [inv_step] performs inversion on hypotheses of the shape
......
(** This file is essentially a bunch of testcases. *)
From program_logic Require Import ownership hoare auth.
From heap_lang Require Import wp_tactics heap notation.
From iris.program_logic Require Import ownership hoare auth.
From iris.heap_lang Require Import wp_tactics heap notation.
Import uPred.
Section LangTests.
......
From algebra Require Export upred_tactics.
From heap_lang Require Export tactics derived substitution.
From iris.algebra Require Export upred_tactics.
From iris.heap_lang Require Export tactics derived substitution.
Import uPred.
(** wp-specific helper tactics *)
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements bsets as functions into Prop. *)
From prelude Require Export prelude.
From iris.prelude Require Export prelude.
Record bset (A : Type) : Type := mkBSet { bset_car : A bool }.
Arguments mkBSet {_} _.
......
......@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** This files implements an efficient implementation of finite/cofinite sets
of positive binary naturals [positive]. *)
From prelude Require Export collections.
From prelude Require Import pmap gmap mapset.
From iris.prelude Require Export collections.
From iris.prelude Require Import pmap gmap mapset.
Local Open Scope positive_scope.
(** * The tree data structure *)
......
......@@ -3,7 +3,7 @@
(** This file collects definitions and theorems on collections. Most
importantly, it implements some tactics to automatically solve goals involving
collections. *)
From prelude Require Export base tactics orders.
From iris.prelude Require Export base tactics orders.
Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
x, x X x Y.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From prelude Require Export list.
From iris.prelude Require Export list.
Local Open Scope positive.
Class Countable A `{ x y : A, Decision (x = y)} := {
......
......@@ -3,7 +3,7 @@
(** This file collects theorems, definitions, tactics, related to propositions
with a decidable equality. Such propositions are collected by the [Decision]
type class. *)
From prelude Require Export proof_irrel.
From iris.prelude Require Export proof_irrel.
Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From prelude Require Export list.
From iris.prelude Require Export list.
Definition error (S E A : Type) : Type := S E + (A * S).
......
......@@ -4,8 +4,8 @@
importantly, it implements a fold and size function and some useful induction
principles on finite collections . *)
From Coq Require Import Permutation.
From prelude Require Import relations listset.
From prelude Require Export numbers collections.
From iris.prelude Require Import relations listset.
From iris.prelude Require Export numbers collections.
Instance collection_size `{Elements A C} : Size C := length elements.
Definition collection_fold `{Elements A C} {B}
......
......@@ -3,7 +3,7 @@
(** This file provides an axiomatization of the domain function of finite
maps. We provide such an axiomatization, instead of implementing the domain
function in a generic way, to allow more efficient implementations. *)
From prelude Require Export collections fin_maps.
From iris.prelude Require Export collections fin_maps.
Class FinMapDom K M D `{FMap M,
A, Lookup K A (M A), A, Empty (M A), A, PartialAlter K A (M A),
......
......@@ -5,7 +5,7 @@ finite maps and collects some theory on it. Most importantly, it proves useful
induction principles for finite maps and implements the tactic
[simplify_map_eq] to simplify goals involving finite maps. *)
From Coq Require Import Permutation.
From prelude Require Export relations vector orders.
From iris.prelude Require Export relations vector orders.
(** * Axiomatization of finite maps *)
(** We require Leibniz equality to be extensional on finite maps. This of
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From prelude Require Export countable list.
From iris.prelude Require Export countable list.
Class Finite A `{ x y : A, Decision (x = y)} := {
enum : list A;
......
From prelude Require Export base tactics.
From iris.prelude Require Export base tactics.
Section definitions.
Context {A T : Type} `{ a b : A, Decision (a = b)}.
......
......@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite maps and finite sets with keys of any countable
type. The implementation is based on [Pmap]s, radix-2 search trees. *)
From prelude Require Export countable fin_maps fin_map_dom.
From prelude Require Import pmap mapset sets.
From iris.prelude Require Export countable fin_maps fin_map_dom.
From iris.prelude Require Import pmap mapset sets.
(** * The data structure *)
(** We pack a [Pmap] together with a proof that ensures that all keys correspond
......
......@@ -3,8 +3,8 @@
(** This file implements finite set using hash maps. Hash sets are represented
using radix-2 search trees. Each hash bucket is thus indexed using an binary
integer of type [Z], and contains an unordered list without duplicates. *)
From prelude Require Export fin_maps listset.
From prelude Require Import zmap.
From iris.prelude Require Export fin_maps listset.
From iris.prelude Require Import zmap.
Record hashset {A} (hash : A Z) := Hashset {
hashset_car : Zmap (list A);
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This files defines a lexicographic order on various common data structures
and proves that it is a partial order having a strong variant of trichotomy. *)
From prelude Require Import numbers.
From iris.prelude Require Import numbers.
Notation cast_trichotomy T :=
match T with
......
......@@ -3,7 +3,7 @@
(** This file collects general purpose definitions and theorems on lists that
are not in the Coq standard library. *)
From Coq Require Export Permutation.
From prelude Require Export numbers base option.
From iris.prelude Require Export numbers base option.
Arguments length {_} _.
Arguments cons {_} _ _.
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file implements finite set as unordered lists without duplicates
removed. This implementation forms a monad. *)
From prelude Require Export collections list.
From iris.prelude Require Export collections list.
Record listset A := Listset { listset_car: list A }.
Arguments listset_car {_} _.
......
......@@ -3,7 +3,7 @@
(** This file implements finite as unordered lists without duplicates.
Although this implementation is slow, it is very useful as decidable equality
is the only constraint on the carrier set. *)
From prelude Require Export collections list.
From iris.prelude Require Export collections list.
Record listset_nodup A := ListsetNoDup {
listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
......
......@@ -3,7 +3,7 @@
(** This files gives an implementation of finite sets using finite maps with
elements of the unit type. Since maps enjoy extensional equality, the
constructed finite sets do so as well. *)
From prelude Require Export fin_map_dom.
From iris.prelude Require Export fin_map_dom.
Record mapset (M : Type Type) : Type :=
Mapset { mapset_car: M (unit : Type) }.
......
......@@ -3,7 +3,7 @@
(** This files implements a type [natmap A] of finite maps whose keys range
over Coq's data type of unary natural numbers [nat]. The implementation equips
a list with a proof of canonicity. *)
From prelude Require Import fin_maps mapset.
From iris.prelude Require Import fin_maps mapset.
Notation natmap_raw A := (list (option A)).
Definition natmap_wf {A} (l : natmap_raw A) :=
......
......@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [N]. *)
From prelude Require Import pmap mapset.
From prelude Require Export prelude fin_maps.
From iris.prelude Require Import pmap mapset.
From iris.prelude Require Export prelude fin_maps.
Local Open Scope N_scope.
......
......@@ -5,7 +5,7 @@ natural numbers, and the type [Z] for integers. It also declares some useful
notations. *)
From Coq Require Export Eqdep PArith NArith ZArith NPeano.
From Coq Require Import QArith Qcanon.
From prelude Require Export base decidable option.
From iris.prelude Require Export base decidable option.
Open Scope nat_scope.
Coercion Z.of_nat : nat >-> Z.
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose definitions and theorems on the option
data type that are not in the Coq standard library. *)
From prelude Require Export tactics.
From iris.prelude Require Export tactics.
Inductive option_reflect {A} (P : A Prop) (Q : Prop) : option A Type :=
| ReflectSome x : P x option_reflect P Q (Some x)
......
......@@ -3,7 +3,7 @@
(** This file collects common properties of pre-orders and semi lattices. This
theory will mainly be used for the theory on collections and finite maps. *)
From Coq Require Export Sorted.
From prelude Require Export tactics list.
From iris.prelude Require Export tactics list.
(** * Arbitrary pre-, parial and total orders *)
(** Properties about arbitrary pre-, partial, and total orders. We do not use
......
......@@ -8,8 +8,8 @@ However, we extend Leroy's implementation by packing the trees into a Sigma
type such that canonicity of representation is ensured. This is necesarry for
Leibniz equality to become extensional. *)
From Coq Require Import PArith.
From prelude Require Import mapset.
From prelude Require Export fin_maps.
From iris.prelude Require Import mapset.
From iris.prelude Require Export fin_maps.
Local Open Scope positive_scope.
Local Hint Extern 0 (@eq positive _ _) => congruence.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From prelude Require Export
From iris.prelude Require Export
base
tactics
orders
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From prelude Require Export strings.
From prelude Require Import relations.
From iris.prelude Require Export strings.
From iris.prelude Require Import relations.
From Coq Require Import Ascii.
Class Pretty A := pretty : A string.
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
(** This file collects facts on proof irrelevant types/propositions. *)
From Coq Require Import Eqdep_dec.
From prelude Require Export base.
From iris.prelude Require Export base.
Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
......
......@@ -5,7 +5,7 @@ These are particularly useful as we define the operational semantics as a
small step semantics. This file defines a hint database [ars] containing
some theorems on abstract rewriting systems. *)
From Coq Require Import Wf_nat.
From prelude Require Export tactics base.
From iris.prelude Require Export tactics base.
(** * Definitions *)
Section definitions.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements sets as functions into Prop. *)
From prelude Require Export collections.
From iris.prelude Require Export collections.
Record set (A : Type) : Type := mkSet { set_car : A Prop }.
Add Printing Constructor set.
......
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
From prelude Require Export tactics.
From iris.prelude Require Export tactics.
CoInductive stream (A : Type) : Type := scons : A stream A stream A.
Arguments scons {_} _ _.
......
......@@ -4,8 +4,8 @@
range over Coq's data type of strings [string]. The implementation uses radix-2
search trees (uncompressed Patricia trees) as implemented in the file [pmap]
and guarantees logarithmic-time operations. *)
From prelude Require Export fin_maps pretty.
From prelude Require Import gmap.
From iris.prelude Require Export fin_maps pretty.
From iris.prelude Require Import gmap.
Notation stringmap := (gmap string).
Notation stringset := (gset string).
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
From Coq Require Import Ascii.
From Coq Require Export String.
From prelude Require Export countable.
From iris.prelude Require Export countable.
(** * Fix scopes *)
Open Scope string_scope.
......
......@@ -4,7 +4,7 @@
the development. *)
From Coq Require Import Omega.
From Coq Require Export Psatz.
From prelude Require Export decidable.
From iris.prelude Require Export decidable.
Lemma f_equal_dep {A B} (f g : x : A, B x) x : f = g f x = g x.
Proof. intros ->; reflexivity. Qed.
......
......@@ -5,7 +5,7 @@
definitions from the standard library, but renames or changes their notations,
so that it becomes more consistent with the naming conventions in this
development. *)
From prelude Require Import list finite.
From iris.prelude Require Import list finite.
Open Scope vector_scope.
(** * The fin type *)
......
......@@ -2,8 +2,8 @@
(* This file is distributed under the terms of the BSD license. *)
(** This files extends the implementation of finite over [positive] to finite
maps whose keys range over Coq's data type of binary naturals [Z]. *)
From prelude Require Import pmap mapset.
From prelude Require Export prelude fin_maps.
From iris.prelude Require Import pmap mapset.
From iris.prelude Require Export prelude fin_maps.
Local Open Scope Z_scope.
Record Zmap (A : Type) : Type :=
......