Ltac2 Automatic compilation to OCaml

[JasonGross]

On low-level code using Constr.Unsafe.kind, line-by-line translating ltac2 to OCaml can bring a speedup of 50x in some cases. It'd be nice to have this be automatic.

[ppedrot]

FTR, this is part of my long-term todo list.

[JasonGross]

Here is another test-case, where I have a(n I think) reasonably hand-written version of something like context that is 800x-1600x slower in Ltac2 than the built-in version:

Fixpoint fact (n : nat) :=
  match n with
  | O => 1
  | S n' => fact n' * S n'
  end.
Require Import Ltac2.Ltac2.
Require Import Ltac2.Constr.
Require Import Ltac2.Control.
Require Import Ltac2.Notations.
Ltac2 rec fold_right f init ls :=
  match ls with
  | [] => init
  | x :: xs => f x (fold_right f init xs)
  end.
Ltac2 rec app ls1 ls2 :=
  match ls1 with
  | [] => ls2
  | x :: xs => x :: app xs ls2
  end.
Ltac2 rec rev ls :=
  match ls with
  | [] => []
  | x :: xs => app (rev xs) [x]
  end.
Ltac2 rec fold_left f ls init :=
  match ls with
  | [] => init
  | x :: xs => fold_left f xs (f init x)
  end.
Ltac2 rec map f ls :=
  match ls with
  | [] => []
  | x :: xs => f x :: map f xs
  end.
Ltac2 rec concat_list sep ls :=
  match ls with
  | [] => Message.of_string ""
  | x :: xs
    => match xs with
       | [] => x
       | _ => Message.concat x (Message.concat sep (concat_list sep xs))
       end
  end.
Ltac2 rec iter tac ls :=
  match ls with
  | [] => ()
  | x :: xs => tac x; iter tac xs
  end.
Ltac2 rec seq' start endv :=
  match Int.equal start endv with
  | true => []
  | false => start :: seq' (Int.add start 1) endv
  end.
Ltac2 rec seq start len := seq' start (Int.add start len).
Ltac2 rec array_iter f ls :=
  iter (fun i => f (Array.get ls i)) (seq 0 (Array.length ls)).
Ltac2 rec find (id : ident) (term : constr) :=
  match Constr.Unsafe.kind term with
  | Constr.Unsafe.Rel _ => ()
  | Constr.Unsafe.Var id' => () (* ... *)
  | Constr.Unsafe.Meta _ => ()
  | Constr.Unsafe.Evar _ _ => ()
  | Constr.Unsafe.Sort _ => ()
  | Constr.Unsafe.Cast c cst ty => find id c; find id ty
  | Constr.Unsafe.Prod id' a b => () (* ... *); find id a; find id b
  | Constr.Unsafe.Lambda id' a b => () (* ... *); find id a; find id b
  | Constr.Unsafe.LetIn id' a b c => () (* ... *); find id a; find id b; find id c
  | Constr.Unsafe.App f xs => find id f; array_iter (find id) xs
  | Constr.Unsafe.Constant _ _ => ()
  | Constr.Unsafe.Ind _ _ => ()
  | Constr.Unsafe.Constructor _ _ => ()
  | Constr.Unsafe.Case _ c r body => find id c; find id r; array_iter (find id) body
  | Constr.Unsafe.Fix _ _ _ ts vs => array_iter (find id) ts; array_iter (find id) vs
  | Constr.Unsafe.CoFix _ _ ts vs => array_iter (find id) ts; array_iter (find id) vs
  | Constr.Unsafe.Proj _ v => find id v
  end.
Goal True.
  ltac1:(pose proof True as x;
         let n := constr:(8) in
         let v := (eval cbv in (fact n)) in
         let c := constr:(eq_refl : fact n = v) in
         do 5 pose c).
  Time let v := Control.hyps () in
       let i := @x in
       iter (fun (h, body, ty) => find i ty; match body with Some b => find i b | None => () end) v.
  (* Finished transaction in 17.031 secs (16.539u,0.008s) (successful) *)
  Time ltac1:(try let x := match goal with x : Prop |- _ => x end in match goal with H : context[x] |- _ => idtac end). (* Finished transaction in 0.229 secs (0.156u,0.s) (successful) *)

[SkySkimmer]

Updated for recent Coq (simplified find that still shows slowness)

Fixpoint fact (n : nat) :=
  match n with
  | O => 1
  | S n' => fact n' * S n'
  end.
Require Import Ltac2.Ltac2.
Require Import Ltac2.Constr.
Require Import Ltac2.Control.
Require Import Ltac2.Notations.

Ltac2 rec iter tac ls :=
  match ls with
  | [] => ()
  | x :: xs => tac x; iter tac xs
  end.

Ltac2 rec find (id : ident) (term : constr) :=
  match Constr.Unsafe.kind term with
  | Constr.Unsafe.Cast c cst ty => find id c; find id ty
  | Constr.Unsafe.App f xs => find id f; Array.iter (find id) xs
  | _ => ()
  end.

