From 2670857539a660c0d946c832fd2a0485b0c282f9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 21 Feb 2024 14:10:02 +0100 Subject: [PATCH] Ltac2 #[abstract] attribute for types Fix #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 in some places. The attribute is disabled for open types as the naive implementation produces not necessarily expected results. --- .../18766-ltac2-abstract-type.rst | 5 + doc/sphinx/proof-engine/ltac2.rst | 22 ++++ plugins/ltac2/tac2entries.ml | 36 ++++-- plugins/ltac2/tac2entries.mli | 2 +- plugins/ltac2/tac2print.ml | 110 +++++++++--------- test-suite/output/ltac2_abstract.out | 56 +++++++++ test-suite/output/ltac2_abstract.v | 110 ++++++++++++++++++ 7 files changed, 277 insertions(+), 64 deletions(-) create mode 100644 doc/changelog/06-Ltac2-language/18766-ltac2-abstract-type.rst create mode 100644 test-suite/output/ltac2_abstract.out create mode 100644 test-suite/output/ltac2_abstract.v diff --git a/doc/changelog/06-Ltac2-language/18766-ltac2-abstract-type.rst b/doc/changelog/06-Ltac2-language/18766-ltac2-abstract-type.rst new file mode 100644 index 0000000000000..5a482667ad89a --- /dev/null +++ b/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 `_, + fixes `#18656 `_, + by Gaëtan Gilbert). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 0736a373dbbbc..db41f52fae67b 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/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 diff --git a/plugins/ltac2/tac2entries.ml b/plugins/ltac2/tac2entries.ml index fb4c65f15a157..b5a54c38df097 100644 --- a/plugins/ltac2/tac2entries.ml +++ b/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,6 +970,8 @@ 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"; @@ -964,8 +979,8 @@ let register_struct atts str = match str with 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, []))); } diff --git a/plugins/ltac2/tac2entries.mli b/plugins/ltac2/tac2entries.mli index 725d6864cc588..d9e9223e5d2d8 100644 --- a/plugins/ltac2/tac2entries.mli +++ b/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 -> diff --git a/plugins/ltac2/tac2print.ml b/plugins/ltac2/tac2print.ml index 5489d59c9a5e7..d68de52f32ac8 100644 --- a/plugins/ltac2/tac2print.ml +++ b/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 "" + | 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 "" | _, 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 "" | _, 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 "" | _, 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 diff --git a/test-suite/output/ltac2_abstract.out b/test-suite/output/ltac2_abstract.out new file mode 100644 index 0000000000000..0bbcac5b836e3 --- /dev/null +++ b/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 = +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 = +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 = +- : bool = false +Ltac2 M.a : M.t + M.a := +Ltac2 M.is_b : M.t -> bool + M.is_b := fun x => match x with + + end +Ltac2 M.get_b : int -> M.t -> int + M.get_b := fun def x => match x with + | => x + | _ => def + end +- : int M.t = +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 = +- : 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 => +Ltac2 p : 'a t -> 'a + p := fun x => +Ltac2 set : 'a t -> 'a -> unit + set := fun x v => +File "./output/ltac2_abstract.v", line 91, characters 32-33: +The command has indeed failed with message: +Open types currently do not support #[abstract]. diff --git a/test-suite/output/ltac2_abstract.v b/test-suite/output/ltac2_abstract.v new file mode 100644 index 0000000000000..54ab968f25a12 --- /dev/null +++ b/test-suite/output/ltac2_abstract.v @@ -0,0 +1,110 @@ +Require Import Ltac2.Ltac2. + +Module AbstractType. + (* redundant, maybe should be an error? *) + #[abstract] Ltac2 Type t. +End AbstractType. + +Module DefinedType. + Module M. + #[abstract] Ltac2 Type t := int. + + Ltac2 foo (x:t) : t := Int.add x 1. + + Ltac2 make (x:int) : t := x. + Ltac2 repr (x:t) : int := x. + + Ltac2 three : t := 3. + End M. + + Fail Ltac2 nope : M.t := 0. + + Ltac2 ok () : M.t := M.make 0. + + Ltac2 Eval ok (). + + Import M. + + Fail Ltac2 nope : M.t := 0. + + Ltac2 Eval repr (foo (make 1)). + + Print foo. + Print three. + + Ltac2 Eval three. +End DefinedType. + +Module AlgebraicType. + Module M. + #[abstract] Ltac2 Type t := [ A | B (int option) ]. + + Ltac2 a := A. + Ltac2 is_b x := match x with B _ => true | _ => false end. + Ltac2 get_b def x := match x with B (Some x) => x | _ => def end. + End M. + + Fail Ltac2 Eval M.A. + + Fail Ltac2 Eval fun x => match x with M.A => true | _ => false end. + + Ltac2 Eval M.a. + + Ltac2 Eval M.is_b M.a. + + Print M.a. + Print M.is_b. + Print M.get_b. +End AlgebraicType. + +Module RecordType. + Module M. + #[abstract] Ltac2 Type 'a t := { mutable p : 'a }. + + Ltac2 make x := { p := x }. + Ltac2 set x v := x.(p) := v. + Ltac2 p x := x.(p). + End M. + + Ltac2 Eval M.make 0. + + Import M. + + Fail Ltac2 Eval { p := 0 }. + + Fail Ltac2 Eval fun x => x.(p). + + Ltac2 Eval make 42. + + Ltac2 Eval p (make 42). + + Fail Ltac2 Eval Int.add (p (make true)) 0. + + Print make. + Print p. + Print set. +End RecordType. + +Module ExtensibleType. + Module M. + (* TODO figure out what this should do, error until then. *) + Fail #[abstract] Ltac2 Type t := [ .. ]. + + (* Ltac2 Type t ::= [ E | E' ]. *) + + (* Fail #[abstract] Ltac2 Type t ::= [ F ]. *) + + (* Ltac2 e := E. *) + + (* Ltac2 is_e x := match x with E => true | _ => false end. *) + End M. + + (* Import M. *) + (* Ltac2 Eval E. *) + + (* Ltac2 Eval match E with E => true | _ => false end. *) + + (* Fail Ltac2 Type t ::= [ F ]. *) + + (* add more tests once we have something to test *) +End ExtensibleType.