aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/notation_ops.ml5
-rw-r--r--lib/dAst.ml2
-rw-r--r--lib/dAst.mli1
-rw-r--r--plugins/funind/glob_term_to_relation.ml10
-rw-r--r--pretyping/glob_ops.ml10
-rw-r--r--pretyping/glob_ops.mli1
-rw-r--r--test-suite/output/Notations4.out20
-rw-r--r--test-suite/output/Notations4.v9
-rw-r--r--test-suite/success/Notations2.v11
9 files changed, 57 insertions, 12 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 890c24e633..7d7e10a05b 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -908,11 +908,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
(* TODO: look at the consequences for alp *)
alp, add_env alp sigma var (DAst.make @@ GVar id)
-let force_cases_pattern c =
- DAst.make ?loc:c.CAst.loc (DAst.get c)
-
let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
- let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in
+ let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in
try
(* If already bound to a binder, unify the term and the binder *)
let patl' = Id.List.assoc var binders in
diff --git a/lib/dAst.ml b/lib/dAst.ml
index f34ab956a3..803b2a0cff 100644
--- a/lib/dAst.ml
+++ b/lib/dAst.ml
@@ -30,6 +30,8 @@ let make ?loc v = CAst.make ?loc (Value v)
let delay ?loc v = CAst.make ?loc (Thunk (Lazy.from_fun v))
+let force x = CAst.make ?loc:x.CAst.loc (Value (get_thunk x.v))
+
let map f n = CAst.map (fun x -> map_thunk f x) n
let map_with_loc f n =
diff --git a/lib/dAst.mli b/lib/dAst.mli
index 28c78784e6..2f58cfc41f 100644
--- a/lib/dAst.mli
+++ b/lib/dAst.mli
@@ -21,6 +21,7 @@ val get_thunk : ('a, 'b) thunk -> 'a
val make : ?loc:Loc.t -> 'a -> ('a, 'b) t
val delay : ?loc:Loc.t -> (unit -> 'a) -> ('a, [ `thunk ]) t
+val force : ('a, 'b) t -> ('a, 'b) t
val map : ('a -> 'b) -> ('a, 'c) t -> ('b, 'c) t
val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> ('b, 'c) t
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 02964d7ba5..ba0a3bbb5c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -321,12 +321,10 @@ let build_constructors_of_type ind' argl =
construct
in
let argl =
- if List.is_empty argl
- then
- Array.to_list
- (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
- )
- else argl
+ if List.is_empty argl then
+ List.make cst_narg (mkGHole ())
+ else
+ List.make npar (mkGHole ()) @ argl
in
let pat_as_term =
mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6b61b1452e..68626597fc 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -485,7 +485,11 @@ let is_gvar id c = match DAst.get c with
| GVar id' -> Id.equal id id'
| _ -> false
-let rec cases_pattern_of_glob_constr na = DAst.map (function
+let rec cases_pattern_of_glob_constr na c =
+ (* Forcing evaluation to ensure that the possible raising of
+ Not_found is not delayed *)
+ let c = DAst.force c in
+ DAst.map (function
| GVar id ->
begin match na with
| Name _ ->
@@ -498,6 +502,8 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
| GApp (c, l) ->
begin match DAst.get c with
| GRef (ConstructRef cstr,_) ->
+ let nparams = Inductiveops.inductive_nparams (fst cstr) in
+ let _,l = List.chop nparams l in
PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
| _ -> raise Not_found
end
@@ -505,7 +511,7 @@ let rec cases_pattern_of_glob_constr na = DAst.map (function
(* A canonical encoding of aliases *)
DAst.get (cases_pattern_of_glob_constr na' b)
| _ -> raise Not_found
- )
+ ) c
open Declarations
open Term
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 91a2ef9c1e..c189a3bcb2 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -89,6 +89,7 @@ val map_pattern : (glob_constr -> glob_constr) ->
(** Conversion from glob_constr to cases pattern, if possible
+ Evaluation is forced.
Take the current alias as parameter,
@raise Not_found if translation is impossible *)
val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index efa895d709..5bf4ec7bfb 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -53,3 +53,23 @@ Notation Cn := Foo.FooCn
Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn
let v := 0%test17 in v : myint63
: myint63
+fun y : nat => # (x, z) |-> y & y
+ : forall y : nat,
+ (?T1 * ?T2 -> ?T1 * ?T2 * nat) * (?T * ?T0 -> ?T * ?T0 * nat)
+where
+?T : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0
+ |- Type] (pat, p0, p cannot be used)
+?T0 : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0
+ |- Type] (pat, p0, p cannot be used)
+?T1 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2
+ |- Type] (pat, p0, p cannot be used)
+?T2 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2
+ |- Type] (pat, p0, p cannot be used)
+fun y : nat => # (x, z) |-> (x + y) & (y + z)
+ : forall y : nat,
+ (nat * ?T -> nat * ?T * nat) * (?T0 * nat -> ?T0 * nat * nat)
+where
+?T : [y : nat pat : nat * ?T p0 : nat * ?T p := p0 : nat * ?T
+ |- Type] (pat, p0, p cannot be used)
+?T0 : [y : nat pat : ?T0 * nat p0 : ?T0 * nat p := p0 : ?T0 * nat
+ |- Type] (pat, p0, p cannot be used)
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index b4c65ce196..b33ad17ed4 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -210,3 +210,12 @@ Module NumeralNotations.
Check let v := 0%test17 in v : myint63.
End Test17.
End NumeralNotations.
+
+Module K.
+
+Notation "# x |-> t & u" := ((fun x => (x,t)),(fun x => (x,u)))
+ (at level 0, x pattern, t, u at level 39).
+Check fun y : nat => # (x,z) |-> y & y.
+Check fun y : nat => # (x,z) |-> (x + y) & (y + z).
+
+End K.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 1b33863e3b..2533a39cc4 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -154,3 +154,14 @@ Module M16.
Print Grammar foo.
Print Grammar foo2.
End M16.
+
+(* Example showing the need for strong evaluation of
+ cases_pattern_of_glob_constr (this used to raise Not_found at some
+ time) *)
+
+Module M17.
+
+Notation "# x ## t & u" := ((fun x => (x,t)),(fun x => (x,u))) (at level 0, x pattern).
+Check fun y : nat => # (x,z) ## y & y.
+
+End M17.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:42:21 +0000