1

WITH construction is defined only for up to 8 variables. How can I use more than 8? Example:

Definition find_key_spec :=
  DECLARE _find_key
    WITH sh : share, m : ArrMapZ, start : Z, key : Z, i : nat,
         vbb : val, vkeys : val, vstart : val, vkey : val, vi : val
    PRE ...

=> 

Toplevel input, characters 176-177:
Syntax error: 'PRE' '[' expected after [constr:operconstr level 200]
(in [constr:binder_constr]).

I use: VST 1.5 (6834P at 2014-10-02), CompCert 2.4, Coq 8.4pl3(Jan'14) with OCaml 4.01.0.

Necto
  • 2,594
  • 1
  • 20
  • 45

2 Answers2

1

My solution: define notation for WITH with 10 variables:

Notation "'WITH'  x1 : t1 , x2 : t2 , x3 : t3 , x4 : t4 , x5 : t5 ,
                  x6 : t6 , x7 : t7 , x8 : t8 , x9 : t9 , x10 : t10
                  'PRE'  [ u , .. , v ] P 'POST' [ tz ] Q" :=
     (mk_funspec ((cons u%formals .. (cons v%formals nil) ..), tz)
                 (t1*t2*t3*t4*t5*t6*t7*t8*t9*t10)
           (fun x => match x with (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) =>
                                  P%logic end)
           (fun x => match x with (x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) =>
                                  Q%logic end))
            (at level 200, x1 at level 0, x2 at level 0, x3 at level 0,
                           x4 at level 0, x5 at level 0, x6 at level 0,
                           x7 at level 0, x8 at level 0, x9 at level 0,
                           x10 at level 0, P at level 100, Q at level 100).
Necto
  • 2,594
  • 1
  • 20
  • 45
  • That looks right. In the trunk version it's already been extended to 14 variables. (I don't recommend the trunk version for general use at the moment, though.) – Andrew Appel Jan 26 '15 at 13:28
1

An alternative is to introduce tuples in the WITH clause (e.g. WITH x12: (t1 * t2)%type), and to refer to their components in PRE and POST by projections (eg use fst x12 in place of x1 in PRE).

Lennart Beringer
  • 11
  • 1