Allow Ltac2 Globalize to accept CTacExt (bit hacky)

plugins/ltac2/tac2core.ml

@@ -1516,25 +1516,29 @@ let () =
   let intern = intern_constr in
   let interp ist c = interp_constr constr_flags ist c in
   let print env sigma c = str "constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in
+  let raw_print env sigma c = str "constr:(" ++ Ppconstr.pr_constr_expr env sigma c ++ str ")" in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
   let obj = {
     ml_intern = intern;
     ml_subst = subst;
     ml_interp = interp;
     ml_print = print;
+    ml_raw_print = raw_print;
   } in
   define_ml_object Tac2quote.wit_constr obj
 
 let () =
   let intern = intern_constr in
   let interp ist c = interp_constr open_constr_no_classes_flags ist c in
   let print env sigma c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in
+  let raw_print env sigma c = str "open_constr:(" ++ Ppconstr.pr_constr_expr env sigma c ++ str ")" in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
   let obj = {
     ml_intern = intern;
     ml_subst = subst;
     ml_interp = interp;
     ml_print = print;
+    ml_raw_print = raw_print;
   } in
   define_ml_object Tac2quote.wit_open_constr obj
 
@@ -1546,6 +1550,7 @@ let () =
     ml_interp = interp;
     ml_subst = (fun _ id -> id);
     ml_print = print;
+    ml_raw_print = print;
   } in
   define_ml_object Tac2quote.wit_ident obj
 
@@ -1563,12 +1568,14 @@ let () =
     Patternops.subst_pattern env sigma subst c
   in
   let print env sigma pat = str "pat:(" ++ Printer.pr_lconstr_pattern_env env sigma pat ++ str ")" in
+  let raw_print env sigma pat = str "pat:(" ++ Ppconstr.pr_constr_pattern_expr env sigma pat ++ str ")" in
   let interp _ c = return (Value.of_pattern c) in
   let obj = {
     ml_intern = intern;
     ml_interp = interp;
     ml_subst = subst;
     ml_print = print;
+    ml_raw_print = raw_print;
   } in
   define_ml_object Tac2quote.wit_pattern obj
 
@@ -1603,11 +1610,13 @@ let () =
     in
     str "preterm:(" ++ ppids ++ Printer.pr_lglob_constr_env env sigma c ++ str ")"
   in
+  let raw_print env sigma c = str "preterm:(" ++ Ppconstr.pr_constr_expr env sigma c ++ str ")" in
   let obj = {
     ml_intern = intern;
     ml_interp = interp;
     ml_subst = subst;
     ml_print = print;
+    ml_raw_print = raw_print;
   } in
   define_ml_object Tac2quote.wit_preterm obj
 
@@ -1630,11 +1639,16 @@ let () =
   | GlobRef.VarRef id -> str "reference:(" ++ str "&" ++ Id.print id ++ str ")"
   | r -> str "reference:(" ++ Printer.pr_global r ++ str ")"
   in
+  let raw_print _ _ r = match r.CAst.v with
+    | Tac2qexpr.QReference qid -> str "reference:(" ++ Libnames.pr_qualid qid ++ str ")"
+    | Tac2qexpr.QHypothesis id -> str "reference:(&" ++ Id.print id ++ str ")"
+  in
   let obj = {
     ml_intern = intern;
     ml_subst = subst;
     ml_interp = interp;
     ml_print = print;
+    ml_raw_print = raw_print;
   } in
   define_ml_object Tac2quote.wit_reference obj
 
@@ -1680,11 +1694,19 @@ let () =
     in
     str "ltac1:(" ++ ids ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
   in
+  let raw_print env sigma (ids, tac) =
+    let ids =
+      if List.is_empty ids then mt ()
+      else pr_sequence (fun id -> Id.print id.CAst.v) ids ++ spc () ++ str "|-" ++ spc ()
+    in
+    str "ltac1:(" ++ ids ++ Ltac_plugin.Pptactic.pr_raw_tactic env sigma tac ++ str ")"
+  in
   let obj = {
     ml_intern = intern;
     ml_subst = subst;
     ml_interp = interp;
     ml_print = print;
+    ml_raw_print = raw_print;
   } in
   define_ml_object Tac2quote.wit_ltac1 obj
 
