Ltac2 #[abstract] attribute for types

Fix coq#18656

Printing of glb_expr is a bit awkward. We don't have access to the
type so we don't know when we cross an abstraction barrier. OTOH
constructors and projections are not in the environment / nametab so
we still print <abstr> in some places.

The attribute is disabled for open types as the naive implementation
produces not necessarily expected results.

doc/changelog/06-Ltac2-language/18766-ltac2-abstract-type.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  :attr:`abstract` for :cmd:`Ltac2 Type` makes it possible to turn types abstract at the end of a module
+  (`#18766 <https://github.com/coq/coq/pull/18766>`_,
+  fixes `#18656 <https://github.com/coq/coq/issues/18656>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proof-engine/ltac2.rst

@@ -192,6 +192,28 @@ One can define new types with the following commands.
    Records are product types with named fields and eliminated by projection.
    Likewise they can be recursive if the `rec` flag is set.
 
+.. attr:: abstract
+   :name: abstract
+
+   Types declared with this attribute are made abstract at the end of
+   the current module. This makes it possible to enforce invariants.
+
+   .. example::
+
+      .. coqtop:: in
+
+         Module PositiveInt.
+           #[abstract] Ltac2 Type t := int.
+
+           Ltac2 make (x:int) : t := if Int.le 0 x then x else Control.throw (Invalid_argument None).
+           Ltac2 get (x:t) : int := x.
+         End PositiveInt.
+
+      .. coqtop:: all
+
+         Ltac2 Eval PositiveInt.get (PositiveInt.make 3).
+         Fail Ltac2 Eval PositiveInt.get (PositiveInt.make -1).
+
 .. cmd:: Ltac2 @ external @ident : @ltac2_type := @string__plugin @string__function
    :name: Ltac2 external
 

plugins/ltac2/tac2entries.ml

@@ -109,6 +109,7 @@ let inTacDef : Id.t -> tacdef -> obj =
 
 type typdef = {
   typdef_local : bool;
+  typdef_abstract : bool;
   typdef_expr : glb_quant_typedef;
 }
 
@@ -188,8 +189,10 @@ let define_typedef kn (params, def as qdef) = match def with
   Tac2env.define_type kn qdef
 
 let perform_typdef vs ((sp, kn), def) =
-  let () = if not def.typdef_local then push_typedef vs sp kn def.typdef_expr in
-  define_typedef kn def.typdef_expr
+  let expr = def.typdef_expr in
+  let expr = if def.typdef_abstract then fst expr, GTydDef None else expr in
+  let () = if not def.typdef_local then push_typedef vs sp kn expr in
+  define_typedef kn expr
 
 let load_typdef i obj = perform_typdef (Until i) obj
 let open_typdef i obj = perform_typdef (Exactly i) obj
@@ -381,7 +384,7 @@ let qualid_to_ident qid =
   if qualid_is_ident qid then CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid
   else user_err ?loc:qid.CAst.loc (str "Identifier expected")
 
-let register_typedef ?(local = false) isrec types =
+let register_typedef ?(local = false) ?(abstract=false) isrec types =
   let same_name ({v=id1}, _) ({v=id2}, _) = Id.equal id1 id2 in
   let () = match List.duplicates same_name types with
   | [] -> ()
@@ -445,7 +448,13 @@ let register_typedef ?(local = false) isrec types =
     | CTydOpn ->
       if isrec then
         user_err ?loc (str "The open type declaration " ++ Id.print id ++
-          str " cannot be recursive")
+                       str " cannot be recursive");
+      if abstract then
+        (* Naive implementation allows to use and match on already
+           existing constructors but not declare new ones outside the
+           type's origin module. Not sure that's what we want so
+           forbid it for now. *)
+        user_err ?loc (str "Open types currently do not support #[abstract].")
   in
   let () = List.iter check types in
   let self =
@@ -459,6 +468,7 @@ let register_typedef ?(local = false) isrec types =
   let map ({v=id}, def) =
     let typdef = {
       typdef_local = local;
+      typdef_abstract = abstract;
       typdef_expr = intern_typedef self def;
     } in
     (id, typdef)
@@ -543,9 +553,12 @@ let register_open ?(local = false) qid (params, def) =
   | CTydRec _ | CTydDef _ ->
     user_err ?loc:qid.CAst.loc (str "Extensions only accept inductive constructors")
 
-let register_type ?local isrec types = match types with
+let register_type ?local ?abstract isrec types = match types with
 | [qid, true, def] ->
-  let () = if isrec then user_err ?loc:qid.CAst.loc (str "Extensions cannot be recursive") in
+  let () = if isrec then user_err ?loc:qid.CAst.loc (str "Extensions cannot be recursive.") in
+  let () = if Option.default false abstract
+    then user_err ?loc:qid.loc (str "Extensions cannot be abstract.")
+  in
   register_open ?local qid def
 | _ ->
   let map (qid, redef, def) =
@@ -555,7 +568,7 @@ let register_type ?local isrec types = match types with
     (qualid_to_ident qid, def)
   in
   let types = List.map map types in
-  register_typedef ?local isrec types
+  register_typedef ?local ?abstract isrec types
 
 (** Parsing *)
 
@@ -957,15 +970,17 @@ let check_modtype what =
   if Lib.is_modtype ()
   then warn_modtype what
 
+let abstract_att = Attributes.bool_attribute ~name:"abstract"
+
 let register_struct atts str = match str with
 | StrVal (mut, isrec, e) ->
   check_modtype "definitions";
   let deprecation, local = Attributes.(parse Notations.(deprecation ++ locality)) atts in
   register_ltac ?deprecation ?local ~mut isrec e
 | StrTyp (isrec, t) ->
   check_modtype "types";
-  let local = Attributes.(parse locality) atts in
-  register_type ?local isrec t
+  let local, abstract = Attributes.(parse Notations.(locality ++ abstract_att)) atts in
+  register_type ?local ?abstract isrec t
 | StrPrm (id, t, ml) ->
   check_modtype "externals";
   let deprecation, local = Attributes.(parse Notations.(deprecation ++ locality)) atts in
@@ -1243,13 +1258,14 @@ let register_prim_alg name params def =
     galg_nnonconst = nnonconst;
   } in
   let def = (params, GTydAlg alg) in
-  let def = { typdef_local = false; typdef_expr = def } in
+  let def = { typdef_local = false; typdef_abstract = false; typdef_expr = def } in
   Lib.add_leaf (inTypDef id def)
 
 let coq_def n = KerName.make Tac2env.coq_prefix (Label.make n)
 
 let def_unit = {
   typdef_local = false;
+  typdef_abstract = false;
   typdef_expr = 0, GTydDef (Some (GTypRef (Tuple 0, [])));
 }
 

plugins/ltac2/tac2entries.mli

@@ -17,7 +17,7 @@ open Tac2expr
 val register_ltac : ?deprecation:Deprecation.t -> ?local:bool -> ?mut:bool -> rec_flag ->
   (Names.lname * raw_tacexpr) list -> unit
 
-val register_type : ?local:bool -> rec_flag ->
+val register_type : ?local:bool -> ?abstract:bool -> rec_flag ->
   (qualid * redef_flag * raw_quant_typedef) list -> unit
 
 val register_primitive : ?deprecation:Deprecation.t -> ?local:bool ->

plugins/ltac2/tac2print.ml

@@ -181,27 +181,28 @@ let pr_factorized_constructor pr_rec lvl tpe = function
   | Other (n,cl) ->
   let _, data = Tac2env.interp_type tpe in
   match data with
-    | GTydAlg def ->
-      let paren = match lvl with
-        | E0 ->
-          if List.is_empty cl then fun x -> x else paren
-        | E1 | E2 | E3 | E4 | E5 -> fun x -> x
-      in
-      let cstr = pr_internal_constructor tpe n (List.is_empty cl) in
-      let cl = match cl with
-        | [] -> mt ()
-        | _ -> spc () ++ pr_sequence (pr_rec E0) cl
-      in
-      paren (hov 2 (cstr ++ cl))
-    | GTydRec def ->
-      let args = List.combine def cl in
-      let pr_arg ((id, _, _), arg) =
-        let kn = change_kn_label tpe id in
-        pr_projection kn ++ spc () ++ str ":=" ++ spc () ++ pr_rec E1 arg
-      in
-      let args = prlist_with_sep pr_semicolon pr_arg args in
-      hv 0 (str "{" ++ spc () ++ args ++ spc () ++ str "}")
-    | (GTydDef _ | GTydOpn) -> assert false
+  | GTydDef None -> str "<abstr>"
+  | GTydAlg def ->
+    let paren = match lvl with
+      | E0 ->
+        if List.is_empty cl then fun x -> x else paren
+      | E1 | E2 | E3 | E4 | E5 -> fun x -> x
+    in
+    let cstr = pr_internal_constructor tpe n (List.is_empty cl) in
+    let cl = match cl with
+      | [] -> mt ()
+      | _ -> spc () ++ pr_sequence (pr_rec E0) cl
+    in
+    paren (hov 2 (cstr ++ cl))
+  | GTydRec def ->
+    let args = List.combine def cl in
+    let pr_arg ((id, _, _), arg) =
+      let kn = change_kn_label tpe id in
+      pr_projection kn ++ spc () ++ str ":=" ++ spc () ++ pr_rec E1 arg
+    in
+    let args = prlist_with_sep pr_semicolon pr_arg args in
+    hv 0 (str "{" ++ spc () ++ args ++ spc () ++ str "}")
+  | (GTydDef _ | GTydOpn) -> assert false
 
 let pr_partial_pat_gen =
   let open PartialPat in
@@ -325,23 +326,24 @@ let pr_glbexpr_gen lvl ~avoid c =
     let e = pr_glbexpr E5 avoid e in
     let br = match info with
     | Other kn ->
-      let def = match Tac2env.interp_type kn with
-      | _, GTydAlg { galg_constructors = def } -> def
+      begin match Tac2env.interp_type kn with
+      | _, GTydDef None -> str "<abstr>"
       | _, GTydDef _ | _, GTydRec _ | _, GTydOpn -> assert false
-      in
-      let br = order_branches cst_br ncst_br def in
-      let pr_branch (cstr, vars, p) =
-        let cstr = change_kn_label kn cstr in
-        let cstr = pr_constructor cstr in
-        let avoid = List.fold_left Termops.add_vname avoid vars in
-        let vars = match vars with
-        | [] -> mt ()
-        | _ -> spc () ++ pr_sequence pr_name vars
+      | _, GTydAlg { galg_constructors = def } ->
+        let br = order_branches cst_br ncst_br def in
+        let pr_branch (cstr, vars, p) =
+          let cstr = change_kn_label kn cstr in
+          let cstr = pr_constructor cstr in
+          let avoid = List.fold_left Termops.add_vname avoid vars in
+          let vars = match vars with
+            | [] -> mt ()
+            | _ -> spc () ++ pr_sequence pr_name vars
+          in
+          hov 4 (str "|" ++ spc () ++ hov 0 (cstr ++ vars ++ spc () ++ str "=>") ++ spc () ++
+                 hov 2 (pr_glbexpr E5 avoid p)) ++ spc ()
         in
-        hov 4 (str "|" ++ spc () ++ hov 0 (cstr ++ vars ++ spc () ++ str "=>") ++ spc () ++
-          hov 2 (pr_glbexpr E5 avoid p)) ++ spc ()
-      in
-      prlist pr_branch br
+        prlist pr_branch br
+      end
     | Tuple n ->
       let (vars, p) = if Int.equal n 0 then ([||], cst_br.(0)) else ncst_br.(0) in
       let avoid = Array.fold_left Termops.add_vname avoid vars in
@@ -385,26 +387,28 @@ let pr_glbexpr_gen lvl ~avoid c =
     let brs = prlist_with_sep spc pr_one_branch brs in
     v 0 (hv 0 (str "match" ++ spc () ++ e ++ spc () ++ str "with") ++ spc () ++ brs ++ spc() ++ str "end")
   | GTacPrj (kn, e, n) ->
-    let def = match Tac2env.interp_type kn with
-    | _, GTydRec def -> def
+    begin  match Tac2env.interp_type kn with
+    | _, GTydDef None -> str "<abstr>"
     | _, GTydDef _ | _, GTydAlg _ | _, GTydOpn -> assert false
-    in
-    let (proj, _, _) = List.nth def n in
-    let proj = change_kn_label kn proj in
-    let proj = pr_projection proj in
-    let e = pr_glbexpr E0 avoid e in
-    hov 0 (e ++ str "." ++ paren proj)
+    | _, GTydRec def ->
+      let (proj, _, _) = List.nth def n in
+      let proj = change_kn_label kn proj in
+      let proj = pr_projection proj in
+      let e = pr_glbexpr E0 avoid e in
+      hov 0 (e ++ str "." ++ paren proj)
+    end
   | GTacSet (kn, e, n, r) ->
-    let def = match Tac2env.interp_type kn with
-    | _, GTydRec def -> def
+    begin match Tac2env.interp_type kn with
+    | _, GTydDef None -> str "<abstr>"
     | _, GTydDef _ | _, GTydAlg _ | _, GTydOpn -> assert false
-    in
-    let (proj, _, _) = List.nth def n in
-    let proj = change_kn_label kn proj in
-    let proj = pr_projection proj in
-    let e = pr_glbexpr E0 avoid e in
-    let r = pr_glbexpr E1 avoid r in
-    hov 0 (e ++ str "." ++ paren proj ++ spc () ++ str ":=" ++ spc () ++ r)
+    | _, GTydRec def ->
+      let (proj, _, _) = List.nth def n in
+      let proj = change_kn_label kn proj in
+      let proj = pr_projection proj in
+      let e = pr_glbexpr E0 avoid e in
+      let r = pr_glbexpr E1 avoid r in
+      hov 0 (e ++ str "." ++ paren proj ++ spc () ++ str ":=" ++ spc () ++ r)
+    end
   | GTacOpn (kn, cl) ->
     let paren = match lvl with
     | E0 -> paren

test-suite/output/ltac2_abstract.out

@@ -0,0 +1,56 @@
+File "./output/ltac2_abstract.v", line 20, characters 27-28:
+The command has indeed failed with message:
+This expression has type int but an expression was expected of type 
+M.t
+- : M.t = <abstr>
+File "./output/ltac2_abstract.v", line 28, characters 27-28:
+The command has indeed failed with message:
+This expression has type int but an expression was expected of type 
+t
+- : int = 2
+Ltac2 foo : t -> t
+      foo := fun x => Int.add x 1
+Ltac2 three : t
+      three := 3
+- : t = <abstr>
+File "./output/ltac2_abstract.v", line 47, characters 18-21:
+The command has indeed failed with message:
+Unbound constructor M.A
+File "./output/ltac2_abstract.v", line 49, characters 40-43:
+The command has indeed failed with message:
+Unbound constructor M.A
+- : M.t = <abstr>
+- : bool = false
+Ltac2 M.a : M.t
+      M.a := <abstr>
+Ltac2 M.is_b : M.t -> bool
+      M.is_b := fun x => match x with
+                         <abstr>
+                         end
+Ltac2 M.get_b : int -> M.t -> int
+      M.get_b := fun def x => match x with
+                              | <abstr> => x
+                              | _ => def
+                              end
+- : int M.t = <abstr>
+File "./output/ltac2_abstract.v", line 73, characters 20-21:
+The command has indeed failed with message:
+p is not a projection
+File "./output/ltac2_abstract.v", line 75, characters 30-31:
+The command has indeed failed with message:
+p is not a projection
+- : int t = <abstr>
+- : int = 42
+File "./output/ltac2_abstract.v", line 81, characters 27-40:
+The command has indeed failed with message:
+This expression has type bool but an expression was expected of type 
+int
+Ltac2 make : 'a -> 'a t
+      make := fun x => <abstr>
+Ltac2 p : 'a t -> 'a
+      p := fun x => <abstr>
+Ltac2 set : 'a t -> 'a -> unit
+      set := fun x v => <abstr>
+File "./output/ltac2_abstract.v", line 91, characters 32-33:
+The command has indeed failed with message:
+Open types currently do not support #[abstract].