Add Print Ltac2 Type

Close coq#16420

doc/sphinx/proof-engine/ltac2.rst

@@ -350,6 +350,10 @@ Printing Ltac2 tactics
    :cmd:`Print` can print defined Ltac2 tactics and can avoid printing
    other objects by using `Print Ltac2`.
 
+.. cmd:: Print Ltac2 Type @qualid
+
+   Prints the definitions of ltac2 types.
+
 .. cmd:: Ltac2 Globalize @ltac2_expr
 
    Prints the result of resolving notations in the given expression.

doc/tools/docgram/fullGrammar

@@ -690,6 +690,7 @@ command: [
 | "Ltac2" "Notation" ltac2def_syn      (* ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr6      (* ltac2 plugin *)
 | "Print" "Ltac2" reference      (* ltac2 plugin *)
+| "Print" "Ltac2" "Type" reference      (* ltac2 plugin *)
 | "Locate" "Ltac2" reference      (* ltac2 plugin *)
 | "Print" "Ltac2" "Signatures"      (* ltac2 plugin *)
 | "Ltac2" "Check" ltac2_expr6      (* ltac2 plugin *)

doc/tools/docgram/orderedGrammar

@@ -958,6 +958,7 @@ command: [
 | "Ltac2" "Notation" [ string | ident      (* ltac2 plugin *) ] ":=" ltac2_expr      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr      (* ltac2 plugin *)
 | "Print" "Ltac2" qualid      (* ltac2 plugin *)
+| "Print" "Ltac2" "Type" qualid      (* ltac2 plugin *)
 | "Locate" "Ltac2" qualid      (* ltac2 plugin *)
 | "Print" "Ltac2" "Signatures"      (* ltac2 plugin *)
 | "Ltac2" "Check" ltac2_expr      (* ltac2 plugin *)

plugins/ltac2/g_ltac2.mlg

@@ -1064,6 +1064,7 @@ open Stdarg
 
 VERNAC COMMAND EXTEND Ltac2Printers CLASSIFIED AS QUERY
 | [ "Print" "Ltac2" reference(tac) ] -> { Tac2entries.print_ltac2 tac }
+| [ "Print" "Ltac2" "Type" reference(tac) ] -> { Tac2entries.print_ltac2_type tac }
 | [ "Locate" "Ltac2" reference(r) ] -> { Tac2entries.print_located_tactic r }
 | [ "Print" "Ltac2" "Signatures" ] -> { Tac2entries.print_signatures () }
 | [ "Ltac2" "Check" ltac2_expr(e) ] -> { Tac2entries.typecheck_expr e }

plugins/ltac2/tac2entries.ml

@@ -1028,6 +1028,38 @@ let print_constant ~print_def qid ?info data =
     hov 2 (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype name t) ++ def ++ info
   )
 
+let print_type ~print_def qid kn =
+  let nparams, data = Tac2env.interp_type kn in
+  let name = int_name () in
+  let params = List.init nparams (fun i -> GTypVar i) in
+  let ty = match params with
+    | [] -> pr_qualid qid
+    | [t] -> pr_glbtype name t ++ spc() ++ pr_qualid qid
+    | _ -> surround (prlist_with_sep pr_comma (pr_glbtype name) params) ++ spc() ++ pr_qualid qid
+  in
+  let def = if not print_def || (match data with GTydDef None -> true | _ -> false)
+    then mt()
+    else spc() ++ str ":= " ++ match data with
+      | GTydDef None -> assert false
+      | GTydDef (Some t) -> pr_glbtype name t
+      | GTydAlg { galg_constructors = [] } -> str "[ ]"
+      | GTydAlg { galg_constructors = ctors } ->
+        let pr_ctor (id, argtys) =
+          hov 0
+            (Id.print id ++ if CList.is_empty argtys then mt()
+             else spc() ++surround (prlist_with_sep pr_comma (pr_glbtype name) argtys))
+        in
+        hv 0 (str "[ " ++ prlist_with_sep (fun () -> spc() ++ str "| ") pr_ctor ctors ++ str " ]")
+      | GTydRec fields ->
+        let pr_field (id, ismut, t) =
+          hov 0 ((if ismut then str "mutable " else mt()) ++ Id.print id
+                 ++ spc() ++ str ": " ++ pr_glbtype name t) ++ str ";"
+        in
+        hv 2 (str "{ " ++ prlist_with_sep spc pr_field fields ++ str " }")
+      | GTydOpn -> str "[ .. ]"
+  in
+  hov 2 (ty ++ def)
+
 let print_tacref ~print_def qid = function
   | TacConstant kn ->
     let data = Tac2env.interp_global kn in
@@ -1048,28 +1080,35 @@ let print_constructor qid kn =
 let locatable_ltac2 = "Ltac2"
 
 type ltac2_object =
+  | Type of type_constant
   | Constructor of ltac_constructor
   | TacRef of tacref
 
 let locate_object qid =
+  try Type (Tac2env.locate_type qid)
+  with Not_found ->
   try Constructor (Tac2env.locate_constructor qid)
   with Not_found ->
-    TacRef (Tac2env.locate_ltac qid)
+  TacRef (Tac2env.locate_ltac qid)
 
 let locate_all_object qid =
   let open Tac2env in
-  (List.map (fun x -> Constructor x) (locate_extended_all_constructor qid))
-   @ (List.map (fun x -> TacRef x) (locate_extended_all_ltac qid))
+  (List.map (fun x -> Type x) (locate_extended_all_type qid))
+  @ (List.map (fun x -> Constructor x) (locate_extended_all_constructor qid))
+  @ (List.map (fun x -> TacRef x) (locate_extended_all_ltac qid))
 
 let shortest_qualid_of_object = function
+  | Type kn -> Tac2env.shortest_qualid_of_type kn
   | Constructor kn -> Tac2env.shortest_qualid_of_constructor kn
   | TacRef kn -> Tac2env.shortest_qualid_of_ltac Id.Set.empty kn
 
 let path_of_object = function
+  | Type kn -> Tac2env.path_of_type kn
   | Constructor kn -> Tac2env.path_of_constructor kn
   | TacRef kn -> Tac2env.path_of_ltac kn
 
 let print_object ~print_def qid = function
+  | Type kn -> str "Ltac2 Type" ++ spc() ++ print_type ~print_def qid kn
   | Constructor kn -> str "Ltac2 constructor" ++ spc() ++ print_constructor qid kn
   | TacRef kn -> str "Ltac2 " ++ print_tacref ~print_def qid kn
 
@@ -1080,6 +1119,7 @@ let () =
   let shortest_qualid (_,kn) = shortest_qualid_of_object kn in
   let name (_,kn) =
     let hdr = match kn with
+      | Type _ -> str "Ltac2 Type"
       | TacRef (TacConstant _) -> str "Ltac2"
       | TacRef (TacAlias _) -> str "Ltac2 Notation"
       | Constructor _ -> str "Ltac2 Constructor"
@@ -1114,6 +1154,12 @@ let print_ltac2 qid =
     in
     Feedback.msg_notice (print_tacref ~print_def:true qid kn)
 
+let print_ltac2_type qid =
+  match Tac2env.locate_type qid with
+  | exception Not_found -> user_err ?loc:qid.CAst.loc (str "Unknown Ltac2 type " ++ pr_qualid qid)
+  | kn ->
+    Feedback.msg_notice (print_type ~print_def:true qid kn)
+
 let print_signatures () =
   let entries = KNmap.bindings (Tac2env.globals ()) in
   let sort (kn1, _) (kn2, _) = KerName.compare kn1 kn2 in

plugins/ltac2/tac2entries.mli

@@ -55,6 +55,9 @@ val print_located_tactic : Libnames.qualid -> unit
 val print_ltac2 : Libnames.qualid -> unit
 (** Display the definition of a tactic. *)
 
+val print_ltac2_type : Libnames.qualid -> unit
+(** Display the definition of a type. *)
+
 val print_signatures : unit -> unit
 (** Print types of all definitions in scope. *)
 

plugins/ltac2/tac2env.ml

@@ -247,6 +247,8 @@ let locate_extended_all_type qid =
   let tab = !nametab in
   KnTab.find_prefixes qid tab.tab_type
 
+let path_of_type kn = KNmap.find kn (!nametab).tab_type_rev
+
 let shortest_qualid_of_type ?loc kn =
   let tab = !nametab in
   let sp = KNmap.find kn tab.tab_type_rev in

plugins/ltac2/tac2env.mli

@@ -113,6 +113,7 @@ val push_type : visibility -> full_path -> type_constant -> unit
 val locate_type : qualid -> type_constant
 val locate_extended_all_type : qualid -> type_constant list
 val shortest_qualid_of_type : ?loc:Loc.t -> type_constant -> qualid
+val path_of_type : type_constant -> full_path
 
 val push_projection : visibility -> full_path -> ltac_projection -> unit
 val locate_projection : qualid -> ltac_projection

test-suite/output/ltac2_printabout.out

@@ -12,3 +12,14 @@ Triple : 'c -> 'b -> 'a -> ('a, 'b, 'c) triple
 Not_found : exn
 Out_of_bounds : message option -> exn
 Ltac2 Notation nota := () ()
+Ltac2 Type constr
+Ltac2 Type constr := Init.constr
+('a, 'b) thing := 'b option
+Ltac2 Type empty := [ ]
+'a option := [ None | Some ('a) ]
+bool := [ true | false ]
+Ltac2 Type ('a, 'b, 'c) triple := [ Triple ('c, 'b, 'a) ]
+Ltac2 Type 'a ref := { mutable contents : 'a; }
+Ltac2 Type
+('a, 'b, 'c) trirecord := { cproj : 'c; mutable bproj : 'b; aproj : 'a; }
+Ltac2 Type extensible := [ .. ]

test-suite/output/ltac2_printabout.v

@@ -34,3 +34,35 @@ Print Ltac2 Out_of_bounds.
 Ltac2 Notation nota := () ().
 
 Print nota.
+
+(* types *)
+
+Print constr.
+
+Ltac2 Type constr := constr.
+
+Print constr.
+
+Ltac2 Type ('a,'b) thing := 'b option.
+
+Print Ltac2 Type thing.
+
+Ltac2 Type empty := [].
+
+Print empty.
+
+Print Ltac2 Type option.
+
+Print Ltac2 Type bool.
+
+Print triple.
+
+Print ref.
+
+Ltac2 Type ('a,'b,'c) trirecord := { cproj : 'c; mutable bproj : 'b; aproj : 'a }.
+
+Print trirecord.
+
+Ltac2 Type extensible := [ .. ].
+
+Print extensible.