1 files changed, 113 insertions, 0 deletions
diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v
new file mode 100644
index 00000000..eb01133e
--- /dev/null
+++ b/test-suite/complexity/injection.v
@@ -0,0 +1,113 @@
+(* This example, submitted by A. Appel, checks the efficiency of
+   injection (see bug #1173) *)
+(* Expected time < 1.50s *)
+
+Set Implicit Arguments.
+
+Record joinable (t: Type) : Type := Joinable {
+   is_empty: t -> Prop;
+   join: t -> t -> t -> Prop;
+   join_com: forall a b c, join a b c -> join b a c;
+   join_empty: forall e a b, is_empty e -> join e a b -> a=b;
+   exists_empty: forall a, exists e, is_empty e /\ join e a a;
+   join_empty2: forall a b c, join a b c ->  is_empty c -> is_empty a;
+   join_empty3: forall e a, join e a a -> is_empty e;
+   join_assoc: forall a b c d e, join a b d -> join d c e ->
+                    exists f, join b c f /\ join a f e;
+   join_eq: forall x y z z', join x y z -> join x y z' -> z = z';
+   cancellation: forall a1 a2 b c, join a1 b c -> join a2 b c -> a1=a2
+}.
+
+Record joinmap (key: Type) (t: Type) (j : joinable t) : Type
+ := Joinmap {
+    jm_t : Type;
+    jm_j : joinable jm_t;
+    lookup: jm_t -> key -> t;
+    prim : forall (f: key -> t) (e: t),
+                  (forall k, j.(join) e (f k) (f k)) ->
+                  jm_t;
+    join_rule: forall s1 s2 s,
+                jm_j.(join) s1 s2 s <->
+                forall x, j.(join) (lookup s1 x) (lookup s2 x) (lookup s x);
+    empty_rule: forall e x, jm_j.(is_empty) e -> j.(is_empty) (lookup e x);
+    prim_rule: forall f e pf k, lookup (prim f e pf) k = f k;
+    ext: forall s1 s2,
+        (forall x, lookup s1 x = lookup s2 x) <-> s1 = s2;
+    can_join: forall s1 s2,
+            (forall x, exists v,
+                j.(join) (lookup s1 x) (lookup s2 x) v) ->
+            exists s3, jm_j.(join) s1 s2 s3;
+    can_split: forall s1 s3,
+            (forall x, exists v,
+                j.(join) (lookup s1 x) v (lookup s3 x)) ->
+            exists s2, jm_j.(join) s1 s2 s3
+}.
+
+Parameter mkJoinmap :   forall (key: Type) (t: Type) (j: joinable t), 
+joinmap key j.
+
+Parameter ADMIT: forall p: Prop, p.
+Implicit Arguments ADMIT [p].    
+
+Module Share.
+Parameter jb : joinable bool.
+Definition jm: joinmap nat jb := mkJoinmap nat jb.
+Definition t := jm.(jm_t).
+Definition j := jm.(jm_j).
+Parameter nonempty: t -> Prop.
+End Share.
+
+Section Own.
+
+Variable inv : Type.
+
+Inductive own : Type :=
+  | NO
+  | VAL' : forall sh, Share.nonempty sh -> own
+  | LK : forall sh, Share.nonempty sh -> Share.t -> inv -> own
+  | CT : forall sh, Share.nonempty sh -> own
+  | FUN: forall sh, Share.nonempty sh -> inv -> own.
+
+Definition own_join (a b c: own) : Prop :=
+ match a , b , c with
+  | NO , _ , _ =>  b=c
+  | _ , NO , _ =>  a=c
+  | VAL' sa _ , VAL' sb _, VAL' sc _ => Share.j.(join) sa sb sc
+  | LK sa pa ha fa, LK sb pb hb fb, LK sc pc hc fc =>
+      Share.j.(join) sa sb sc /\
+      Share.j.(join) ha hb hc /\
+      fa=fc /\
+      fb=fc
+  | CT sa pa , CT sb pb, CT sc pc => Share.j.(join) sa sb sc
+  | FUN sa pa fa, FUN sb pb fb, FUN sc pc fc =>
+        Share.j.(join) sa sb sc /\ fa=fc /\ fb=fc
+  | _ , _ , _ => False
+ end.
+
+Definition own_is_empty (a: own) := a=NO.
+
+Definition jown : joinable own :=
+  Joinable own_is_empty own_join
+     ADMIT ADMIT  ADMIT  ADMIT  ADMIT  ADMIT  ADMIT  ADMIT .
+End Own.
+  
+Fixpoint sinv (n: nat) : Type :=
+  match n with
+   | O => unit
+   | S n => prodT (sinv n) (own (sinv n) -> unit -> Prop)
+ end.
+
+Parameter address: Set.
+
+Definition jm (n: nat) := mkJoinmap address (jown (sinv n)).
+
+Definition worldfun (n: nat) := (jm n).(jm_t).
+
+Inductive world : Type :=
+  mk_world: forall n, worldfun n -> world.
+
+Lemma test: forall n1 w1 n2 w2, mk_world n1 w1 = mk_world n2 w2 ->
+         n1 = n2.
+Proof.
+intros.
+Time injection H.