Typecheck ignoring errors instead of globalize for Ltac2 Globalize

This adds a mode to ltac2 typechecking which accumulates errors
instead of raising an exception at the first error.

Ltac2 Globalize then uses this mode and ignores the accumulated errors
(we could print them instead).

The accumulation mode could also be used to provide all errors from an
ltac2 expression in regular code in the future (with a flag).

Together with #21617 this gets us closer to removing the globalize
code (which doesn't work on quotations so should be avoided).

Author: SkySkimmer

plugins/ltac2/tac2entries.ml

@@ -1599,8 +1599,9 @@ let typecheck_expr e =
 
 let globalize_expr e =
   let avoid = Id.Set.empty in
-  let e = Tac2intern.debug_globalize_allow_ext avoid e in
-  Feedback.msg_notice (Tac2print.pr_rawexpr_gen E5 ~avoid e)
+  let e, t, errors = Tac2intern.intern_accumulate_errors ~strict:false [] e in
+  (* XXX print type and errors? *)
+  Feedback.msg_notice (Tac2print.pr_glbexpr_gen E5 ~avoid e)
 
 (** Calling tactics *)
 

plugins/ltac2/tac2extravals.ml

@@ -418,7 +418,6 @@ let () =
   let pr_raw e = Genprint.PrinterBasic (fun _env _sigma ->
       let avoid = Id.Set.empty in
       (* FIXME avoid set, same as pr_glb *)
-      let e = Tac2intern.debug_globalize_allow_ext avoid e in
       Tac2print.pr_rawexpr_gen ~avoid E5 e) in
   let pr_glb (ids, e) =
     let ids =
@@ -438,7 +437,6 @@ let () =
 
 let () =
   let pr_raw e = Genprint.PrinterBasic (fun _ _ ->
-      let e = Tac2intern.debug_globalize_allow_ext Id.Set.empty e in
       Tac2print.pr_rawexpr_gen ~avoid:Id.Set.empty E5 e)
   in
   let pr_glb e = Genprint.PrinterBasic (fun _ _ -> Tac2print.pr_glbexpr ~avoid:Id.Set.empty e) in

plugins/ltac2/tac2intern.ml

@@ -1076,9 +1076,12 @@ let tycon_fun_body ?loc env tycon dom =
     let () = unify ?loc env (GTypArrow (dom,codom)) tycon in
     codom
   | GTypRef _ ->
-    CErrors.user_err ?loc
-      Pp.(str "This expression should not be a function, the expected type is" ++ spc() ++
-          pr_glbtype env tycon ++ str ".")
+    let () =
+      add_error env ?loc
+        Pp.(str "This expression should not be a function, the expected type is" ++ spc() ++
+            pr_glbtype env tycon ++ str ".")
+    in
+    GTypVar (fresh_id env)
 
 let tycon_app ?loc env ~ft t =
   match kind env t with
@@ -1093,14 +1096,16 @@ let tycon_app ?loc env ~ft t =
       | GTypArrow _ -> true
       | _ -> false
     in
-    if is_fun then
-      CErrors.user_err ?loc
+    let () = if is_fun then
+      add_error env ?loc
         Pp.(str "This function has type" ++ spc() ++ pr_glbtype env ft ++
             spc() ++ str "and is applied to too many arguments.")
     else
-      CErrors.user_err ?loc
+      add_error env ?loc
         Pp.(str "This expression has type" ++ spc() ++ pr_glbtype env ft ++ str"." ++
             spc() ++ str "It is not a function and cannot be applied.")
+    in
+    GTypVar (fresh_id env), GTypVar (fresh_id env)
 
 let warn_useless_record_with = CWarnings.create ~name:"ltac2-useless-record-with" ~default:AsError
     ~category:CWarnings.CoreCategories.ltac2
@@ -1521,29 +1526,32 @@ and intern_constructor env loc tycon kn args = match kn with
   else
     error_nargs_mismatch ?loc kn nargs (List.length args)
 | Tuple n ->
-  let () = if not (Int.equal n (List.length args)) then begin
-      if Int.equal 0 n then
-        (* parsing [() bla] produces [CTacApp (Tuple 0, [bla])] but parsing
-           [((), ()) bla] produces [CTacApp (CTacApp (Tuple 2, [(); ()]), [bla])]
-           so we only need to produce a sensible error for [Tuple 0] *)
-        let t = GTypRef (Tuple 0, []) in
-        CErrors.user_err ?loc Pp.(
-            str "This expression has type" ++ spc () ++ pr_glbtype env t ++
-            spc () ++ str "and is not a function")
-      else assert false
-    end
-  in
-  let types = List.init n (fun i -> GTypVar (fresh_id env)) in
-  let ans = GTypRef (Tuple n, types) in
-  let ans = match tycon with
-    | None -> ans
-    | Some tycon ->
-      let () = unify ?loc env ans tycon in
-      tycon
-  in
-  let map arg tpe = intern_rec_with_constraint env arg tpe in
-  let args = List.map2 map args types in
-  GTacCst (Tuple n, 0, args), ans
+  if not (Int.equal n (List.length args)) then begin
+    assert (Int.equal 0 n);
+    (* parsing [() bla] produces [CTacApp (Tuple 0, [bla])] but parsing
+         [((), ()) bla] produces [CTacApp (CTacApp (Tuple 2, [(); ()]), [bla])]
+         so we only need to produce a sensible error for [Tuple 0] *)
+    let t = GTypRef (Tuple 0, []) in
+    let () =
+      add_error env ?loc Pp.(
+        str "This expression has type" ++ spc () ++ pr_glbtype env t ++
+        spc () ++ str "and is not a function.")
+    in
+    let args = List.map (fun arg -> fst @@ intern_rec env None arg) args in
+    GTacApp (GTacCst (Tuple 0, 0, []), args), GTypVar (fresh_id env)
+  end
+  else
+    let types = List.init n (fun i -> GTypVar (fresh_id env)) in
+    let ans = GTypRef (Tuple n, types) in
+    let ans = match tycon with
+      | None -> ans
+      | Some tycon ->
+        let () = unify ?loc env ans tycon in
+        tycon
+    in
+    let map arg tpe = intern_rec_with_constraint env arg tpe in
+    let args = List.map2 map args types in
+    GTacCst (Tuple n, 0, args), ans
 
 and intern_case env loc e tycon pl =
   let e, et = intern_rec env None e in
@@ -1583,6 +1591,17 @@ let intern ~strict ctx e =
   let t = normalize env (count, vars) t in
   (e, (!count, t))
 
+let intern_accumulate_errors ~strict ctx e =
+  let env = empty_env ~strict ~accumulate_errors:true () in
+  (* XXX not doing check_unused_variables *)
+  let fold accu (id, t) = push_name (Name id) (polymorphic t) accu in
+  let env = List.fold_left fold env ctx in
+  let (e, t) = intern_rec env None e in
+  let count = ref 0 in
+  let vars = ref TVar.Map.empty in
+  let t = normalize env (count, vars) t in
+  (e, (!count, t), get_errors env)
+
 let intern_typedef self (ids, t) : glb_quant_typedef =
   let env = set_rec self (empty_env ()) in
   (* Initialize type parameters *)
@@ -1776,10 +1795,6 @@ let globalize ids tac =
   in
   globalize_gen ~tacext ids tac
 
-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:true ()

plugins/ltac2/tac2intern.mli

@@ -19,6 +19,9 @@ val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quan
 val intern_open_type : raw_typexpr -> type_scheme
 val intern_notation_data : Id.Set.t -> raw_tacexpr -> Tac2env.notation_data
 
+val intern_accumulate_errors : strict:bool -> context -> raw_tacexpr ->
+  glb_tacexpr * type_scheme * Pp.t Loc.located list
+
 (** [check_unused] is default true *)
 val genintern_warn_not_unit : ?check_unused:bool ->
   Genintern.glob_sign ->
@@ -66,10 +69,6 @@ val globalize : Id.Set.t -> raw_tacexpr -> raw_tacexpr
 (** Replaces all qualified identifiers by their corresponding kernel name. The
     set represents bound variables in the context. *)
 
-val debug_globalize_allow_ext : Id.Set.t -> raw_tacexpr -> raw_tacexpr
-(** Variant of globalize which can accept CTacExt using the provided function.
-    Intended for debugging. *)
-
 (** Errors *)
 
 val error_nargs_mismatch : ?loc:Loc.t -> ltac_constructor -> int -> int -> 'a

plugins/ltac2/tac2typing_env.ml

@@ -105,6 +105,9 @@ type mix_type_scheme = int * mix_var glb_typexpr
    so instead we use mutation to detect them *)
 type used = { mutable used : bool }
 
