aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/changes.txt7
-rw-r--r--doc/common/macros.tex3
-rw-r--r--doc/refman/RefMan-ext.tex24
-rw-r--r--interp/constrexpr_ops.ml88
-rw-r--r--interp/constrexpr_ops.mli12
-rw-r--r--parsing/g_constr.ml48
-rw-r--r--parsing/g_vernac.ml414
-rw-r--r--plugins/funind/indfun.ml6
-rw-r--r--test-suite/output/PatternsInBinders.out2
-rw-r--r--test-suite/output/PatternsInBinders.v3
-rw-r--r--test-suite/success/record_syntax.v8
-rw-r--r--vernac/command.ml2
12 files changed, 91 insertions, 86 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index af077bbb4..2080f164a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -44,6 +44,13 @@ The following constructors have been renamed:
LocalRawAssum -> CLocalAssum
LocalPattern -> CLocalPattern
+In Constrexpr_ops:
+
+ Deprecating abstract_constr_expr in favor of mkCLambdaN, and
+ prod_constr_expr in favor of mkCProdN. Note: the first ones were
+ interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second
+ ones were preserving the original sharing of the type.
+
** Ltac API **
Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 5abdecfc1..0a4251a37 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -145,7 +145,7 @@
\newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}}
\newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}}
-
+\newcommand{\typecstrtype}{\zeroone{{\tt :}~{\type}}}
\newcommand{\Fwterm}{\nterm{Fwterm}}
\newcommand{\Index}{\nterm{index}}
@@ -164,6 +164,7 @@
\newcommand{\digit}{\nterm{digit}}
\newcommand{\exteqn}{\nterm{ext\_eqn}}
\newcommand{\field}{\nterm{field}}
+\newcommand{\fielddef}{\nterm{field\_def}}
\newcommand{\firstletter}{\nterm{first\_letter}}
\newcommand{\fixpg}{\nterm{fix\_pgm}}
\newcommand{\fixpointbodies}{\nterm{fix\_bodies}}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 74d64497a..6dd0ddf81 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -29,8 +29,8 @@ construction allows defining ``signatures''.
{\recordkw} & ::= &
{\tt Record} $|$ {\tt Inductive} $|$ {\tt CoInductive}\\
& & \\
-{\field} & ::= & {\name} \zeroone{\binders} : {\type} [ {\tt where} {\it notation} ] \\
- & $|$ & {\name} \zeroone{\binders} {\typecstr} := {\term}
+{\field} & ::= & {\name} \zeroone{\binders} : {\type} \zeroone{{\tt where} {\it notation}} \\
+ & $|$ & {\name} \zeroone{\binders} {\typecstrtype} := {\term}\\
\end{tabular}
\end{centerframe}
\caption{Syntax for the definition of {\tt Record}}
@@ -213,7 +213,21 @@ Record point := { x : nat; y : nat }.
Definition a := Build_point 5 3.
\end{coq_example}
-The following syntax allows creating objects by using named fields. The
+\begin{figure}[t]
+\begin{centerframe}
+\begin{tabular}{lcl}
+{\term} & ++= &
+ \verb!{|! \zeroone{\nelist{\fielddef}{;}} \verb!|}! \\
+ & & \\
+{\fielddef} & ::= & {\name} \zeroone{\binders} := {\term} \\
+\end{tabular}
+\end{centerframe}
+\caption{Syntax for constructing elements of a \texttt{Record} using named fields}
+\label{fig:fieldsyntax}
+\end{figure}
+
+A syntax is available for creating objects by using named fields, as
+shown on Figure~\ref{fig:fieldsyntax}. The
fields do not have to be in any particular order, nor do they have to be all
present if the missing ones can be inferred or prompted for (see
Section~\ref{Program}).
@@ -252,7 +266,7 @@ Eval compute in (
Reset Initial.
\end{coq_eval}
-\Rem An experimental syntax for projections based on a dot notation is
+\Rem A syntax for projections based on a dot notation is
available. The command to activate it is
\optindex{Printing Projections}
\begin{quote}
@@ -267,7 +281,7 @@ available. The command to activate it is
& $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )}
\end{tabular}
\end{centerframe}
-\caption{Syntax of \texttt{Record} projections}
+\caption{Syntax for \texttt{Record} projections}
\label{fig:projsyntax}
\end{figure}
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 53c97f6b6..a592b4cff 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -303,83 +303,51 @@ let add_name_in_env env n =
let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) ()
-let expand_pattern_binders mkC bl c =
- let rec loop bl c =
+let expand_binders mkC loc bl c =
+ let rec loop loc bl c =
match bl with
- | [] -> ([], [], c)
+ | [] -> ([], c)
| b :: bl ->
- let (env, bl, c) = loop bl c in
match b with
- | CLocalDef (n, _, _) ->
+ | CLocalDef ((loc1,_) as n, oty, b) ->
+ let env, c = loop (Loc.merge loc1 loc) bl c in
let env = add_name_in_env env n in
- (env, b :: bl, c)
- | CLocalAssum (nl, _, _) ->
+ (env, CLetIn (loc,n,oty,b,c))
+ | CLocalAssum ((loc1,_)::_ as nl, bk, t) ->
+ let env, c = loop (Loc.merge loc1 loc) bl c in
let env = List.fold_left add_name_in_env env nl in
- (env, b :: bl, c)
- | CLocalPattern (loc, p, ty) ->
+ (env, mkC loc (nl,bk,t) c)
+ | CLocalAssum ([],_,_) -> loop loc bl c
+ | CLocalPattern (loc1, p, ty) ->
+ let env, c = loop (Loc.merge loc1 loc) bl c in
let ni = Hook.get fresh_var env c in
- let id = (loc, Name ni) in
- let b =
- CLocalAssum
- ([id], Default Explicit,
- match ty with
+ let id = (loc1, Name ni) in
+ let ty = match ty with
| Some ty -> ty
- | None -> CHole (loc, None, IntroAnonymous, None))
+ | None -> CHole (loc1, None, IntroAnonymous, None)
in
- let e = CRef (Libnames.Ident (loc, ni), None) in
+ let e = CRef (Libnames.Ident (loc1, ni), None) in
let c =
CCases
(loc, LetPatternStyle, None, [(e,None,None)],
- [(loc, [(loc,[p])], mkC loc bl c)])
+ [(loc1, [(loc1,[p])], c)])
in
- (ni :: env, [b], c)
+ (ni :: env, mkC loc ([id],Default Explicit,ty) c)
in
- let (_, bl, c) = loop bl c in
- (bl, c)
+ let (_, c) = loop loc bl c in
+ c
let mkCProdN loc bll c =
- let rec loop loc bll c =
- match bll with
- | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
- CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
- | CLocalDef ((loc1,_) as id,b,t) :: bll ->
- CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c)
- | [] -> c
- | CLocalAssum ([],_,_) :: bll -> loop loc bll c
- | CLocalPattern (loc,p,ty) :: bll -> assert false
- in
- let (bll, c) = expand_pattern_binders loop bll c in
- loop loc bll c
+ let mk loc b c = CProdN (loc,[b],c) in
+ expand_binders mk loc bll c
let mkCLambdaN loc bll c =
- let rec loop loc bll c =
- match bll with
- | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
- CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
- | CLocalDef ((loc1,_) as id,b,t) :: bll ->
- CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c)
- | [] -> c
- | CLocalAssum ([],_,_) :: bll -> loop loc bll c
- | CLocalPattern (loc,p,ty) :: bll -> assert false
- in
- let (bll, c) = expand_pattern_binders loop bll c in
- loop loc bll c
-
-let rec abstract_constr_expr c = function
- | [] -> c
- | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,abstract_constr_expr c bl)
- | CLocalAssum (idl,bk,t)::bl ->
- List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
- (abstract_constr_expr c bl)
- | CLocalPattern _::_ -> assert false
-
-let rec prod_constr_expr c = function
- | [] -> c
- | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,prod_constr_expr c bl)
- | CLocalAssum (idl,bk,t)::bl ->
- List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
- (prod_constr_expr c bl)
- | CLocalPattern _::_ -> assert false
+ let mk loc b c = CLambdaN (loc,[b],c) in
+ expand_binders mk loc bll c
+
+(* Deprecated *)
+let abstract_constr_expr c bl = mkCLambdaN (local_binders_loc bl) bl c
+let prod_constr_expr c bl = mkCProdN (local_binders_loc bl) bl c
let coerce_reference_to_id = function
| Ident (_,id) -> id
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 45e3a19bc..f6d97e107 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -49,19 +49,19 @@ val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr ->
val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr
val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
-val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
-val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
-
val mkCLambdaN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
(** Same as [abstract_constr_expr], with location *)
val mkCProdN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
(** Same as [prod_constr_expr], with location *)
+(** @deprecated variant of mkCLambdaN *)
+val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
+
+(** @deprecated variant of mkCProdN *)
+val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
+
val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t
-val expand_pattern_binders :
- (Loc.t -> local_binder_expr list -> constr_expr -> constr_expr) ->
- local_binder_expr list -> constr_expr -> local_binder_expr list * constr_expr
(** {6 Destructors}*)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 05cb74ddc..0f2ed88fe 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -43,9 +43,6 @@ let binder_of_name expl (loc,na) =
let binders_of_names l =
List.map (binder_of_name Explicit) l
-let binders_of_lidents l =
- List.map (fun (loc, id) -> binder_of_name Explicit (loc, Name id)) l
-
let mk_fixb (id,bl,ann,body,(loc,tyc)) =
let ty = match tyc with
Some ty -> ty
@@ -222,15 +219,14 @@ GEXTEND Gram
record_fields:
[ [ f = record_field_declaration; ";"; fs = record_fields -> f :: fs
- | f = record_field_declaration; ";" -> [f]
| f = record_field_declaration -> [f]
| -> []
] ]
;
record_field_declaration:
- [ [ id = global; params = LIST0 identref; ":="; c = lconstr ->
- (id, abstract_constr_expr c (binders_of_lidents params)) ] ]
+ [ [ id = global; bl = binders; ":="; c = lconstr ->
+ (id, mkCLambdaN (!@loc) bl c) ] ]
;
binder_constr:
[ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 71b93439b..4fd316119 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -236,16 +236,22 @@ GEXTEND Gram
(* Simple definitions *)
def_body:
[ [ bl = binders; ":="; red = reduce; c = lconstr ->
- let (bl, c) = expand_pattern_binders mkCLambdaN bl c in
- (match c with
- CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t)
+ if List.exists (function CLocalPattern _ -> true | _ -> false) bl
+ then
+ (* FIXME: "red" will be applied to types in bl and Cast with remain *)
+ let c = mkCLambdaN (!@loc) bl c in
+ DefineBody ([], red, c, None)
+ else
+ (match c with
+ | CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t)
| _ -> DefineBody (bl, red, c, None))
| bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
let ((bl, c), tyo) =
if List.exists (function CLocalPattern _ -> true | _ -> false) bl
then
+ (* FIXME: "red" will be applied to types in bl and Cast with remain *)
let c = CCast (!@loc, c, CastConv t) in
- (expand_pattern_binders mkCLambdaN bl c, None)
+ (([],mkCLambdaN (!@loc) bl c), None)
else ((bl, c), Some t)
in
DefineBody (bl, red, c, tyo)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ebeddf5f6..d335836df 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -156,7 +156,7 @@ let build_newrecursive
let (rec_sign,rec_impls) =
List.fold_left
(fun (env,impls) (((_,recname),_),bl,arityc,_) ->
- let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
+ let arityc = Constrexpr_ops.mkCProdN Loc.ghost bl arityc in
let arity,ctx = Constrintern.interp_type env0 sigma arityc in
let evdref = ref (Evd.from_env env0) in
let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
@@ -453,7 +453,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
pre_hook
=
- let type_of_f = Constrexpr_ops.prod_constr_expr ret_type args in
+ let type_of_f = Constrexpr_ops.mkCProdN Loc.ghost args ret_type in
let rec_arg_num =
let names =
List.map
@@ -484,7 +484,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
Constrexpr.CApp (Loc.ghost,(None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))),
[(f_app_args,None);(body,None)])
in
- let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in
+ let eq = Constrexpr_ops.mkCProdN Loc.ghost args unbounded_eq in
let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
nb_args relation =
try
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index c012a86b0..95be04c32 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -37,3 +37,5 @@ fun '(x, y) '(z, t) => swap (x, y) = (z, t)
: A * B -> B * A -> Prop
forall '(x, y) '(z, t), swap (x, y) = (z, t)
: Prop
+fun (pat : nat) '(x, y) => x + y = pat
+ : nat -> nat * nat -> Prop
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 6fa357a90..0bad472f4 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -64,3 +64,6 @@ Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
End Suboptimal.
+
+(** Test risk of collision for internal name *)
+Check fun pat => fun '(x,y) => x+y = pat.
diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v
index db2bbb0dc..07a5bc060 100644
--- a/test-suite/success/record_syntax.v
+++ b/test-suite/success/record_syntax.v
@@ -45,3 +45,11 @@ Record Foo := { foo : unit; }.
Definition foo_ := {| foo := tt; |}.
End E.
+
+Module F.
+
+Record Foo := { foo : nat * nat -> nat -> nat }.
+
+Definition foo_ := {| foo '(x,y) n := x+y+n |}.
+
+End F.
diff --git a/vernac/command.ml b/vernac/command.ml
index 781bf3223..4a5a4312e 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -266,7 +266,7 @@ match local with
(gr,inst,Lib.is_modtype_strict ())
let interp_assumption evdref env impls bl c =
- let c = prod_constr_expr c bl in
+ let c = mkCProdN (local_binders_loc bl) bl c in
let ty, impls = interp_type_evars_impls env evdref ~impls c in
let ty = EConstr.Unsafe.to_constr ty in
(ty, impls)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 07:56:30 +0000