Use elpi.derive instead of "Scheme Equality" #1052

eponier · 2025-02-14T10:23:48Z

elpi.derive is much faster on inductives with many constructors. This is particularly interesting for type x86_op which has more than 100 constructors.

eponier · 2025-02-14T10:28:07Z

There are currently a few caveats:

it does not work with coq.8.19 and coq-elpi 2.2.3 (it works for previous and next versions, so looks like a bug upstream); EDIT: the culprit seems to be coq-elpi.2.2.x
Scheme Equality has a specific impact on injection (there is a note about it in the Coq doc (I cannot put a link directly to the note, it is a bit below where the link points to)). We may want to keep Scheme Equality for wsize. to reduce the number of changes in this PR.
there is an option module to put all what is generated by derive inside a module. I used it for stype because there was a name clash with is_sbool. But it has impact on the extracted code, so maybe this was not the right choice (I think is_sbool is not even used, so maybe the right thing to do is just to remove it).
we have new warnings in the extracted OCaml code because derive generates recursive functions that are not actually recursive. There are two problems here:
- derive should not generate fake recursive functions, but this should be fixed upstream
- do we really want to extract these functions? (after a bit of thought, maybe they are used by eqb functions that we need, so we have no choice)
importing derive.std hides Datatypes.is_true; nothing problematic here, it is just painful

eponier · 2025-02-14T10:36:17Z

proofs/_CoqProject

@@ -15,6 +15,7 @@
 -arg "-w -deprecated-since-mathcomp-2.3.0"
 -arg "-w -deprecated-from-Coq"
 -arg "-w -deprecated-dirpath-Coq"
+-arg "-async-proofs off"


Oops, should not be there.

eponier · 2025-02-14T10:38:32Z

proofs/compiler/riscv_decl.v

-   ; call_xreg_ret  := [::]
-   ; call_reg_ret_uniq := erefl true;
-  |}.
+Definition riscv_linux_call_conv : calling_convention :=


Unrelated fix. The comment was not true anymore.

eponier · 2025-02-14T10:39:40Z

proofs/compiler/stack_alloc.v

@@ -105,19 +107,15 @@ End CmpR.
 Module Mr := Mmake CmpR.

 (* ------------------------------------------------------------------ *)
+#[only(eqbOK)] derive Z.


We may want to move that elsewhere. In utils?

eponier · 2025-02-14T10:40:16Z

proofs/compiler/x86_lowering_proof.v

@@ -176,6 +176,11 @@ Section PROOF.
    end.
  Qed.

+  Lemma cons_inj {A} {x1 x2 : A} (s1 s2 : seq A) :


We may want to move this to utils.

eponier · 2025-02-14T10:41:31Z

proofs/lang/type.v

@@ -147,7 +143,7 @@ Module CEDecStype.
    | sword w1 =>
      match t2 as t0 return {sword w1 = t0} + {True} with
      | sword w2 =>
-        match wsize_eq_dec w1 w2 with
+        match Bool.reflect_dec _ _ (wsize_eqb_OK w1 w2) with


In the end, I reintroduced wsize_eq_dec so this change is not needed.

eponier · 2025-02-14T10:41:39Z

proofs/lang/type.v

@@ -169,7 +167,7 @@ Module CEDecStype.
    + case: pos_dec (@pos_dec_r n n' I) => [Heq _ | [] neq ] //=.
      move => _; apply/eqP => -[].
      by move/eqP: (neq erefl).
-    case: wsize_eq_dec => // eqw.
+    case: Bool.reflect_dec => // eqw.


eponier · 2025-02-14T10:42:29Z

proofs/compiler/arm_lowering_proof.v

-    move=> [?]; subst v.
+    case: ves => [// | ? []]; last by t_xrbindP.
+    apply: rbindP => v /=.
+    apply: rbindP => _ -> [->] /ok_inj /(f_equal (head (Vbool true))) /= /Vword_inj [?]; subst ws''.


TODO: use cons_inv instead

eponier · 2025-02-14T10:42:35Z

proofs/compiler/arm_lowering_proof.v

-  move=> [?]; subst v.
+  case: ves => [// | ? []]; last by t_xrbindP.
+  apply: rbindP => v /=.
+  apply: rbindP => _ -> [->] /ok_inj /(f_equal (head (Vbool true))) /= /Vword_inj [?]; subst ws''.


eponier · 2025-02-18T14:08:40Z

Note to self: it seems we can remove eq_axiom_of_scheme.

Use elpi.derive instead of "Scheme Equality"

b790e97

elpi.derive is much faster on inductives with many constructors. This is particularly interesting for type x86_op which has more than 100 constructors.

eponier commented Feb 14, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use elpi.derive instead of "Scheme Equality" #1052

Use elpi.derive instead of "Scheme Equality" #1052

eponier commented Feb 14, 2025

eponier commented Feb 14, 2025 •

edited

Loading

eponier Feb 14, 2025

eponier Feb 14, 2025

eponier Feb 14, 2025

eponier Feb 14, 2025

eponier Feb 14, 2025

eponier Feb 14, 2025

eponier Feb 14, 2025

eponier Feb 14, 2025

eponier commented Feb 18, 2025

Use elpi.derive instead of "Scheme Equality" #1052

Are you sure you want to change the base?

Use elpi.derive instead of "Scheme Equality" #1052

Conversation

eponier commented Feb 14, 2025

eponier commented Feb 14, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eponier commented Feb 18, 2025

eponier commented Feb 14, 2025 •

edited

Loading