From 3ecc3dc6cebf87f87091d2aa35b06224c41a824e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 31 Jan 2015 15:07:04 +0100
Subject: [PATCH] make Coq *much* faster by introducing names for some
instances
---
configure | 2 ++
iris.v | 16 ++++++++++++----
world_prop.v | 12 ++++++++++++
3 files changed, 26 insertions(+), 4 deletions(-)
create mode 100755 configure
diff --git a/configure b/configure
new file mode 100755
index 000000000..244a33b85
--- /dev/null
+++ b/configure
@@ -0,0 +1,2 @@
+#!/bin/sh
+coq_makefile lib/ModuRes -R lib/ModuRes ModuRes *.v -o Makefile
diff --git a/iris.v b/iris.v
index ea1e11eb8..125f48707 100644
--- a/iris.v
+++ b/iris.v
@@ -25,7 +25,7 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
Instance Props_BI : ComplBI Props | 0 := _.
Instance Props_Later : Later Props | 0 := _.
-
+
(* Benchmark: How large is thid type? *)
Section Benchmark.
Local Open Scope mask_scope.
@@ -33,11 +33,12 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
Local Open Scope bi_scope.
Local Open Scope lang_scope.
- Local Instance expr_type : Setoid expr := discreteType.
- Local Instance expr_metr : metric expr := discreteMetric.
- Local Instance expr_cmetr : cmetric expr := discreteCMetric.
+ Local Instance _bench_expr_type : Setoid expr := discreteType.
+ Local Instance _bench_expr_metr : metric expr := discreteMetric.
+ Local Instance _bench_cmetr : cmetric expr := discreteCMetric.
Set Printing All.
+ Check (expr -n> (value -n> Props) -n> Props).
Check ((expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props).
End Benchmark.
@@ -403,6 +404,7 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
End Erasure.
+ Check erasure.
Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity).
@@ -484,6 +486,8 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
End ViewShifts.
+ Check vs.
+
Section ViewShiftProps.
Local Open Scope mask_scope.
Local Open Scope pcm_scope.
@@ -996,6 +1000,8 @@ Qed.
End HoareTriples.
+ Check wp.
+
Section Soundness.
Local Open Scope mask_scope.
Local Open Scope pcm_scope.
@@ -1211,6 +1217,8 @@ Qed.
End Soundness.
+ Check soundness.
+
Section HoareTripleProperties.
Local Open Scope mask_scope.
Local Open Scope pcm_scope.
diff --git a/world_prop.v b/world_prop.v
index 103ead16f..1466e8e12 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -80,8 +80,20 @@ Module WorldProp (Res : PCM_T).
Lemma isoR T : ı (ı' T) == T.
Proof. apply (UF_id T). Qed.
+ Set Printing All.
+ (* PreProp has an equivalence and a complete metric. It also has a preorder that fits to everything else. *)
+ Instance PProp_ty : Setoid PreProp := _.
+ Instance PProp_m : metric PreProp := _.
+ Instance PProp_cm : cmetric PreProp := _.
Instance PProp_preo : preoType PreProp := disc_preo PreProp.
Instance PProp_pcm : pcmType PreProp := disc_pcm PreProp.
Instance PProp_ext : extensible PreProp := disc_ext PreProp.
+ (* Give names to the things for Props, so the terms can get shorter. *)
+ 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 WorldProp.
--
GitLab