Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Ltac2: use 0 argument externals when possible #17534

Merged
merged 2 commits into from Dec 4, 2023
Merged

Ltac2: use 0 argument externals when possible #17534

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0b2fa5a
Ltac2: use 0 argument externals when possible
SkySkimmer Apr 26, 2023
3260fa8
Compat for 0 arg Ltac2.Array.empty
SkySkimmer Nov 8, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
4 changes: 4 additions & 0 deletions doc/changelog/06-Ltac2-language/17534-ltac2-0arg-empty.rst
View file
Open in desktop
@@ -0,0 +1,4 @@
- **Changed:**
`Array.empty`, `Message.Format.stop` and `Pattern.empty_context` are not thunked
(`#17534 <https://github.com/coq/coq/pull/17534>`_,
by Gaëtan Gilbert).
8 changes: 4 additions & 4 deletions plugins/ltac2/tac2core.ml
View file
Open in desktop
Expand Up @@ -273,7 +273,7 @@ let () =

let () = define "message_concat" (pp @-> pp @-> ret pp) Pp.app

let () = define "format_stop" (unit @-> ret format) (fun _ -> [])
let () = define "format_stop" (ret format) []

let () =
define "format_string" (format @-> ret format) @@ fun s ->
Expand Down Expand Up @@ -346,7 +346,7 @@ let () =

(** Array *)

let () = define "array_empty" (unit @-> ret valexpr) (fun _ -> v_blk 0 [||])
let () = define "array_empty" (ret valexpr) (v_blk 0 [||])

let () =
define "array_make" (int @-> valexpr @-> tac valexpr) @@ fun n x ->
Expand Down Expand Up @@ -816,8 +816,8 @@ let () =

let () =
define "pattern_empty_context"
(unit @-> ret (repr_ext val_matching_context))
(fun _ -> Constr_matching.empty_context)
(ret (repr_ext val_matching_context))
Constr_matching.empty_context

let () =
define "pattern_matches" (pattern @-> constr @-> tac valexpr) @@ fun pat c ->
Expand Down
2 changes: 1 addition & 1 deletion plugins/ltac2/tac2quote.ml
View file
Open in desktop
Expand Up @@ -553,5 +553,5 @@ let of_format { v = fmt; loc } =
with Tac2print.InvalidFormat ->
CErrors.user_err ?loc (str "Invalid format")
in
let stop = CAst.make @@ CTacApp (global_ref (kername format_prefix "stop"), [of_tuple []]) in
let stop = global_ref (kername format_prefix "stop") in
List.fold_left of_format stop fmt
12 changes: 6 additions & 6 deletions test-suite/ltac2/array_lib.v
View file
Open in desktop
Expand Up @@ -45,14 +45,14 @@ Goal True.
Fail check_eq_int ((init 3 (fun i => (Int.add i 10)))) [10;11;13].

(* test empty with int *)
check_eq_int (empty ()) [].
check_eq_int (append (empty ()) (init 3 (fun i => (Int.add i 10)))) [10;11;12].
check_eq_int (append (init 3 (fun i => (Int.add i 10))) (empty ())) [10;11;12].
check_eq_int empty [].
check_eq_int (append empty (init 3 (fun i => (Int.add i 10)))) [10;11;12].
check_eq_int (append (init 3 (fun i => (Int.add i 10))) empty) [10;11;12].

(* test empty with bool *)
check_eq_bool (empty ()) [].
check_eq_bool (append (empty ()) (init 3 (fun i => (Int.ge i 2)))) [false;false;true].
check_eq_bool (append (init 3 (fun i => (Int.ge i 2))) (empty ())) [false;false;true].
check_eq_bool empty [].
check_eq_bool (append empty (init 3 (fun i => (Int.ge i 2)))) [false;false;true].
check_eq_bool (append (init 3 (fun i => (Int.ge i 2))) empty) [false;false;true].

(* test init with int *)
check_eq_int (init 0 (fun i => (Int.add i 10))) [].
Expand Down
2 changes: 1 addition & 1 deletion test-suite/ltac2/fragile_matching.v
View file
Open in desktop
Expand Up @@ -109,7 +109,7 @@ Module RealCodeTest.
} =>
true
end)
(Array.empty ())
Array.empty
}.

End RealCodeTest.
4 changes: 2 additions & 2 deletions theories/Compat/Coq817.v
View file
Open in desktop
Expand Up @@ -10,12 +10,12 @@

(** Compatibility file for making Coq act similar to Coq v8.17 *)

Local Set Warnings "-masking-absolute-name".

Require Export Coq.Compat.Coq818.

Require Coq.Lists.ListSet.

Local Set Warnings "-masking-absolute-name".