Goal True.
  ltac1:(pose proof True as x;
         let n := constr:(7) in
         let v := (eval cbv in (fact n)) in
         let c := constr:(eq_refl : fact n = v) in
         do 5 pose c).
  Time let v := Control.hyps () in
       let i := @x in
       iter (fun (h, body, ty) => find i ty; match body with Some b => find i b | None => () end) v.
  (* Finished transaction in 0.75 secs *)

  Time ltac1:(try let x := match goal with x : Prop |- _ => x end in match goal with H : context[x] |- _ => idtac end).
  (* Finished transaction in 0.005 secs *)

[SkySkimmer]

Even just writing Array.iter in ocaml gives 2.5x perf

[SkySkimmer]

Comparison with ltac1 iteration without using context:

Fixpoint fact (n : nat) :=
  match n with
  | O => 1
  | S n' => fact n' * S n'
  end.
Require Import Ltac2.Ltac2.
Require Import Ltac2.Constr.
Require Import Ltac2.Control.
Require Import Ltac2.Notations.

Ltac2 rec iter tac ls :=
  match ls with
  | [] => ()
  | x :: xs => tac x; iter tac xs
  end.

Ltac2 rec find  (term : constr) :=
  match Constr.Unsafe.kind term with
  | Constr.Unsafe.Cast c cst ty => find c
  | Constr.Unsafe.App f xs => find f; Array.iter find xs
  | _ => ()
  end.

Ltac finder c :=
  match c with
  | ?h ?v => finder h; finder v
  | _ => idtac
  end.

Ltac2 finder (c:constr) := ltac1:(v |- finder v) (Ltac1.of_constr c).

Goal True.
  ltac1:(pose proof True as x;
         let n := constr:(7) in
         let v := (eval cbv in (fact n)) in
         let c := constr:(eq_refl : fact n = v) in
         do 5 pose c).

  Time let v := Control.hyps () in
       iter (fun (h, body, ty) => find ty; match body with Some b => find b | None => () end) v.
  (* Finished transaction in 0.15 secs *)

  Time let v := Control.hyps () in
       iter (fun (h, body, ty) => finder ty; match body with Some b => finder b | None => () end) v.
  (* Finished transaction in 0.38 secs *)

  Time ltac1:(repeat match goal with H : ?t |- _ => finder t; fail end).
  (* 0.38s *)

  Time ltac1:(try let x := match goal with x : Prop |- _ => x end in match goal with H : context[x] |- _ => idtac end).
  (* Finished transaction in 0.005 secs *)

[SkySkimmer]

It should be possible to automatically translate the find in the previous post to something like

(* available definitions and opens as if this is put at the end of tac2core.ml *)

let app_prim name l = Tac2ffi.apply (Tac2env.interp_primitive (pname name)) l

let rec array_iter_aux f a pos len =
  app_prim "int_equal" [len; ValInt 0] >>= function
  | ValInt 0 -> return v_unit
  | ValInt _ ->
    app_prim "array_get" [a; pos] >>= fun v ->
    Tac2ffi.apply (to_closure f) [v] >>= fun _ ->
    app_prim "int_add" [pos; (ValInt 1)] >>= fun pos' ->
    app_prim "int_sub" [len; (ValInt 1)] >>= fun len' ->
    array_iter_aux f a pos' len'
  | _ -> assert false

let array_iter f a =
  app_prim "array_length" [a] >>= fun len ->
  array_iter_aux f a (ValInt 0) len

let rec constr_iter term =
  app_prim "constr_kind" [term] >>= function
  | ValBlk (5, [|c;_;ty|]) -> constr_iter c
  | ValBlk (9, [|f; xs|]) ->
    constr_iter f >>= fun _ ->
    array_iter (of_closure (mk_closure arity_one constr_iter)) xs
  | _ -> return v_unit

let () = define1 "test_constr_iter" valexpr constr_iter

Then

Ltac2 @ external find' : constr -> unit := "ltac2" "test_constr_iter".

  Time let v := Control.hyps () in
       iter (fun (h, body, ty) => find' ty; match body with Some b => find' b | None => () end) v.
  (* 0.025s *)

about 6x improvement (with another 5x left to reach match goal 0.005s speed)

If we understand int primitives enough to optimize to

let rec array_iter_aux f a pos len =
  if len = 0 then return v_unit
  else
    app_prim "array_get" [a; ValInt pos] >>= fun v ->
    Tac2ffi.apply (to_closure f) [v] >>= fun _ ->
    array_iter_aux f a (pos+1) (len-1)

let array_iter f a =
  app_prim "array_length" [a] >>= fun len ->
  array_iter_aux f a 0 (to_int len)

we get 0.015s, and if we also understand arrays enough to do

let rec array_iter_aux f a pos len =
  if len = 0 then return v_unit
  else
    let _, ar = to_block a in
    if pos < 0 || pos >= Array.length ar then throw err_outofbounds
    else
      let v = ar.(pos) in
      Tac2ffi.apply (to_closure f) [v] >>= fun _ ->
      array_iter_aux f a (pos+1) (len-1)

let array_iter f a =
  let len = Array.length (snd (to_block a)) in
  array_iter_aux f a 0 len

we get about 0.01s

To go farther than that we need to understand Constr.Unsafe.kind, let's worry about that once we've got the other ideas done.

[SkySkimmer]

Development has moved to https://github.com/SkySkimmer/coq-ltac2-compiler