+(* TODO delay printing? but printing depends on env which is mutable *)
+type error = Pp.t Loc.located
+
 type t = {
   env_var : (mix_type_scheme * used) Id.Map.t;
   (** Type schemes of bound variables *)
@@ -118,17 +121,30 @@ type t = {
   (** Recursive type definitions *)
   env_strict : bool;
   (** True iff in strict mode *)
+  env_errs : error list ref option;
+  (** [None] if raise on first error, [Some] if accumulate errors *)
 }
 
-let empty_env ?(strict=true) () = {
+let empty_env ?(strict=true) ?(accumulate_errors=false) () = {
   env_var = Id.Map.empty;
   env_cst = UF.create ();
   env_als = ref Id.Map.empty;
   env_opn = true;
   env_rec = Id.Map.empty;
   env_strict = strict;
+  env_errs = if accumulate_errors then Some (ref []) else None;
 }
 
+let add_error ?loc env msg =
+  match env.env_errs with
+  | None -> CErrors.user_err ?loc msg
+  | Some errs -> errs := (loc,msg) :: !errs
+
+let get_errors env =
+  match env.env_errs with
+  | None -> assert false
+  | Some errs -> !errs
+
 let env_strict env = env.env_strict
 
 let set_rec self env = { env with env_rec = self }
@@ -328,7 +344,7 @@ let rec unify0 env t1 t2 = match kind env t1, kind env t2 with
 let unify ?loc env t1 t2 =
   try unify0 env t1 t2
   with CannotUnify (u1, u2) ->
-    CErrors.user_err ?loc Pp.(str "This expression has type" ++ spc () ++ pr_glbtype env t1 ++
+    add_error env ?loc Pp.(str "This expression has type" ++ spc () ++ pr_glbtype env t1 ++
       spc () ++ str "but an expression was expected of type" ++ spc () ++ pr_glbtype env t2)
 
 let unify_arrow ?loc env ft args =
@@ -343,12 +359,17 @@ let unify_arrow ?loc env ft args =
     let () = unify ?loc env (GTypVar id) (GTypArrow (t, ft)) in
     iter ft args true
   | GTypRef _, _ :: _ ->
-    if is_fun then
-      CErrors.user_err ?loc Pp.(str "This function has type" ++ spc () ++ pr_glbtype env ft0 ++
-        spc () ++ str "and is applied to too many arguments")
-    else
-      CErrors.user_err ?loc Pp.(str "This expression has type" ++ spc () ++ pr_glbtype env ft0 ++
-        spc () ++ str "and is not a function")
+    let () =
+      if is_fun then
+        add_error env ?loc
+          Pp.(str "This function has type" ++ spc () ++ pr_glbtype env ft0 ++
+              spc () ++ str "and is applied to too many arguments")
+      else
+        add_error env ?loc
+          Pp.(str "This expression has type" ++ spc () ++ pr_glbtype env ft0 ++
+              spc () ++ str "and is not a function")
+    in
+    GTypVar (fresh_id env)
   in
   iter ft args false
 

plugins/ltac2/tac2typing_env.mli

@@ -21,8 +21,14 @@ end
 
 type t
 
-(** default strict:true *)
-val empty_env : ?strict:bool -> unit -> t
+(** default strict:true, accumulate_errors:false *)
+val empty_env : ?strict:bool -> ?accumulate_errors:bool -> unit -> t
+
+(** In accumulate mode, add the error to the list in the env. Otherwise raise UserError. *)
+val add_error : ?loc:Loc.t -> t -> Pp.t -> unit
+
+(** Get accumulated errors. Assertion failure if not in accumulate mode. *)
+val get_errors : t -> Pp.t Loc.located list
 
 val set_rec : (KerName.t * int) Id.Map.t -> t -> t
 

test-suite/output/ltac2_check_globalize.out

@@ -16,25 +16,26 @@ let x := fun x => x in
 let _ := x 1 in
 let _ := x "" in
 () : unit
-let accu := { contents := []} in
-(let x := fun x => accu.(contents) := (x :: accu.(contents)) in
- let _ := x 1 in
- let _ := x "" in
- ());
+let accu := { contents := [] } in
+let _ :=
+  let x := fun x => accu.(contents) := (x :: accu.(contents)) in
+  let _ := x 1 in
+  let _ := x "" in
+  ()
+in
 accu.(contents)
 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 : '__α Pattern.goal_matching) :=
-  ([(([(None, (Pattern.MatchPattern, pat:(_)))],
+let m :=
+  [(([(None, (Pattern.MatchPattern, pat:(_)))],
       (Pattern.MatchPattern, pat:(_))),
      (fun h =>
       let h := Array.get h 0 in
       fun _ => fun _ => fun _ => fun _ => Std.clear h));
-     (([], (Pattern.MatchPattern, pat:(_))),
+    (([], (Pattern.MatchPattern, pat:(_))),
       (fun _ => fun _ => fun _ => fun _ => fun _ => ()))]
-    : _ Pattern.goal_matching)
 in
-Pattern.lazy_goal_match0 false m :'__α
+Pattern.lazy_goal_match0 false m
 constr:(ltac2:(()))

test-suite/output/ltac2_typed_notations.out

@@ -2,12 +2,10 @@ 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)
+fun b =>
+let c := b in
+let m :=
+  [(Pattern.MatchPattern, pat:(true), (fun _ => fun _ => true));
+    (Pattern.MatchPattern, pat:(false), (fun _ => fun _ => false))]
+with t := c in
+Pattern.one_match0 t m