Как использовать более 8 переменных в спецификации функции?

Question

WITH Конструкция определяется только для 8 переменных. Как я могу использовать более 8? Пример:

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]).

---

Я использую: VST 1.5 (6834P в 2014-10-02), CompCert 2.4, Coq 8.4pl3(январь 14) с OCaml 4.01.0.

Answer 1

Мое решение: определить обозначение для WITH с 10 переменными:

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).

Answer 2

Альтернативой является введение кортежей в предложении WITH (например, WITH x12: (t1 * t2)%type) и обращение к их компонентам в PRE и POST посредством проекций (например, используйте fst x12 вместо x1 в PRE).