aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml13
-rw-r--r--interp/constrintern.ml51
-rw-r--r--interp/notation_ops.ml6
-rw-r--r--pretyping/glob_ops.ml33
-rw-r--r--pretyping/glob_ops.mli2
-rw-r--r--test-suite/output/Cases.out14
-rw-r--r--test-suite/output/Cases.v15
-rw-r--r--test-suite/output/Record.out10
-rw-r--r--test-suite/output/Record.v7
9 files changed, 129 insertions, 22 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0ba056a87..74504e36d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -274,17 +274,8 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
(* Better to use extern_glob_constr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
- (* pboutill: There are letins in pat which is incompatible with notations and
- not explicit application. *)
- match pat with
- | PatCstr(loc,cstrsp,args,na)
- when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
- let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
- let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
- CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
- | _ ->
try
- if !Flags.raw_print || !print_no_symbol then raise No_match;
+ if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
match availability_of_prim_token p sc scopes with
| None -> raise No_match
@@ -293,7 +284,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
with No_match ->
try
- if !Flags.raw_print || !print_no_symbol then raise No_match;
+ if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
extern_notation_pattern scopes vars pat
(uninterp_cases_pattern_notations pat)
with No_match ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c916fcd88..99ef21da3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -994,6 +994,45 @@ let check_constructor_length env loc cstr len_pl pl0 =
(error_wrong_numarg_constructor_loc loc env cstr
(Inductiveops.constructor_nrealargs cstr)))
+open Term
+open Declarations
+
+(* Similar to Cases.adjust_local_defs but on RCPat *)
+let insert_local_defs_in_pattern (ind,j) l =
+ let (mib,mip) = Global.lookup_inductive ind in
+ if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
+ (* Optimisation *) l
+ else
+ let typi = mip.mind_nf_lc.(j-1) in
+ let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in
+ let (decls,_) = decompose_prod_assum typi in
+ let rec aux decls args =
+ match decls, args with
+ | Context.Rel.Declaration.LocalDef _ :: decls, args -> Constrexpr.RCPatAtom (Loc.ghost,None) :: aux decls args
+ | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *)
+ | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
+ | _ -> assert false in
+ aux (List.rev decls) l
+
+let add_local_defs_and_check_length loc env g pl args = match g with
+ | ConstructRef cstr ->
+ (* We consider that no variables corresponding to local binders
+ have been given in the "explicit" arguments, which come from a
+ "@C args" notation or from a custom user notation *)
+ let pl' = insert_local_defs_in_pattern cstr pl in
+ let maxargs = Inductiveops.constructor_nalldecls cstr in
+ if List.length pl' + List.length args > maxargs then
+ error_wrong_numarg_constructor_loc loc env cstr (Inductiveops.constructor_nrealargs cstr);
+ (* Two possibilities: either the args are given with explict
+ variables for local definitions, then we give the explicit args
+ extended with local defs, so that there is nothing more to be
+ added later on; or the args are not enough to have all arguments,
+ which a priori means local defs to add in the [args] part, so we
+ postpone the insertion of local defs in the explicit args *)
+ (* Note: further checks done later by check_constructor_length *)
+ if List.length pl' + List.length args = maxargs then pl' else pl
+ | _ -> pl
+
let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
let impl_list = if Int.equal len_pl1 0
then select_impargs_size (List.length pl2) impls_st
@@ -1221,7 +1260,7 @@ let rec subst_pat_iterator y t p = match p with
| RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a)
| RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl)
-let drop_notations_pattern looked_for =
+let drop_notations_pattern looked_for genv =
(* At toplevel, Constructors and Inductives are accepted, in recursive calls
only constructor are allowed *)
let ensure_kind top loc g =
@@ -1350,9 +1389,9 @@ let drop_notations_pattern looked_for =
| NApp (NRef g,pl) ->
ensure_kind top loc g;
let (argscs1,argscs2) = find_remaining_scopes pl args g in
- RCPatCstr (loc, g,
- List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
- List.map (in_pat false scopes) args, [])
+ let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in
+ let pl = add_local_defs_and_check_length loc genv g pl args in
+ RCPatCstr (loc, g, pl @ List.map (in_pat false scopes) args, [])
| NList (x,y,iter,terminator,lassoc) ->
if not (List.is_empty args) then user_err_loc
(loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns.");
@@ -1445,7 +1484,7 @@ and check_no_patcast_subst (pl,pll) =
let intern_cases_pattern genv scopes aliases pat =
check_no_patcast pat;
intern_pat genv aliases
- (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
+ (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat)
let _ =
intern_cases_pattern_fwd :=
@@ -1455,7 +1494,7 @@ let intern_ind_pattern genv scopes pat =
check_no_patcast pat;
let no_not =
try
- drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
+ drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat
with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type loc
in
match no_not with
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0c5393cf4..564882153 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1158,6 +1158,7 @@ let match_notation_constr u c (metas,pat) =
metas ([],[],[])
(* Matching cases pattern *)
+
let add_patterns_for_params ind l =
let mib,_ = Global.lookup_inductive ind in
let nparams = mib.Declarations.mind_nparams in
@@ -1190,10 +1191,11 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
| r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
| PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
| PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
- sigma,(0,add_patterns_for_params (fst r1) largs)
+ let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in
+ sigma,(0,l)
| PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
when eq_constructor r1 r2 ->
- let l1 = add_patterns_for_params (fst r1) args1 in
+ let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in
let le2 = List.length l2 in
if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
then
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 51660818f..0eda77651 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -559,12 +559,45 @@ let rec cases_pattern_of_glob_constr na = function
PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
| _ -> raise Not_found
+open Declarations
+open Term
+open Context
+
+(* Keep only patterns which are not bound to a local definitions *)
+let drop_local_defs typi args =
+ let (decls,_) = decompose_prod_assum typi in
+ let rec aux decls args =
+ match decls, args with
+ | [], [] -> []
+ | Rel.Declaration.LocalDef _ :: decls, pat :: args ->
+ begin
+ match pat with
+ | PatVar (_,Anonymous) -> aux decls args
+ | _ -> raise Not_found (* The pattern is used, one cannot drop it *)
+ end
+ | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
+ | _ -> assert false in
+ aux (List.rev decls) args
+
+let add_patterns_for_params_remove_local_defs (ind,j) l =
+ let (mib,mip) = Global.lookup_inductive ind in
+ let nparams = mib.Declarations.mind_nparams in
+ let l =
+ if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
+ (* Optimisation *) l
+ else
+ let typi = mip.mind_nf_lc.(j-1) in
+ let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in
+ drop_local_defs typi l in
+ Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l
+
(* Turn a closed cases pattern into a glob_constr *)
let rec glob_constr_of_closed_cases_pattern_aux = function
| PatCstr (loc,cstr,[],Anonymous) ->
GRef (loc,ConstructRef cstr,None)
| PatCstr (loc,cstr,l,Anonymous) ->
let ref = GRef (loc,ConstructRef cstr,None) in
+ let l = add_patterns_for_params_remove_local_defs cstr l in
GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l)
| _ -> raise Not_found
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 55e6b6533..6b8f131f4 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -76,3 +76,5 @@ val map_pattern : (glob_constr -> glob_constr) ->
val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern
val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr
+
+val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 8ce6f9795..f064dfe76 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -2,18 +2,18 @@ t_rect =
fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
fix F (t : t) : P t :=
match t as t0 return (P t0) with
- | @k _ x0 => f x0 (F x0)
+ | k _ x0 => f x0 (F x0)
end
: forall P : t -> Type,
(let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
Argument scopes are [function_scope function_scope _]
= fun d : TT => match d with
- | @CTT _ _ b => b
+ | {| f3 := b |} => b
end
: TT -> 0 = 0
= fun d : TT => match d with
- | @CTT _ _ b => b
+ | {| f3 := b |} => b
end
: TT -> 0 = 0
proj =
@@ -72,3 +72,11 @@ e1 : texp t1
e2 : texp t2
The term "0" has type "nat" while it is expected to have type
"typeDenote t0".
+fun '{{n, m, _}} => n + m
+ : J -> nat
+fun '{{n, m, p}} => n + m + p
+ : J -> nat
+fun '(D n m p q) => n + m + p + q
+ : J -> nat
+The command has indeed failed with message:
+The constructor D (in type J) expects 3 arguments.
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 407489642..6a4fd007d 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -106,3 +106,18 @@ Fail Fixpoint texpDenote t (e:texp t):typeDenote t:=
| TBinop t1 t2 _ b e1 e2 => O
end.
+(* Test notations with local definitions in constructors *)
+
+Inductive J := D : forall n m, let p := n+m in nat -> J.
+Notation "{{ n , m , q }}" := (D n m q).
+
+Check fun x : J => let '{{n, m, _}} := x in n + m.
+Check fun x : J => let '{{n, m, p}} := x in n + m + p.
+
+(* Cannot use the notation because of the dependency in p *)
+
+Check fun x => let '(D n m p q) := x in n+m+p+q.
+
+(* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *)
+
+Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p.
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
index 37b4fb25f..d45343fe6 100644
--- a/test-suite/output/Record.out
+++ b/test-suite/output/Record.out
@@ -20,3 +20,13 @@ fun '{| T := T |} => T
: N -> Type
fun '(C T p) => (T, p)
: N -> Type * True
+fun '{| q := p |} => p
+ : M -> True
+fun '{| U := T |} => T
+ : M -> Type
+fun '{| U := T; q := p |} => (T, p)
+ : M -> Type * True
+fun '{| U := T; a := a; q := p |} => (T, p, a)
+ : M -> Type * True * nat
+fun '{| U := T; a := a; q := p |} => (T, p, a)
+ : M -> Type * True * nat
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index c3d9f1e57..d9a649fad 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -24,3 +24,10 @@ Record N := C { T : Type; _ : True }.
Check fun x:N => let 'C _ p := x in p.
Check fun x:N => let 'C T _ := x in T.
Check fun x:N => let 'C T p := x in (T,p).
+
+Record M := D { U : Type; a := 0; q : True }.
+Check fun x:M => let 'D T _ p := x in p.
+Check fun x:M => let 'D T _ p := x in T.
+Check fun x:M => let 'D T p := x in (T,p).
+Check fun x:M => let 'D T a p := x in (T,p,a).
+Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 09:39:43 +0000