gds (gds) wrote,
gds
gds

coq + inlining + "merge right"

Некоторые люди прочитали статью http://alaska-kamtchatka.blogspot.com/2012/08/merge-right.html , где была показана весьма общая функция для слияния/пересечения/разницы списков.
А господин ygrek в камлочятике прилюдно мучил MetaOCaml для инлайнинга функций-аргументов merge. Я не мог на это смотреть спокойно. Однако и сразу разобраться не смог, так как не знал многого, но вполне так узнал.
Чтобы было хоть сколько-нибудь интересно читать, рекомендую прочитать сначала исходную статью.
Потому что сейчас будет простыня.

Require Import List.
Require Import Wf.
Require Import Wf_nat.
Require Import Omega.

Definition nat_lt := lt.

Inductive cmp_res :=
  | Lt
  | Eq
  | Gt
.

Definition merge : forall
  {A : Type}
  (cmp : A -> A -> cmp_res)
  (ln rn : list A -> list A)
  (lt eq gt : A -> list A -> list A)
  (l r : list A),
  list A.
refine
  (fun {A} cmp ln rn lt eq gt l r =>
     (fix go l r (H : Acc nat_lt (length l + length r)) {struct H} :=
        match H with
        | Acc_intro H1 =>
            match l as l1, r as r1
              return l = l1 -> r = r1 -> list A
            with
            | nil, _ => fun _Leq _Req => ln r
            | _, nil => fun _Leq _Req => rn l
            | cons x xs, cons y ys =>
                fun Leq Req =>
                match cmp x y with
                | Lt => lt x (go       xs (y :: ys) (H1 _ _))
                | Eq => eq x (go       xs       ys  (H1 _ _))
                | Gt => gt y (go (x :: xs)      ys  (H1 _ _))
                end
            end
            (eq_refl l)
            (eq_refl r)
        end
     )
     l r
     (Acc_intro _ _)
  );
intros;
try rewrite Leq;
try rewrite Req;
simpl;
unfold nat_lt;
try omega;
try apply lt_wf.
Defined.


Definition self {A}         (xs : list A) : list A :=     xs .
Definition null {A}         (_  : list A) : list A :=     nil.
Definition cons {A} (x : A) (xs : list A) : list A := x :: xs.
Definition tail {A} (_ : A) (xs : list A) : list A :=      xs.

Extraction Inline merge self null cons tail.

Definition union {A} cmp (l : list A) r :=
  merge cmp self self  cons cons cons l r.
Definition inter {A} cmp (l : list A) r :=
  merge cmp null null  tail cons tail l r.
Definition diff {A} cmp (l : list A) r :=
  merge cmp null self  cons tail tail l r.

Extraction Inline union inter diff.

Axiom int' : Type.
Extract Constant int' => "int".
Definition int := int'.

Axiom cmp_int : int -> int -> cmp_res.
Extract Inlined Constant cmp_int =>
  "(fun (a : int) b -> if a < b then Lt else if a = b then Eq else Gt)".

Definition union_int := @union int cmp_int.

Require Import ExtrOcamlBasic.

Extraction union_int.

-----

(** val union_int : int list -> int list -> int list **)

let rec union_int l0 r0 =
  match l0 with
  | [] -> r0
  | x :: xs ->
    (match r0 with
     | [] -> l0
     | y :: ys ->
       (match (fun (a : int) b -> if a < b then Lt else if a = b then Eq else Gt)
                x y with
        | Lt -> x :: (union_int xs (y :: ys))
        | Eq -> x :: (union_int xs ys)
        | Gt -> y :: (union_int (x :: xs) ys)))


Вроде ЗБС.
Можно было бы сравнение не инлайнить, но избавиться от вызова функции (будь то "(fun (a : int) b -> ...)", будь то Pervasives.compare) не получается сходу.
Мне Coq нужен не только для зависимых типов и доказательств кода, но и для инлайнинга. Я -- практичная скотина, да!
Если будут вопросы -- поясню. Потому что всё сразу пояснять -- руки устанут.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 4 comments