Commit 2ad23105 authored by Ralf Jung's avatar Ralf Jung

get rid of the "inner" module, use an opaque WorldProp instead

parent 5b22c4cf
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
# #
# This Makefile was generated by the command line : # This Makefile was generated by the command line :
# coq_makefile lib/ModuRes -R lib/ModuRes ModuRes core_lang.v iris.v iris_core.v lang.v masks.v world_prop.v world_prop_sig.v -o Makefile # coq_makefile lib/ModuRes -R lib/ModuRes ModuRes core_lang.v iris.v iris_core.v lang.v masks.v world_prop.v -o Makefile
# #
.DEFAULT_GOAL := all .DEFAULT_GOAL := all
...@@ -85,8 +85,7 @@ VFILES:=core_lang.v\ ...@@ -85,8 +85,7 @@ VFILES:=core_lang.v\
iris_core.v\ iris_core.v\
lang.v\ lang.v\
masks.v\ masks.v\
world_prop.v\ world_prop.v
world_prop_sig.v
-include $(addsuffix .d,$(VFILES)) -include $(addsuffix .d,$(VFILES))
.SECONDARY: $(addsuffix .d,$(VFILES)) .SECONDARY: $(addsuffix .d,$(VFILES))
......
Require Import world_prop_sig core_lang lang masks. Require Import world_prop core_lang lang masks.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap. Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T. Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T.
...@@ -10,10 +10,9 @@ Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T. ...@@ -10,10 +10,9 @@ Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T.
End IrisRes. End IrisRes.
Module Iris (RL : PCM_T) (C : CORE_LANG). Module Iris (RL : PCM_T) (C : CORE_LANG).
Module Import R := IrisRes RL C.
Module IrisInner (WP : WORLD_PROP R).
Module Import L := Lang C. Module Import L := Lang C.
Import WP. Module Import R := IrisRes RL C.
Module Import WP := WorldProp R.
Delimit Scope iris_scope with iris. Delimit Scope iris_scope with iris.
Local Open Scope iris_scope. Local Open Scope iris_scope.
...@@ -409,9 +408,6 @@ Module IrisInner (WP : WORLD_PROP R). ...@@ -409,9 +408,6 @@ Module IrisInner (WP : WORLD_PROP R).
End Erasure. End Erasure.
Check erasure.
Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity). Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity).
End IrisInner.
End Iris. End Iris.
...@@ -3,8 +3,34 @@ ...@@ -3,8 +3,34 @@
Require Import ModuRes.PreoMet ModuRes.MetricRec ModuRes.CBUltInst. Require Import ModuRes.PreoMet ModuRes.MetricRec ModuRes.CBUltInst.
Require Import ModuRes.Finmap ModuRes.Constr. Require Import ModuRes.Finmap ModuRes.Constr.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI. Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI.
Require Import world_prop_sig.
(* This interface keeps some of the details of the solution opaque *)
Module Type WORLD_PROP (Res : PCM_T).
(* PreProp: The solution to the recursive equation. Equipped with a discrete order *)
Parameter PreProp : cmtyp.
Instance PProp_preo: preoType PreProp := disc_preo PreProp.
Instance PProp_pcm : pcmType PreProp := disc_pcm PreProp.
Instance PProp_ext : extensible PreProp := disc_ext PreProp.
(* Defines Worlds, Propositions *)
Definition Wld := nat -f> PreProp.
Definition Props := Wld -m> UPred Res.res.
(* Define all the things on Props, so they have names - this shortens the terms later *)
Instance Props_ty : Setoid Props := _.
Instance Props_m : metric Props := _.
Instance Props_cm : cmetric Props := _.
Instance Props_preo : preoType Props := _.
Instance Props_pcm : pcmType Props := _.
(* Establish the recursion isomorphism *)
Parameter ı : PreProp -t> halve (cmfromType Props).
Parameter ı' : halve (cmfromType Props) -t> PreProp.
Axiom iso : forall P, ı' (ı P) == P.
Axiom isoR: forall T, ı (ı' T) == T.
End WORLD_PROP.
(* Now we come to the actual implementation *)
Module WorldProp (Res : PCM_T) : WORLD_PROP Res. Module WorldProp (Res : PCM_T) : WORLD_PROP Res.
(** The construction is parametric in the monoid we choose *) (** The construction is parametric in the monoid we choose *)
......
(* For some reason, the order matters. We cannot import Constr last. *)
Require Import ModuRes.Finmap ModuRes.Constr ModuRes.MetricRec.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet.
Module Type WORLD_PROP (Res : PCM_T).
Import Res.
(* PreProp: The solution to the recursive equation. Equipped with a discrete order *)
Parameter PreProp : cmtyp.
Instance PProp_preo: preoType PreProp := disc_preo PreProp.
Instance PProp_pcm : pcmType PreProp := disc_pcm PreProp.
Instance PProp_ext : extensible PreProp := disc_ext PreProp.
(* Defines Worlds, Propositions *)
Definition Wld := nat -f> PreProp.
Definition Props := Wld -m> UPred res.
(* Establish the recursion isomorphism *)
Parameter ı : PreProp -t> halve (cmfromType Props).
Parameter ı' : halve (cmfromType Props) -t> PreProp.
Axiom iso : forall P, ı' (ı P) == P.
Axiom isoR: forall T, ı (ı' T) == T.
(* Define all the things on Props, so they have names - this shortens the terms later *)
Instance Props_ty : Setoid Props := _.
Instance Props_m : metric Props := _.
Instance Props_cm : cmetric Props := _.
Instance Props_preo : preoType Props := _.
Instance Props_pcm : pcmType Props := _.
End WORLD_PROP.
This diff is collapsed.
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