Commit 4a272286 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename modures -> algebra and iris -> program_logic.

parent 8f25b2f2
...@@ -34,35 +34,35 @@ prelude/sets.v ...@@ -34,35 +34,35 @@ prelude/sets.v
prelude/decidable.v prelude/decidable.v
prelude/list.v prelude/list.v
prelude/error.v prelude/error.v
modures/option.v algebra/option.v
modures/cmra.v algebra/cmra.v
modures/cmra_big_op.v algebra/cmra_big_op.v
modures/cmra_tactics.v algebra/cmra_tactics.v
modures/sts.v algebra/sts.v
modures/auth.v algebra/auth.v
modures/fin_maps.v algebra/fin_maps.v
modures/logic.v logic/upred.v
modures/cofe.v algebra/cofe.v
modures/base.v algebra/base.v
modures/dra.v algebra/dra.v
modures/cofe_solver.v algebra/cofe_solver.v
modures/agree.v algebra/agree.v
modures/excl.v algebra/excl.v
iris/model.v program_logic/model.v
iris/adequacy.v program_logic/adequacy.v
iris/hoare_lifting.v program_logic/hoare_lifting.v
iris/lifting.v program_logic/lifting.v
iris/namespace.v program_logic/namespace.v
iris/viewshifts.v program_logic/viewshifts.v
iris/wsat.v program_logic/wsat.v
iris/ownership.v program_logic/ownership.v
iris/weakestpre.v program_logic/weakestpre.v
iris/pviewshifts.v program_logic/pviewshifts.v
iris/resources.v program_logic/resources.v
iris/hoare.v program_logic/hoare.v
iris/language.v program_logic/language.v
iris/functor.v program_logic/functor.v
iris/tests.v program_logic/tests.v
heap_lang/heap_lang.v heap_lang/heap_lang.v
heap_lang/heap_lang_tactics.v heap_lang/heap_lang_tactics.v
heap_lang/lifting.v heap_lang/lifting.v
......
Require Export modures.cmra. Require Export algebra.cmra.
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
Record agree (A : Type) : Type := Agree { Record agree (A : Type) : Type := Agree {
......
Require Export modures.excl. Require Export algebra.excl.
Local Arguments validN _ _ _ !_ /. Local Arguments validN _ _ _ !_ /.
Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }. Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
......
Require Export modures.cofe. Require Export algebra.cofe.
Class Unit (A : Type) := unit : A A. Class Unit (A : Type) := unit : A A.
Instance: Params (@unit) 2. Instance: Params (@unit) 2.
......
Require Export modures.cmra. Require Export algebra.cmra.
Require Import prelude.fin_maps. Require Import prelude.fin_maps.
Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A := Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
......
Require Export modures.cmra. Require Export algebra.cmra.
Require Import modures.cmra_big_op. Require Import algebra.cmra_big_op.
(** * Simple solver for validity and inclusion by reflection *) (** * Simple solver for validity and inclusion by reflection *)
Module ra_reflection. Section ra_reflection. Module ra_reflection. Section ra_reflection.
......
Require Export modures.base. Require Export algebra.base.
(** Unbundeled version *) (** Unbundeled version *)
Class Dist A := dist : nat relation A. Class Dist A := dist : nat relation A.
......
Require Export modures.cofe. Require Export algebra.cofe.
Record solution (F : cofeT cofeT cofeT) := Solution { Record solution (F : cofeT cofeT cofeT) := Solution {
solution_car :> cofeT; solution_car :> cofeT;
......
Require Export modures.cmra. Require Export algebra.cmra.
(** From disjoint pcm *) (** From disjoint pcm *)
Record validity {A} (P : A Prop) : Type := Validity { Record validity {A} (P : A Prop) : Type := Validity {
......
Require Export modures.cmra. Require Export algebra.cmra.
Local Arguments validN _ _ _ !_ /. Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /. Local Arguments valid _ _ !_ /.
......
Require Export modures.cmra prelude.gmap modures.option. Require Export algebra.cmra prelude.gmap algebra.option.
Section cofe. Section cofe.
Context `{Countable K} {A : cofeT}. Context `{Countable K} {A : cofeT}.
......
Require Export modures.cmra. Require Export algebra.cmra.
(* COFE *) (* COFE *)
Section cofe. Section cofe.
......
Require Export modures.cmra. Require Export algebra.cmra.
Require Import prelude.sets modures.dra. Require Import prelude.sets algebra.dra.
Local Arguments valid _ _ !_ /. Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /. Local Arguments op _ _ !_ !_ /.
Local Arguments unit _ _ !_ /. Local Arguments unit _ _ !_ /.
......
Require Export Autosubst.Autosubst. Require Export Autosubst.Autosubst.
Require Export iris.language. Require Export program_logic.language.
Require Import prelude.gmap. Require Import prelude.gmap.
Module heap_lang. Module heap_lang.
......
Require Import prelude.gmap iris.lifting. Require Import prelude.gmap program_logic.lifting.
Require Export iris.weakestpre heap_lang.heap_lang_tactics. Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
Import uPred. Import uPred.
Import heap_lang. Import heap_lang.
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2). Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
......
(** This file is essentially a bunch of testcases. *) (** This file is essentially a bunch of testcases. *)
Require Import modures.logic. Require Import logic.upred.
Require Import heap_lang.lifting heap_lang.sugar. Require Import heap_lang.lifting heap_lang.sugar.
Import heap_lang. Import heap_lang.
Import uPred. Import uPred.
......
Require Export modures.cmra. Require Export algebra.cmra.
Local Hint Extern 1 (_ _) => etransitivity; [eassumption|]. Local Hint Extern 1 (_ _) => etransitivity; [eassumption|].
Local Hint Extern 1 (_ _) => etransitivity; [|eassumption]. Local Hint Extern 1 (_ _) => etransitivity; [|eassumption].
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
......
Require Export iris.hoare. Require Export program_logic.hoare.
Require Import iris.wsat. Require Import program_logic.wsat.
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of. Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
Local Hint Extern 10 ({_} _) => Local Hint Extern 10 ({_} _) =>
......
Require Export modures.cmra. Require Export algebra.cmra.
Structure iFunctor := IFunctor { Structure iFunctor := IFunctor {
ifunctor_car :> cofeT cmraT; ifunctor_car :> cofeT cmraT;
......
Require Export iris.weakestpre iris.viewshifts. Require Export program_logic.weakestpre program_logic.viewshifts.
Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ) Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
(e : expr Λ) (Q : val Λ iProp Λ Σ) : iProp Λ Σ := (e : expr Λ) (Q : val Λ iProp Λ Σ) : iProp Λ Σ :=
......
Require Export iris.hoare iris.lifting. Require Export program_logic.hoare program_logic.lifting.
Local Notation "{{ P } } ef ?@ E {{ Q } }" := Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
(default True%I ef (λ e, ht E P e Q)) (default True%I ef (λ e, ht E P e Q))
......
Require Export modures.cofe. Require Export algebra.cofe.
Structure language := Language { Structure language := Language {
expr : Type; expr : Type;
......
Require Export iris.weakestpre. Require Export program_logic.weakestpre.
Require Import iris.wsat. Require Import program_logic.wsat.
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of. Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
Local Hint Extern 10 ({_} _) => Local Hint Extern 10 ({_} _) =>
......
Require Export modures.logic iris.resources. Require Export logic.upred program_logic.resources.
Require Import modures.cofe_solver. Require Import algebra.cofe_solver.
Module iProp. Module iProp.
Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT := Definition F (Λ : language) (Σ : iFunctor) (A B : cofeT) : cofeT :=
......
Require Export modures.base prelude.countable prelude.co_pset. Require Export algebra.base prelude.countable prelude.co_pset.
Definition namespace := list positive. Definition namespace := list positive.
Definition nnil : namespace := nil. Definition nnil : namespace := nil.
......
Require Export iris.model. Require Export program_logic.model.
Definition inv {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ := Definition inv {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
uPred_own (Res {[ i to_agree (Later (iProp_unfold P)) ]} ). uPred_own (Res {[ i to_agree (Later (iProp_unfold P)) ]} ).
......
Require Export iris.ownership prelude.co_pset. Require Export program_logic.ownership prelude.co_pset.
Require Import iris.wsat. Require Import program_logic.wsat.
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of. Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
Local Hint Extern 100 (_ _) => solve_elem_of. Local Hint Extern 100 (_ _) => solve_elem_of.
......
Require Export modures.fin_maps modures.agree modures.excl. Require Export algebra.fin_maps algebra.agree algebra.excl.
Require Export iris.language iris.functor. Require Export program_logic.language program_logic.functor.
Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res { Record res (Λ : language) (Σ : iFunctor) (A : cofeT) := Res {
wld : mapRA positive (agreeRA A); wld : mapRA positive (agreeRA A);
......
(** This file tests a bunch of things. *) (** This file tests a bunch of things. *)
Require Import iris.model. Require Import program_logic.model.
Module ModelTest. (* Make sure we got the notations right. *) Module ModelTest. (* Make sure we got the notations right. *)
Definition iResTest {Λ : language} {Σ : iFunctor} Definition iResTest {Λ : language} {Σ : iFunctor}
......
Require Export iris.pviewshifts. Require Export program_logic.pviewshifts.
Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ := Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
( (P pvs E1 E2 Q))%I. ( (P pvs E1 E2 Q))%I.
......
Require Export iris.pviewshifts. Require Export program_logic.pviewshifts.
Require Import iris.wsat. Require Import program_logic.wsat.
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of. Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
Local Hint Extern 100 (_ _) => solve_elem_of. Local Hint Extern 100 (_ _) => solve_elem_of.
......
Require Export iris.model prelude.co_pset. Require Export program_logic.model prelude.co_pset.
Require Export modures.cmra_big_op modures.cmra_tactics. Require Export algebra.cmra_big_op algebra.cmra_tactics.
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
Local Hint Extern 10 ({_} _) => solve_validN. Local Hint Extern 10 ({_} _) => solve_validN.
Local Hint Extern 1 ({_} (gst _)) => apply gst_validN. Local Hint Extern 1 ({_} (gst _)) => apply gst_validN.
......
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