cstring should not need a compspecs argument

[andrew-appel]

cstring should not need a compspecs argument

[andrew-appel]

In case we want to do the latter (get change_compspecs to handle cstring), here's the code to do it:

Lemma change_compspecs_cstring: forall cs1 cs2: compspecs, (* put this in Floyd *)
    @cstring cs1 = @cstring cs2.
Proof.
intros.
extensionality sh s p.
unfold cstring.
f_equal.
set (u := map _ _). clearbody u.
set (n := Zlength _ + _). clearbody n.
unfold data_at.
unfold field_at.
f_equal.
f_equal.
unfold field_compatible.
f_equal; auto.
f_equal; auto.
f_equal; auto.
f_equal; auto.
unfold align_compatible.
destruct p; simpl; auto.
apply prop_ext; split; intro;
(apply align_compatible_rec_Tarray; intros j ?;
 apply align_compatible_rec_Tarray_inv with (i:=j) in H; auto;
 inv H; econstructor; eauto).
Qed.

Ltac forward.change_compspecs cs :=
  match goal with
  | |- context [ ?cs' ] =>
        match type of cs' with
        | compspecs =>
            try (constr_eq cs cs'; fail 1); 
            first [rewrite !(change_compspecs_cstring cs' cs)  (* new! *)
                  | change_compspecs' cs' cs];
            repeat change_compspecs' cs cs'
        end
  end.

[lennartberinger]

I believe this is a more general issue (and somewhat related to the fact that computational aspects of compspecs are built into floyd rather early), so it would be good if a solution with a minimal (or perhaps even better: arbitrary but not automatically instantiated) compspecs could be realized.