Adapt to rocq-prover/rocq#20566 (Ltac2 rec doesn't produce a wrapper lambda) (#30)

Fix #29

Author: SkySkimmer

src/tac2compile.ml

@@ -259,6 +259,7 @@ type nontac_expr =
   | PrjV of nontac_expr * int (* non-mutable projection *)
   | Prim of ml_tactic_name
   | ValLetNoRec of (Name.t * nontac_expr) list * nontac_expr
+  | ValLetRec of (Id.t * (Name.t list * tac_expr)) list * nontac_expr
 
 (** evaluates to a valexpr tactic *)
 and tac_expr_head =
@@ -450,11 +451,11 @@ let rec is_nontac = function
   | GTacPrj (typ, sube, i) ->
     not (is_mutable_proj typ i) && is_nontac sube
 
-  | GTacLet (false, bnd, e) ->
+  | GTacLet (_, bnd, e) ->
     List.for_all (fun (_, e) -> is_nontac e) bnd
     && is_nontac e
 
-  | GTacApp _ | GTacLet (true, _, _) | GTacCse _
+  | GTacApp _ | GTacCse _
   | GTacSet _ | GTacWth _ | GTacFullMatch _
   | GTacExt _
     -> false
@@ -495,6 +496,12 @@ let rec nontac_expr env ((cnt, nonvals) as acc) e = match e with
         acc, Ref (LocalKn ("Tac2compiledPrim."^ml.mltac_tactic, info))
     end
 