@@ -1729,11 +1751,19 @@ let () =
     in
     str "ltac1val:(" ++ ids++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
   in
+  let raw_print env sigma (ids, tac) =
+    let ids =
+      if List.is_empty ids then mt ()
+      else pr_sequence (fun id -> Id.print id.CAst.v) ids ++ spc () ++ str "|-" ++ spc ()
+    in
+    str "ltac1val:(" ++ ids ++ Ltac_plugin.Pptactic.pr_raw_tactic env sigma tac ++ str ")"
+  in
   let obj = {
     ml_intern = intern;
     ml_subst = subst;
     ml_interp = interp;
     ml_print = print;
+    ml_raw_print = raw_print;
   } in
   define_ml_object Tac2quote.wit_ltac1val obj
 
@@ -1981,7 +2011,11 @@ let () =
   Genprint.register_print0 wit_ltac2in1 pr_raw pr_glb pr_top
 
 let () =
-  let pr_raw _ = Genprint.PrinterBasic (fun _env _sigma -> assert false) in
+  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 =
       let ids = Id.Set.elements ids in

plugins/ltac2/tac2entries.ml

@@ -1135,7 +1135,7 @@ let typecheck_expr e =
 
 let globalize_expr e =
   let avoid = Id.Set.empty in
-  let e = Tac2intern.globalize avoid e in
+  let e = Tac2intern.debug_globalize_allow_ext avoid e in
   Feedback.msg_notice (Tac2print.pr_rawexpr_gen E5 ~avoid e)
 
 (** Calling tactics *)

plugins/ltac2/tac2env.ml

@@ -286,6 +286,7 @@ type ('a, 'b) ml_object = {
   ml_subst : Mod_subst.substitution -> 'b -> 'b;
   ml_interp : environment -> 'b -> valexpr Proofview.tactic;
   ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
+  ml_raw_print : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
 }
 
 module MLTypeObj =

plugins/ltac2/tac2env.mli

@@ -144,6 +144,7 @@ type ('a, 'b) ml_object = {
   ml_subst : Mod_subst.substitution -> 'b -> 'b;
   ml_interp : environment -> 'b -> valexpr Proofview.tactic;
   ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
+  ml_raw_print : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
 }
 
 val define_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object -> unit

plugins/ltac2/tac2intern.ml

@@ -1512,111 +1512,126 @@ let get_projection0 var = match var with
   kn
 | AbsKn kn -> kn
 
