From 616700f03d94fc6113c6b8aa5a26e44972aee86a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?=
Date: Thu, 21 Dec 2023 11:39:37 +0100
Subject: [PATCH 1/6] Ltac2 CTacSyn is statically using names not patterns for
arguments
---
plugins/ltac2/tac2entries.ml | 2 +-
plugins/ltac2/tac2expr.mli | 2 +-
plugins/ltac2/tac2intern.ml | 2 ++
3 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/plugins/ltac2/tac2entries.ml b/plugins/ltac2/tac2entries.ml
index 079061b7b2c8..d82b60b42309 100644
--- a/plugins/ltac2/tac2entries.ml
+++ b/plugins/ltac2/tac2entries.ml
@@ -674,7 +674,7 @@ let perform_notation syn st =
| Some depr -> deprecated_ltac2_notation ~loc (syn.synext_tok, depr)
in
let map (na, e) =
- ((CAst.make ?loc:e.loc @@ CPatVar na), e)
+ ((CAst.make ?loc:e.loc na), e)
in
let bnd = List.map map args in
CAst.make ~loc @@ CTacSyn (bnd, syn.synext_kn)
diff --git a/plugins/ltac2/tac2expr.mli b/plugins/ltac2/tac2expr.mli
index 6a439adf5183..e4033aeb0ed1 100644
--- a/plugins/ltac2/tac2expr.mli
+++ b/plugins/ltac2/tac2expr.mli
@@ -107,7 +107,7 @@ type raw_tacexpr_r =
| CTacCst of ltac_constructor or_tuple or_relid
| CTacFun of raw_patexpr list * raw_tacexpr
| CTacApp of raw_tacexpr * raw_tacexpr list
-| CTacSyn of (raw_patexpr * raw_tacexpr) list * KerName.t
+| CTacSyn of (lname * raw_tacexpr) list * KerName.t
| CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
| CTacCnv of raw_tacexpr * raw_typexpr
| CTacSeq of raw_tacexpr * raw_tacexpr
diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml
index ab19f0c8c6a3..2685cb765e60 100644
--- a/plugins/ltac2/tac2intern.ml
+++ b/plugins/ltac2/tac2intern.ml
@@ -1186,6 +1186,7 @@ let rec intern_rec env tycon {loc;v=e} =
else intern_let env loc ids el tycon e
| CTacSyn (el, kn) ->
let body = Tac2env.interp_notation kn in
+ let el = List.map (fun (pat, e) -> CAst.map (fun na -> CPatVar na) pat, e) el in
let v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
intern_rec env tycon v
| CTacCnv (e, tc) ->
@@ -1603,6 +1604,7 @@ let globalize_gen ~tacext ids tac =
CAst.make ?loc @@ CTacLet (isrec, bnd, e)
| CTacSyn (el, kn) ->
let body = Tac2env.interp_notation kn in
+ let el = List.map (fun (pat, e) -> CAst.map (fun na -> CPatVar na) pat, e) el in
let v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
globalize ids v
| CTacCnv (e, t) ->
From aca716eca1d685e09ee78c146de7b207e9966a97 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?=
Date: Thu, 21 Dec 2023 15:02:37 +0100
Subject: [PATCH 2/6] Ltac2 infrastructure for typed notations
---
plugins/ltac2/tac2entries.ml | 19 ++++++++--
plugins/ltac2/tac2env.ml | 9 +++++
plugins/ltac2/tac2env.mli | 14 ++++++-
plugins/ltac2/tac2expr.mli | 73 +++++++++++++++++++-----------------
plugins/ltac2/tac2intern.ml | 68 ++++++++++++++++++++++++++++++---
plugins/ltac2/tac2intern.mli | 1 +
plugins/ltac2/tac2print.ml | 28 ++++++++++++++
7 files changed, 165 insertions(+), 47 deletions(-)
diff --git a/plugins/ltac2/tac2entries.ml b/plugins/ltac2/tac2entries.ml
index d82b60b42309..029a11f4eeca 100644
--- a/plugins/ltac2/tac2entries.ml
+++ b/plugins/ltac2/tac2entries.ml
@@ -721,8 +721,19 @@ let cache_synext_interp (local,kn,tac) =
let open_synext_interp i o =
if Int.equal i 1 then cache_synext_interp o
+let subst_notation_data subst = function
+ | Tac2env.UntypedNota body as n ->
+ let body' = Tac2intern.subst_rawexpr subst body in
+ if body' == body then n else UntypedNota body'
+ | TypedNota { nota_prms=prms; nota_argtys=argtys; nota_ty=ty; nota_body=body } as n ->
+ let body' = Tac2intern.subst_expr subst body in
+ let argtys' = Id.Map.Smart.map (subst_type subst) argtys in
+ let ty' = subst_type subst ty in
+ if body' == body && argtys' == argtys && ty' == ty then n
+ else TypedNota {nota_body=body'; nota_argtys=argtys'; nota_ty=ty'; nota_prms=prms}
+
let subst_synext_interp (subst, (local,kn,tac as o)) =
- let tac' = Tac2intern.subst_rawexpr subst tac in
+ let tac' = subst_notation_data subst tac in
let kn' = Mod_subst.subst_kn subst kn in
if kn' == kn && tac' == tac then o else
(local, kn', tac')
@@ -730,7 +741,7 @@ let subst_synext_interp (subst, (local,kn,tac as o)) =
let classify_synext_interp (local,_,_) =
if local then Dispose else Substitute
-let inTac2NotationInterp : (bool*KerName.t*raw_tacexpr) -> obj =
+let inTac2NotationInterp : (bool*KerName.t*Tac2env.notation_data) -> obj =
declare_object {(default_object "TAC2-NOTATION-INTERP") with
cache_function = cache_synext_interp;
open_function = simple_open ~cat:ltac2_notation_cat open_synext_interp;
@@ -837,8 +848,8 @@ let register_notation_interpretation = function
let abbr = { abbr_body = body; abbr_depr = deprecation } in
Lib.add_leaf (inTac2Abbreviation id abbr)
| Synext (local,kn,ids,body) ->
- let body = Tac2intern.globalize ids body in
- Lib.add_leaf (inTac2NotationInterp (local,kn,body))
+ let data = intern_notation_data ids body in
+ Lib.add_leaf (inTac2NotationInterp (local,kn,data))
type redefinition = {
redef_kn : ltac_constant;
diff --git a/plugins/ltac2/tac2env.ml b/plugins/ltac2/tac2env.ml
index 775725ffb1bd..b9965b2ecdd5 100644
--- a/plugins/ltac2/tac2env.ml
+++ b/plugins/ltac2/tac2env.ml
@@ -65,6 +65,15 @@ let ltac_state = Summary.ref empty_state ~name:"ltac2-state"
let compiled_tacs = Summary.ref ~local:true ~name:"ltac2-compiled-state" KNmap.empty
+type notation_data =
+ | UntypedNota of raw_tacexpr
+ | TypedNota of {
+ nota_prms : int;
+ nota_argtys : int glb_typexpr Id.Map.t;
+ nota_ty : int glb_typexpr;
+ nota_body : glb_tacexpr;
+ }
+
let ltac_notations = Summary.ref KNmap.empty ~stage:Summary.Stage.Synterp ~name:"ltac2-notations"
let define_global kn e =
diff --git a/plugins/ltac2/tac2env.mli b/plugins/ltac2/tac2env.mli
index 555a014e12d6..7356208ba3ad 100644
--- a/plugins/ltac2/tac2env.mli
+++ b/plugins/ltac2/tac2env.mli
@@ -95,8 +95,18 @@ val interp_alias : ltac_constant -> alias_data
(** {5 Toplevel definition of notations} *)
-val define_notation : ltac_notation -> raw_tacexpr -> unit
-val interp_notation : ltac_notation -> raw_tacexpr
+(* no deprecation info: deprecation warning is emitted by the parser *)
+type notation_data =
+ | UntypedNota of raw_tacexpr
+ | TypedNota of {
+ nota_prms : int;
+ nota_argtys : int glb_typexpr Id.Map.t;
+ nota_ty : int glb_typexpr;
+ nota_body : glb_tacexpr;
+ }
+
+val define_notation : ltac_notation -> notation_data -> unit
+val interp_notation : ltac_notation -> notation_data
(** {5 Name management} *)
diff --git a/plugins/ltac2/tac2expr.mli b/plugins/ltac2/tac2expr.mli
index e4033aeb0ed1..bc2df44b2ec3 100644
--- a/plugins/ltac2/tac2expr.mli
+++ b/plugins/ltac2/tac2expr.mli
@@ -89,41 +89,6 @@ type atom =
| AtmInt of int
| AtmStr of string
-(** Tactic expressions *)
-type raw_patexpr_r =
-| CPatVar of Name.t
-| CPatAtm of atom
-| CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
-| CPatRecord of (ltac_projection or_relid * raw_patexpr) list
-| CPatCnv of raw_patexpr * raw_typexpr
-| CPatOr of raw_patexpr list
-| CPatAs of raw_patexpr * lident
-
-and raw_patexpr = raw_patexpr_r CAst.t
-
-type raw_tacexpr_r =
-| CTacAtm of atom
-| CTacRef of tacref or_relid
-| CTacCst of ltac_constructor or_tuple or_relid
-| CTacFun of raw_patexpr list * raw_tacexpr
-| CTacApp of raw_tacexpr * raw_tacexpr list
-| CTacSyn of (lname * raw_tacexpr) list * KerName.t
-| CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
-| CTacCnv of raw_tacexpr * raw_typexpr
-| CTacSeq of raw_tacexpr * raw_tacexpr
-| CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
-| CTacCse of raw_tacexpr * raw_taccase list
-| CTacRec of raw_tacexpr option * raw_recexpr
-| CTacPrj of raw_tacexpr * ltac_projection or_relid
-| CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
-| CTacExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr_r
-
-and raw_tacexpr = raw_tacexpr_r CAst.t
-
-and raw_taccase = raw_patexpr * raw_tacexpr
-
-and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list
-
(* We want to generate these easily in the Closed case, otherwise we
could have the kn in the ctor_data_for_patterns type. Maybe still worth doing?? *)
type ctor_indx =
@@ -180,6 +145,44 @@ type glb_tacexpr =
| GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr
| GTacPrm of ml_tactic_name
+(** Tactic expressions *)
+type raw_patexpr_r =
+| CPatVar of Name.t
+| CPatAtm of atom
+| CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
+| CPatRecord of (ltac_projection or_relid * raw_patexpr) list
+| CPatCnv of raw_patexpr * raw_typexpr
+| CPatOr of raw_patexpr list
+| CPatAs of raw_patexpr * lident
+
+and raw_patexpr = raw_patexpr_r CAst.t
+
+type raw_tacexpr_r =
+| CTacAtm of atom
+| CTacRef of tacref or_relid
+| CTacCst of ltac_constructor or_tuple or_relid
+| CTacFun of raw_patexpr list * raw_tacexpr
+| CTacApp of raw_tacexpr * raw_tacexpr list
+| CTacSyn of (lname * raw_tacexpr) list * KerName.t
+| CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
+| CTacCnv of raw_tacexpr * raw_typexpr
+| CTacSeq of raw_tacexpr * raw_tacexpr
+| CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
+| CTacCse of raw_tacexpr * raw_taccase list
+| CTacRec of raw_tacexpr option * raw_recexpr
+| CTacPrj of raw_tacexpr * ltac_projection or_relid
+| CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
+| CTacExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr_r
+| CTacGlb of int * (lname * raw_tacexpr * int glb_typexpr option) list * glb_tacexpr * int glb_typexpr
+(** CTacGlb is essentially an expanded typed notation.
+ Arguments bound with Anonymous have no type constraint. *)
+
+and raw_tacexpr = raw_tacexpr_r CAst.t
+
+and raw_taccase = raw_patexpr * raw_tacexpr
+
+and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list
+
(** {5 Parsing & Printing} *)
type exp_level =
diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml
index 2685cb765e60..c7937c7ce1c2 100644
--- a/plugins/ltac2/tac2intern.ml
+++ b/plugins/ltac2/tac2intern.ml
@@ -1089,6 +1089,25 @@ let warn_useless_record_with = CWarnings.create ~name:"ltac2-useless-record-with
str "All the fields are explicitly listed in this record:" ++
spc() ++ str "the 'with' clause is useless.")
+let expand_notation ?loc el kn =
+ match Tac2env.interp_notation kn with
+ | UntypedNota body ->
+ let el = List.map (fun (pat, e) -> CAst.map (fun na -> CPatVar na) pat, e) el in
+ let v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
+ v
+ | TypedNota {nota_prms=prms; nota_argtys=argtys; nota_ty=ty; nota_body=body} ->
+ let argtys, el = List.fold_left_map (fun argtys (na,arg) ->
+ let argty, argtys = match na.CAst.v with
+ | Anonymous -> None, argtys
+ | Name id -> Some (Id.Map.get id argtys), Id.Map.remove id argtys
+ in
+ argtys ,(na, arg, argty))
+ argtys
+ el
+ in
+ assert (Id.Map.is_empty argtys);
+ CAst.make ?loc @@ CTacGlb (prms, el, body, ty)
+
let rec intern_rec env tycon {loc;v=e} =
let check et = check ?loc env tycon et in
match e with
@@ -1185,9 +1204,7 @@ let rec intern_rec env tycon {loc;v=e} =
if is_rec then intern_let_rec env el tycon e
else intern_let env loc ids el tycon e
| CTacSyn (el, kn) ->
- let body = Tac2env.interp_notation kn in
- let el = List.map (fun (pat, e) -> CAst.map (fun na -> CPatVar na) pat, e) el in
- let v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
+ let v = expand_notation ?loc el kn in
intern_rec env tycon v
| CTacCnv (e, tc) ->
let tc = intern_type env tc in
@@ -1317,6 +1334,28 @@ let rec intern_rec env tycon {loc;v=e} =
| GlbTacexpr e -> e
in
check (e, tpe)
+| CTacGlb (prms, args, body, ty) ->
+ let tysubst = Array.init prms (fun _ -> fresh_id env) in
+ let tysubst i = GTypVar tysubst.(i) in
+ let ty = subst_type tysubst ty in
+ let ty = match tycon with
+ | None -> ty
+ | Some tycon ->
+ let () = unify ?loc env ty tycon in
+ tycon
+ in
+ let args = List.map (fun (na, arg, ty) ->
+ let ty = Option.map (subst_type tysubst) ty in
+ let () = match na.CAst.v, ty with
+ | Anonymous, None | Name _, Some _ -> ()
+ | Anonymous, Some _ | Name _, None -> assert false
+ in
+ let e, _ = intern_rec env ty arg in
+ na.CAst.v, e)
+ args
+ in
+ if CList.is_empty args then body, ty
+ else GTacLet (false, args, body), ty
and intern_rec_with_constraint env e exp =
let (er, t) = intern_rec env (Some exp) e in
@@ -1603,9 +1642,7 @@ let globalize_gen ~tacext ids tac =
let bnd = List.map map bnd in
CAst.make ?loc @@ CTacLet (isrec, bnd, e)
| CTacSyn (el, kn) ->
- let body = Tac2env.interp_notation kn in
- let el = List.map (fun (pat, e) -> CAst.map (fun na -> CPatVar na) pat, e) el in
- let v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
+ let v = expand_notation ?loc el kn in
globalize ids v
| CTacCnv (e, t) ->
let e = globalize ids e in
@@ -1641,6 +1678,9 @@ let globalize_gen ~tacext ids tac =
let e' = globalize ids e' in
CAst.make ?loc @@ CTacSet (e, AbsKn p, e')
| CTacExt (tag, arg) -> tacext ?loc (RawExt (tag, arg))
+ | CTacGlb (prms, args, body, ty) ->
+ let args = List.map (fun (na, arg, ty) -> na, globalize ids arg, ty) args in
+ CAst.make ?loc @@ CTacGlb (prms, args, body, ty)
and globalize_case ids (p, e) =
(globalize_pattern ids p, globalize ids e)
@@ -1682,6 +1722,10 @@ let debug_globalize_allow_ext ids tac =
let tacext ?loc (RawExt (tag,arg)) = CAst.make ?loc @@ CTacExt (tag,arg) in
globalize_gen ~tacext ids tac
+let intern_notation_data ids body =
+ let body = globalize ids body in
+ Tac2env.UntypedNota body
+
(** Kernel substitution *)
open Mod_subst
@@ -1936,6 +1980,18 @@ let rec subst_rawexpr subst ({loc;v=tr} as t) = match tr with
let e' = subst_rawexpr subst e in
let r' = subst_rawexpr subst r in
if prj' == prj && e' == e && r' == r then t else CAst.make ?loc @@ CTacSet (e', prj', r')
+| CTacGlb (prms, args, body, ty) ->
+ let args' = List.Smart.map (fun (na, arg, ty as o) ->
+ let arg' = subst_rawexpr subst arg in
+ let ty' = Option.Smart.map (subst_type subst) ty in
+ if arg' == arg && ty' == ty then o
+ else (na, arg', ty'))
+ args
+ in
+ let body' = subst_expr subst body in
+ let ty' = subst_type subst ty in
+ if args' == args && body' == body && ty' == ty then t
+ else CAst.make ?loc @@ CTacGlb (prms, args', body', ty')
| CTacSyn _ | CTacExt _ -> assert false (** Should not be generated by globalization *)
(** Registering *)
diff --git a/plugins/ltac2/tac2intern.mli b/plugins/ltac2/tac2intern.mli
index 22a082f2bafb..58a2ff58949d 100644
--- a/plugins/ltac2/tac2intern.mli
+++ b/plugins/ltac2/tac2intern.mli
@@ -17,6 +17,7 @@ type context = (Id.t * type_scheme) list
val intern : strict:bool -> context -> raw_tacexpr -> glb_tacexpr * type_scheme
val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef
val intern_open_type : raw_typexpr -> type_scheme
+val intern_notation_data : Id.Set.t -> raw_tacexpr -> Tac2env.notation_data
(** Check that a term is a value. Only values are safe to marshall between
processes. *)
diff --git a/plugins/ltac2/tac2print.ml b/plugins/ltac2/tac2print.ml
index 3b4d96c2f0f2..d661e444f2fb 100644
--- a/plugins/ltac2/tac2print.ml
+++ b/plugins/ltac2/tac2print.ml
@@ -575,6 +575,8 @@ let rec pr_rawpat_gen lvl p = match p.CAst.v with
in
paren (hv 0 (pr_rawpat_gen E1 p ++ spc() ++ str "as" ++ spc () ++ Id.print x.v))
+(* XXX in principle we could have collisions with user names *)
+let base_internal_ty_ident = Id.of_string "__α"
let pr_rawexpr_gen lvl ~avoid c =
let rec pr_rawexpr lvl avoid c =
@@ -699,6 +701,32 @@ let pr_rawexpr_gen lvl ~avoid c =
let env = Global.env() in
let sigma = Evd.from_env env in
obj.ml_raw_print env sigma arg
+ | CTacGlb (prms, args, body, ty) ->
+ let avoid, tynames =
+ Array.fold_left_map (fun avoid () ->
+ let na = Namegen.next_ident_away base_internal_ty_ident avoid in
+ let avoid = Id.Set.add na avoid in
+ avoid, Id.to_string na)
+ avoid
+ (Array.make prms ())
+ in
+ let tynames i = tynames.(i) in
+ let pr_arg (pat, arg, ty) =
+ let bnd = match ty with
+ | Some ty ->
+ paren (pr_name pat.CAst.v ++ spc() ++ str ":" ++ spc() ++ pr_glbtype_gen tynames T5_l ty)
+ | None -> pr_name pat.CAst.v
+ in
+ bnd ++ spc() ++ str ":=" ++ spc() ++ hov 2 (pr_rawexpr E5 avoid arg) ++ spc()
+ in
+ let paren = match lvl with
+ | E0 | E1 | E2 | E3 | E4 -> paren
+ | E5 -> fun x -> x
+ in
+ let bnd = prlist_with_sep (fun () -> str "with" ++ spc ()) pr_arg args in
+ paren (hv 0 (hov 2 (str "let" ++ spc() ++ bnd ++ str "in") ++ spc()
+ ++ pr_glbexpr_gen ~avoid E5 body ++ spc()
+ ++ str ":" ++ pr_glbtype_gen tynames T5_l ty))
in
hov 0 (pr_rawexpr lvl avoid c)
From 882ddac22e6072988481fda5d5afc39810227f3f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?=
Date: Thu, 21 Dec 2023 15:37:03 +0100
Subject: [PATCH 3/6] Ltac2 typed notations
---
plugins/ltac2/tac2intern.ml | 29 +++++++++++++++++++++++++++--
1 file changed, 27 insertions(+), 2 deletions(-)
diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml
index c7937c7ce1c2..870c58a3d82b 100644
--- a/plugins/ltac2/tac2intern.ml
+++ b/plugins/ltac2/tac2intern.ml
@@ -1722,9 +1722,34 @@ let debug_globalize_allow_ext ids tac =
let tacext ?loc (RawExt (tag,arg)) = CAst.make ?loc @@ CTacExt (tag,arg) in
globalize_gen ~tacext ids tac
+let { Goptions.get = typed_notations } =
+ Goptions.declare_bool_option_and_ref
+ ~key:["Ltac2";"Typed";"Notations"] ~value:false ()
+
let intern_notation_data ids body =
- let body = globalize ids body in
- Tac2env.UntypedNota body
+ if typed_notations () then
+ let env = empty_env ~strict:true () in
+ let fold id (env,argtys) =
+ let ty = GTypVar (fresh_id env) in
+ let env = push_name (Name id) (monomorphic ty) env in
+ env, Id.Map.add id ty argtys
+ in
+ let env, argtys = Id.Set.fold fold ids (env,Id.Map.empty) in
+ let body, ty = intern_rec env None body in
+ let count = ref 0 in
+ let vars = ref TVar.Map.empty in
+ let argtys = Id.Map.map (fun ty -> normalize env (count, vars) ty) argtys in
+ let ty = normalize env (count, vars) ty in
+ let prms = !count in
+ Tac2env.TypedNota {
+ nota_prms = prms;
+ nota_argtys = argtys;
+ nota_ty = ty;
+ nota_body = body;
+ }
+ else
+ let body = globalize ids body in
+ Tac2env.UntypedNota body
(** Kernel substitution *)
From cf8944bd201b743ebd524aadc279f771156d1a1b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?=
Date: Thu, 21 Dec 2023 15:39:11 +0100
Subject: [PATCH 4/6] Turn ltac2 typed notations on by default
Fix #17477
---
doc/stdlib/index-list.html.template | 1 +
plugins/ltac2/tac2intern.ml | 2 +-
sysinit/coqargs.ml | 1 +
test-suite/output/ltac2_check_globalize.out | 7 ++++---
test-suite/output/ltac2_check_globalize.v | 2 ++
test-suite/output/ltac2_typed_notations.out | 4 ++++
test-suite/output/ltac2_typed_notations.v | 9 +++++++++
user-contrib/Ltac2/Compat/Coq818.v | 2 ++
user-contrib/Ltac2/Compat/Coq819.v | 3 +++
9 files changed, 27 insertions(+), 4 deletions(-)
create mode 100644 test-suite/output/ltac2_typed_notations.out
create mode 100644 test-suite/output/ltac2_typed_notations.v
create mode 100644 user-contrib/Ltac2/Compat/Coq819.v
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index e57cfd7e8c05..f9c5eccfc597 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -710,6 +710,7 @@ through the Require Import command.
theories/Compat/Coq819.v
theories/Compat/Coq820.v
user-contrib/Ltac2/Compat/Coq818.v
+ user-contrib/Ltac2/Compat/Coq819.v
Array:
diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml
index 870c58a3d82b..5c4457835eeb 100644
--- a/plugins/ltac2/tac2intern.ml
+++ b/plugins/ltac2/tac2intern.ml
@@ -1724,7 +1724,7 @@ let debug_globalize_allow_ext ids tac =
let { Goptions.get = typed_notations } =
Goptions.declare_bool_option_and_ref
- ~key:["Ltac2";"Typed";"Notations"] ~value:false ()
+ ~key:["Ltac2";"Typed";"Notations"] ~value:true ()
let intern_notation_data ids body =
if typed_notations () then
diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index a465dfdefc6c..0a6efbf5259e 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -242,6 +242,7 @@ let get_compat_file = function
let get_compat_files v =
let coq_compat = get_compat_file v in
match v with
+ | "8.19" -> coq_compat :: ["Ltac2.Compat.Coq819"]
| "8.18" | "8.17" -> coq_compat :: ["Ltac2.Compat.Coq818"]
| _ -> [coq_compat]
diff --git a/test-suite/output/ltac2_check_globalize.out b/test-suite/output/ltac2_check_globalize.out
index cf70cba87c4f..b5a8f75bbb23 100644
--- a/test-suite/output/ltac2_check_globalize.out
+++ b/test-suite/output/ltac2_check_globalize.out
@@ -4,7 +4,7 @@ fun x => x : 'a -> 'a
() ()
(1, 2) 3
let x := () in x ()
-File "./output/ltac2_check_globalize.v", line 20, characters 32-33:
+File "./output/ltac2_check_globalize.v", line 22, characters 32-33:
The command has indeed failed with message:
This expression has type unit. It is not a function and cannot be applied.
let x := fun x => x in let _ := x 1 in let _ := x "" in ()
@@ -13,11 +13,11 @@ let accu := { contents := []} in
(let x := fun x => accu.(contents) := (x :: accu.(contents)) in
let _ := x 1 in let _ := x "" in ());
accu.(contents)
-File "./output/ltac2_check_globalize.v", line 36, characters 0-144:
+File "./output/ltac2_check_globalize.v", line 38, characters 0-144:
The command has indeed failed with message:
This expression has type string but an expression was expected of type
int
-let m :=
+let (m : '__α Pattern.goal_matching) :=
[(([(None, (Pattern.MatchPattern, pat:(_)))],
(Pattern.MatchPattern, pat:(_))),
(fun h =>
@@ -27,4 +27,5 @@ let m :=
(fun _ => fun _ => fun _ => fun _ => fun _ => ()))] : _
Pattern.goal_matching in
Pattern.lazy_goal_match0 false m
+:'__α
constr:(ltac2:(()))
diff --git a/test-suite/output/ltac2_check_globalize.v b/test-suite/output/ltac2_check_globalize.v
index 72ffc0d62f83..cbeea4f06581 100644
--- a/test-suite/output/ltac2_check_globalize.v
+++ b/test-suite/output/ltac2_check_globalize.v
@@ -1,5 +1,7 @@
Require Import Ltac2.Ltac2.
+Unset Ltac2 Typed Notations.
+
Ltac2 Notation "foo" := ().
Ltac2 Globalize foo.
diff --git a/test-suite/output/ltac2_typed_notations.out b/test-suite/output/ltac2_typed_notations.out
new file mode 100644
index 000000000000..91c0d870767a
--- /dev/null
+++ b/test-suite/output/ltac2_typed_notations.out
@@ -0,0 +1,4 @@
+File "./output/ltac2_typed_notations.v", line 5, characters 9-10:
+The command has indeed failed with message:
+This expression has type bool but an expression was expected of type
+constr
diff --git a/test-suite/output/ltac2_typed_notations.v b/test-suite/output/ltac2_typed_notations.v
new file mode 100644
index 000000000000..5048223c00ee
--- /dev/null
+++ b/test-suite/output/ltac2_typed_notations.v
@@ -0,0 +1,9 @@
+Require Import Ltac2.Ltac2.
+
+Fail Ltac2 foo(b: bool): bool :=
+ let c := b in
+ match! c with
+ | true => true
+ | false => false
+ end.
+(* error used to be on the whole command *)
diff --git a/user-contrib/Ltac2/Compat/Coq818.v b/user-contrib/Ltac2/Compat/Coq818.v
index f97a43c0d28c..d0b4b8576c06 100644
--- a/user-contrib/Ltac2/Compat/Coq818.v
+++ b/user-contrib/Ltac2/Compat/Coq818.v
@@ -1,5 +1,7 @@
Local Set Warnings "-masking-absolute-name".
+Require Export Ltac2.Compat.Coq819.
+
Require Ltac2.Array.
Module Export Ltac2.
diff --git a/user-contrib/Ltac2/Compat/Coq819.v b/user-contrib/Ltac2/Compat/Coq819.v
new file mode 100644
index 000000000000..f1345eb96d60
--- /dev/null
+++ b/user-contrib/Ltac2/Compat/Coq819.v
@@ -0,0 +1,3 @@
+Require Ltac2.Init.
+
+#[export] Unset Ltac2 Typed Notations.
From 58a2643cb5efc41d9b3f6718eea9ce6d506c111c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?=
Date: Thu, 21 Dec 2023 15:42:41 +0100
Subject: [PATCH 5/6] More ltac2 typed notations testing, remove now useless
extra type annotation
---
plugins/ltac2/tac2quote.ml | 5 +----
test-suite/output/ltac2_typed_notations.out | 10 ++++++++++
test-suite/output/ltac2_typed_notations.v | 7 +++++++
3 files changed, 18 insertions(+), 4 deletions(-)
diff --git a/plugins/ltac2/tac2quote.ml b/plugins/ltac2/tac2quote.ml
index 0e817036303c..ae2a6385aa32 100644
--- a/plugins/ltac2/tac2quote.ml
+++ b/plugins/ltac2/tac2quote.ml
@@ -450,10 +450,7 @@ let of_constr_matching {loc;v=m} =
of_tuple [knd; pat; e]
in
let e = of_list ?loc map m in
- let tykn = pattern_core "constr_matching" in
- let ty = CAst.make ?loc (CTypRef (AbsKn (Other tykn),[CAst.make ?loc (CTypVar Anonymous)])) in
- CAst.make ?loc (CTacCnv (e, ty))
-
+ e
(** From the patterns and the body of the branch, generate:
- a goal pattern: (constr_match list * constr_match)
diff --git a/test-suite/output/ltac2_typed_notations.out b/test-suite/output/ltac2_typed_notations.out
index 91c0d870767a..5898783ae6d9 100644
--- a/test-suite/output/ltac2_typed_notations.out
+++ b/test-suite/output/ltac2_typed_notations.out
@@ -2,3 +2,13 @@ File "./output/ltac2_typed_notations.v", line 5, characters 9-10:
The command has indeed failed with message:
This expression has type bool but an expression was expected of type
constr
+fun (b : bool) =>
+let c := b in
+let (m : '__α Pattern.constr_matching) :=
+ [(Pattern.MatchPattern, pat:(true),
+ (fun _ => fun (_ : constr array) => true));
+ (Pattern.MatchPattern, pat:(false),
+ (fun _ => fun (_ : constr array) => false))] with
+ (t : constr) := c in
+Pattern.one_match0 t m
+:'__α : bool
diff --git a/test-suite/output/ltac2_typed_notations.v b/test-suite/output/ltac2_typed_notations.v
index 5048223c00ee..2de4a96c76cd 100644
--- a/test-suite/output/ltac2_typed_notations.v
+++ b/test-suite/output/ltac2_typed_notations.v
@@ -7,3 +7,10 @@ Fail Ltac2 foo(b: bool): bool :=
| false => false
end.
(* error used to be on the whole command *)
+
+Ltac2 Globalize fun (b: bool) =>
+ (let c := b in
+ match! c with
+ | true => true
+ | false => false
+ end : bool).
From 1512cc3981fa9f1cf1cb0dd53edcb4f2d791edb4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?=
Date: Tue, 23 Jan 2024 13:58:27 +0100
Subject: [PATCH 6/6] Doc for ltac2 typed notations
---
.../18432-ltac2-typed-notation.rst | 10 ++++++++++
doc/sphinx/proof-engine/ltac2.rst | 15 +++++++++++++--
2 files changed, 23 insertions(+), 2 deletions(-)
create mode 100644 doc/changelog/06-Ltac2-language/18432-ltac2-typed-notation.rst
diff --git a/doc/changelog/06-Ltac2-language/18432-ltac2-typed-notation.rst b/doc/changelog/06-Ltac2-language/18432-ltac2-typed-notation.rst
new file mode 100644
index 000000000000..8a3ec953076c
--- /dev/null
+++ b/doc/changelog/06-Ltac2-language/18432-ltac2-typed-notation.rst
@@ -0,0 +1,10 @@
+- **Changed:**
+ Ltac2 are typechecked at declaration time by default.
+ This should produce better errors when a notation argument does not have the expected type
+ (e.g. wrong branch type in `match! goal`).
+ The previous behaviour of typechecking only the expansion result can be
+ recovered using :flag:`Ltac2 Typed Notations`. We believe there are no real
+ use cases for this, please report if you have any
+ (`#18432 `_,
+ fixes `#17477 `_,
+ by Gaëtan Gilbert).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 862b12710f17..e42af2fb211b 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1220,11 +1220,22 @@ Notations
side (before the `:=`) defines the syntax to recognize and gives formal parameter
names for the syntactic values. :n:`@integer` is the level of the notation.
When the notation is used, the values are substituted
- into the right-hand side. The right-hand side is typechecked when the notation is used,
- not when it is defined. In the following example, `x` is the formal parameter name and
+ into the right-hand side. In the following example, `x` is the formal parameter name and
`constr` is its :ref:`syntactic class`. `print` and `of_constr` are
functions provided by Coq through `Message.v`.
+ .. flag:: Ltac2 Typed Notations
+
+ By default Ltac2 notations are typechecked at declaration time.
+ This assigns an expected type to notation arguments.
+
+ When a notation is declared with this flag unset, it is not
+ typechecked at declaration time and its expansion is typechecked
+ when it is used. This may allow slightly more flexible use of
+ the notation arguments at the cost of worse error messages when
+ incorrectly using the notation. It is not believed to be useful
+ in practice, please report any real use cases you find.
+
.. todo "print" doesn't seem to pay attention to "Set Printing All"
.. example:: Printing a :n:`@term`