+  | GTacLet (true, bnd, sube) when is_nontac e ->
+    let envbnd, lets = letrec_bnd env bnd in
+    let acc', sube = nontac_expr envbnd acc sube in
+    assert (acc' == acc);
+    acc, ValLetRec (lets, sube)
+
   | GTacLet (false, bnd, sube) when is_nontac e ->
     let envbnd, nas' = push_env push_user_names (List.map fst bnd) Valexpr env in
     let bnd = List.map2 (fun (_, e) na' ->
@@ -544,36 +551,16 @@ and tac_expr env e =
       let acc, args = List.fold_left_map (nontac_expr env) acc args in
       acc, App (h, args)
 
-    | GTacLet (true, lets, e) ->
-      let lets = lets |> List.filter_map (fun (na, e) ->
-          match e with
-          | GTacFun (bnd, e) ->
-            begin match na with
-            |  Anonymous ->
-              (* "let rec _ := ..." seems good for nothing, just a syntax curiosity
-                 lambda abstraction can't have effects so just drop it *)
-              None
-            | Name na ->
-              Some (na, (bnd, e))
-            end
-          | _ -> assert false)
-      in
-      let env, nas' =
-        List.fold_left_map (fun env (na, (bnd, _)) ->
-            push_env push_user_id na (Function {arity=List.length bnd}) env)
-          env lets
-      in
-      let lets = List.map2 (fun (_, (bnd, e)) na' ->
-          let env, bnd = push_env push_user_names bnd Valexpr env in
-          let e = tac_expr env e in
-          (na', (bnd, e)))
-          lets
-          nas'
-      in
-      let e = tac_expr env e in
-      acc, LetRec (lets, e)
+    | GTacLet (true, lets, sube) ->
+      if is_nontac e then
+        let acc', e = nontac_expr env acc e in
+        assert (acc == acc');
+        acc, Return e
+      else
+        let env, lets = letrec_bnd env lets in
+        let sube = tac_expr env sube in
+        acc, LetRec (lets, sube)
 
-    (* XXX detect when a let can be nontac_expr *)
     | GTacLet (false, bnd, sube) ->
       if is_nontac e then
         let acc', e = nontac_expr env acc e in
@@ -650,6 +637,34 @@ and tac_expr env e =
   { spilled_exprs = nonvals;
     head_expr = e; }
 
+and letrec_bnd env lets =
+  let lets = lets |> List.filter_map (fun (na, e) ->
+      match e with
+      | GTacFun (bnd, e) ->
+        begin match na with
+        |  Anonymous ->
+          (* "let rec _ := ..." seems good for nothing, just a syntax curiosity
+             lambda abstraction can't have effects so just drop it *)
+          None
+        | Name na ->
+          Some (na, (bnd, e))
+        end
+      | _ -> assert false)
+  in
+  let env, nas' =
+    List.fold_left_map (fun env (na, (bnd, _)) ->
+        push_env push_user_id na (Function {arity=List.length bnd}) env)
+      env lets
+  in
+  let lets = List.map2 (fun (_, (bnd, e)) na' ->
+      let env, bnd = push_env push_user_names bnd Valexpr env in
+      let e = tac_expr env e in
+      (na', (bnd, e)))
+      lets
+      nas'
+  in
+  env, lets
+
 let nontac_expr env state acc e =
   let state = ref state in
   let acc, e = nontac_expr {env;state} acc e in
@@ -799,7 +814,16 @@ let rec pp_nontac_expr = function
        str "in" ++ spc() ++
        pp_nontac_expr e ++
        str ")")
-
+  | ValLetRec (lets, e) ->
+    let pr_one_let (na, (bnd, e)) =
+      hov 1 (Id.print na ++ pp_binders bnd ++ str " =") ++ spc () ++
+      pp_expr e ++ spc()
+    in
+    surround
+      (hv 0
+         (str "let rec " ++ prlist_with_sep (fun () -> str "and ") pr_one_let lets ++
+          str "in" ++ spc()) ++
+       pp_nontac_expr e)
 
 (* produce a ocaml term of type valexpr tactic *)
 and pp_expr e =

src/tac2compiledPrim.ml

@@ -16,7 +16,7 @@ open Proofview.Notations
 
 let core_prefix path n = KerName.make path (Label.of_id (Id.of_string_soft n))
 
-let coq_core n = core_prefix Tac2env.coq_prefix n
+let coq_core n = core_prefix Tac2env.rocq_prefix n
 
 let err_outofbounds =
   Tac2interp.LtacError (coq_core "Out_of_bounds", [||])

tests/Makefile

@@ -5,7 +5,7 @@ submake: Makefile.coq
 	$(MAKE) $(MAKE_OPTS) -f Makefile.coq $(MAKECMDGOALS)
 
 Makefile.coq: _CoqProject
-	$(COQBIN)coq_makefile -f $< -o $@
+	$(COQBIN)coq_makefile -f $< -o $@ $(wildcard *.v)
 
 %:: submake ;
 

tests/_CoqProject

@@ -3,16 +3,6 @@
 
 -R . Test
 
-tac2compile_test.v
-bug_10107.v
-minibench.v
-compiler_bug_4.v
-compiler_bug_6.v
-compiler_bug_14.v
-compiler_bug_16.v
-compiler_bug_17.v
-compiler_bug_24.v
-
 -I src
 
 src/META.compiler-bugs

tests/bug_10107.v

@@ -17,7 +17,7 @@ Ltac2 rec iter tac ls :=
 
 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.Cast c _cst ty => find id c; find id ty
   | Constr.Unsafe.App f xs => find id f; Array.iter (find id) xs
   | _ => ()
   end.
@@ -32,6 +32,6 @@ Goal True.
          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.
+       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 *)
 Abort.

tests/compiler_bug_29.v

@@ -0,0 +1,7 @@
+Require Import Ltac2.Ltac2.
+Require Import Ltac2Compiler.Ltac2Compiler.
+
+Ltac2 foo := let rec foo () := foo () in foo.
+
+Ltac2 Compile foo.
+(* Error: Anomaly "File "src/tac2compile.ml", line 662, characters 2-8: Assertion failed." *)

tests/tac2compile_test.v

@@ -189,7 +189,7 @@ Module MatchGoal.
 
   Ltac2 check () :=
     lazy_match! goal with
-    | [ h1 : context c1 [ ?t1 ] , h2 := context c2 [ Nat.add ?v2 ] , h3 : context c3 [ ?t2 ] |- _ ] =>
+    | [ _h1 : context c1 [ ?t1 ] , _h2 := context c2 [ Nat.add ?v2 ] , _h3 : context c3 [ ?t2 ] |- _ ] =>
         check_constr t1 'bool;
         check_constr v2 '0;
         check_constr t2 'bool;