-let rec globalize ids ({loc;v=er} as e) = match er with
-| CTacAtm _ -> e
-| CTacRef ref ->
-  let mem id = Id.Set.mem id ids in
-  begin match get_variable0 mem ref with
-  | ArgVar _ -> e
-  | ArgArg kn ->
-    let () = check_deprecated_ltac2 ?loc ref kn in
-    CAst.make ?loc @@ CTacRef (AbsKn kn)
-  end
-| CTacCst qid ->
-  let knc = get_constructor () qid in
-  CAst.make ?loc @@ CTacCst (AbsKn knc)
-| CTacFun (bnd, e) ->
-  let fold (pats, accu) pat =
-    let accu = ids_of_pattern accu pat in
-    let pat = globalize_pattern ids pat in
-    (pat :: pats, accu)
-  in
-  let bnd, ids = List.fold_left fold ([], ids) bnd in
-  let bnd = List.rev bnd in
-  let e = globalize ids e in
-  CAst.make ?loc @@ CTacFun (bnd, e)
-| CTacApp (e, el) ->
-  let e = globalize ids e in
-  let el = List.map (fun e -> globalize ids e) el in
-  CAst.make ?loc @@ CTacApp (e, el)
-| CTacLet (isrec, bnd, e) ->
-  let fold accu (pat, _) = ids_of_pattern accu pat in
-  let ext = List.fold_left fold Id.Set.empty bnd in
-  let eids = Id.Set.union ext ids in
-  let e = globalize eids e in
-  let map (qid, e) =
-    let ids = if isrec then eids else ids in
-    let qid = globalize_pattern ids qid in
-    (qid, globalize ids e)
-  in
-  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 v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
-  globalize ids v
-| CTacCnv (e, t) ->
-  let e = globalize ids e in
-  CAst.make ?loc @@ CTacCnv (e, t)
-| CTacSeq (e1, e2) ->
-  let e1 = globalize ids e1 in
-  let e2 = globalize ids e2 in
-  CAst.make ?loc @@ CTacSeq (e1, e2)
-| CTacIft (e, e1, e2) ->
-  let e = globalize ids e in
-  let e1 = globalize ids e1 in
-  let e2 = globalize ids e2 in
-  CAst.make ?loc @@ CTacIft (e, e1, e2)
-| CTacCse (e, bl) ->
-  let e = globalize ids e in
-  let bl = List.map (fun b -> globalize_case ids b) bl in
-  CAst.make ?loc @@ CTacCse (e, bl)
-| CTacRec (def, r) ->
-  let def = Option.map (globalize ids) def in
-  let map (p, e) =
-    let p = get_projection0 p in
-    let e = globalize ids e in
-    (AbsKn p, e)
-  in
-  CAst.make ?loc @@ CTacRec (def, List.map map r)
-| CTacPrj (e, p) ->
-  let e = globalize ids e in
-  let p = get_projection0 p in
-  CAst.make ?loc @@ CTacPrj (e, AbsKn p)
-| CTacSet (e, p, e') ->
-  let e = globalize ids e in
-  let p = get_projection0 p in
-  let e' = globalize ids e' in
-  CAst.make ?loc @@ CTacSet (e, AbsKn p, e')
-| CTacExt (tag, arg) ->
-  let arg = str (Tac2dyn.Arg.repr tag) in
-  CErrors.user_err ?loc (str "Cannot globalize generic arguments of type" ++ spc () ++ arg)
+type raw_ext = RawExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_ext
+
+let globalize_gen ~tacext ids tac =
+  let rec globalize ids ({loc;v=er} as e) = match er with
+    | CTacAtm _ -> e
+    | CTacRef ref ->
+      let mem id = Id.Set.mem id ids in
+      begin match get_variable0 mem ref with
+      | ArgVar _ -> e
+      | ArgArg kn ->
+        let () = check_deprecated_ltac2 ?loc ref kn in
+        CAst.make ?loc @@ CTacRef (AbsKn kn)
+      end
+    | CTacCst qid ->
+      let knc = get_constructor () qid in
+      CAst.make ?loc @@ CTacCst (AbsKn knc)
+    | CTacFun (bnd, e) ->
+      let fold (pats, accu) pat =
+        let accu = ids_of_pattern accu pat in
+        let pat = globalize_pattern ids pat in
+        (pat :: pats, accu)
+      in
+      let bnd, ids = List.fold_left fold ([], ids) bnd in
+      let bnd = List.rev bnd in
+      let e = globalize ids e in
+      CAst.make ?loc @@ CTacFun (bnd, e)
+    | CTacApp (e, el) ->
+      let e = globalize ids e in
+      let el = List.map (fun e -> globalize ids e) el in
+      CAst.make ?loc @@ CTacApp (e, el)
+    | CTacLet (isrec, bnd, e) ->
+      let fold accu (pat, _) = ids_of_pattern accu pat in
+      let ext = List.fold_left fold Id.Set.empty bnd in
+      let eids = Id.Set.union ext ids in
+      let e = globalize eids e in
+      let map (qid, e) =
+        let ids = if isrec then eids else ids in
+        let qid = globalize_pattern ids qid in
+        (qid, globalize ids e)
+      in
+      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 v = if CList.is_empty el then body else CAst.make ?loc @@ CTacLet(false, el, body) in
+      globalize ids v
+    | CTacCnv (e, t) ->
+      let e = globalize ids e in
+      CAst.make ?loc @@ CTacCnv (e, t)
+    | CTacSeq (e1, e2) ->
+      let e1 = globalize ids e1 in
+      let e2 = globalize ids e2 in
+      CAst.make ?loc @@ CTacSeq (e1, e2)
+    | CTacIft (e, e1, e2) ->
+      let e = globalize ids e in
+      let e1 = globalize ids e1 in
+      let e2 = globalize ids e2 in
+      CAst.make ?loc @@ CTacIft (e, e1, e2)
+    | CTacCse (e, bl) ->
+      let e = globalize ids e in
+      let bl = List.map (fun b -> globalize_case ids b) bl in
+      CAst.make ?loc @@ CTacCse (e, bl)
+    | CTacRec (def, r) ->
+      let def = Option.map (globalize ids) def in
+      let map (p, e) =
+        let p = get_projection0 p in
+        let e = globalize ids e in
+        (AbsKn p, e)
+      in
+      CAst.make ?loc @@ CTacRec (def, List.map map r)
+    | CTacPrj (e, p) ->
+      let e = globalize ids e in
+      let p = get_projection0 p in
+      CAst.make ?loc @@ CTacPrj (e, AbsKn p)
+    | CTacSet (e, p, e') ->
+      let e = globalize ids e in
+      let p = get_projection0 p in
+      let e' = globalize ids e' in
+      CAst.make ?loc @@ CTacSet (e, AbsKn p, e')
+    | CTacExt (tag, arg) -> tacext ?loc (RawExt (tag, arg))
+
+  and globalize_case ids (p, e) =
+    (globalize_pattern ids p, globalize ids e)
+
+  and globalize_pattern ids ({loc;v=pr} as p) = match pr with
+    | CPatVar _ | CPatAtm _ -> p
+    | CPatRef (cst, pl) ->
+      let knc = get_constructor () cst in
+      let cst = AbsKn knc in
+      let pl = List.map (fun p -> globalize_pattern ids p) pl in
+      CAst.make ?loc @@ CPatRef (cst, pl)
+    | CPatCnv (pat, ty) ->
+      let pat = globalize_pattern ids pat in
+      CAst.make ?loc @@ CPatCnv (pat, ty)
+    | CPatOr pl ->
+      let pl = List.map (fun p -> globalize_pattern ids p) pl in
+      CAst.make ?loc @@ CPatOr pl
+    | CPatAs (p,x) ->
+      CAst.make ?loc @@ CPatAs (globalize_pattern ids p, x)
+    | CPatRecord pats ->
+      let map (p, e) =
+        let p = get_projection0 p in
+        let e = globalize_pattern ids e in
+        (AbsKn p, e)
+      in
+      CAst.make ?loc @@ CPatRecord (List.map map pats)
 
-and globalize_case ids (p, e) =
-  (globalize_pattern ids p, globalize ids e)
+  in
+  globalize ids tac
 
-and globalize_pattern ids ({loc;v=pr} as p) = match pr with
-| CPatVar _ | CPatAtm _ -> p
-| CPatRef (cst, pl) ->
-  let knc = get_constructor () cst in
-  let cst = AbsKn knc in
-  let pl = List.map (fun p -> globalize_pattern ids p) pl in
-  CAst.make ?loc @@ CPatRef (cst, pl)
-| CPatCnv (pat, ty) ->
-  let pat = globalize_pattern ids pat in
-  CAst.make ?loc @@ CPatCnv (pat, ty)
-| CPatOr pl ->
-  let pl = List.map (fun p -> globalize_pattern ids p) pl in
-  CAst.make ?loc @@ CPatOr pl
-| CPatAs (p,x) ->
-  CAst.make ?loc @@ CPatAs (globalize_pattern ids p, x)
-| CPatRecord pats ->
-  let map (p, e) =
-    let p = get_projection0 p in
-    let e = globalize_pattern ids e in
-    (AbsKn p, e)
-  in
-  CAst.make ?loc @@ CPatRecord (List.map map pats)
+let globalize ids tac =
+  let tacext ?loc (RawExt (tag,_)) =
+    let arg = str (Tac2dyn.Arg.repr tag) in
+    CErrors.user_err ?loc (str "Cannot globalize generic arguments of type" ++ spc () ++ arg)
+  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
 
 (** Kernel substitution *)