Module Export Coq.
Module Export Lists.
Module Export ListSet.
Expand Down
11 changes: 11 additions & 0 deletions theories/Compat/Coq818.v
View file
Open in desktop
Expand Up @@ -55,3 +55,14 @@ Ltac Z.euclidean_division_equations_cleanup ::=
| [ H : ?A -> ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
| [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
end.

Local Set Warnings "-masking-absolute-name".

Require Ltac2.Array.

Module Export Ltac2.
Module Array.
Export Ltac2.Array.
Ltac2 empty () := empty.
End Array.
End Ltac2.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@SkySkimmer @ppedrot this seems wrong, as it makes the stdlib depend on Ltac2 .

It doesn't fail in CI because we implicitly put Ltac2 in scope, but that could change in the future.

I'm not sure we should do anything about this, but at least I feel I had to signal it to you.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't we have Compat as a separate theory depending on everything from Coq?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't know, several options are possible; I guess it'd make more sense to have the stdlib depend on Ltac2?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

As of today we handle Ltac2 and Coq as the same package, in both cases we pass -boot -Q $path_to_ltac2 Ltac2 -R $path_to_theories Coq, so there is no separation.

I detected this issue on some private setups I have where I enforce more separation.

For example if you wish, we could compile Ltac2 without -R theories Coq and with -noinit, similarly for the stdlib.

8 changes: 4 additions & 4 deletions user-contrib/Ltac2/Array.v
View file
Open in desktop
Expand Up @@ -34,7 +34,7 @@ Require Ltac2.Message.
(* Question: what is returned in case of an out of range value?
Answer: Ltac2 throws a panic *)

Ltac2 @external empty : unit -> 'a array := "coq-core.plugins.ltac2" "array_empty".
Ltac2 @external empty : 'a array := "coq-core.plugins.ltac2" "array_empty".
Ltac2 @external make : int -> 'a -> 'a array := "coq-core.plugins.ltac2" "array_make".
Ltac2 @external length : 'a array -> int := "coq-core.plugins.ltac2" "array_length".
Ltac2 @external get : 'a array -> int -> 'a := "coq-core.plugins.ltac2" "array_get".
Expand All @@ -48,7 +48,7 @@ Ltac2 @external concat : ('a array) list -> 'a array := "coq-core.plugins.ltac2"
Ltac2 lowlevel_sub (arr : 'a array) (start : int) (len : int) :=
let l := length arr in
match Int.equal l 0 with
| true => empty ()
| true => empty
| false =>
let newarr:=make len (get arr 0) in
lowlevel_blit arr start newarr 0 len;
Expand All @@ -67,7 +67,7 @@ Ltac2 init (l : int) (f : int->'a) :=
end
in
match Int.le l 0 with
| true => empty ()
| true => empty
| false =>
let arr:=make l (f 0) in
init_aux arr 1 (Int.sub l 1) f;
Expand Down Expand Up @@ -174,7 +174,7 @@ Ltac2 of_list (ls : 'a list) :=
| _ :: tl => Int.add 1 (list_length tl)
end in
match ls with
| [] => empty ()
| [] => empty
| hd::tl =>
let anew := make (list_length ls) hd in
of_list_aux ls anew 0;
Expand Down
2 changes: 1 addition & 1 deletion user-contrib/Ltac2/Message.v
View file
Open in desktop
Expand Up @@ -32,7 +32,7 @@ Module Format.

(** Only for internal use. *)

Ltac2 @ external stop : unit -> ('a, 'b, 'c, 'a) format := "coq-core.plugins.ltac2" "format_stop".
Ltac2 @ external stop : ('a, 'b, 'c, 'a) format := "coq-core.plugins.ltac2" "format_stop".

Ltac2 @ external string : ('a, 'b, 'c, 'd) format ->
(string -> 'a, 'b, 'c, 'd) format := "coq-core.plugins.ltac2" "format_string".
Expand Down
6 changes: 3 additions & 3 deletions user-contrib/Ltac2/Pattern.v
View file
Open in desktop
Expand Up @@ -20,7 +20,7 @@ Ltac2 Type match_kind := [
| MatchContext
].

Ltac2 @ external empty_context : unit -> context :=
Ltac2 @ external empty_context : context :=
"coq-core.plugins.ltac2" "pattern_empty_context".
(** A trivial context only made of the hole. *)

Expand Down Expand Up @@ -88,7 +88,7 @@ Ltac2 lazy_match0 t (pats:'a constr_matching) :=
let p := match knd with
| MatchPattern =>
(fun _ =>
let context := empty_context () in
let context := empty_context in
let bind := matches_vect pat t in
fun _ => f context bind)
| MatchContext =>
Expand All @@ -109,7 +109,7 @@ Ltac2 multi_match0 t (pats:'a constr_matching) :=
let p := match knd with
| MatchPattern =>
(fun _ =>
let context := empty_context () in
let context := empty_context in
let bind := matches_vect pat t in
f context bind)
| MatchContext =>
Expand Down