aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml99
-rw-r--r--interp/constrintern.ml18
-rw-r--r--library/impargs.ml4
-rw-r--r--pretyping/constrMatching.ml23
-rw-r--r--test-suite/success/primitiveproj.v112
-rw-r--r--theories/FSets/FMapPositive.v4
-rw-r--r--theories/Init/Datatypes.v4
-rw-r--r--theories/Init/Specif.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v2
9 files changed, 214 insertions, 54 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6f0491ca1..284bba1b7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -437,15 +437,22 @@ let occur_name na aty =
| Name id -> occur_var_constr_expr id aty
| Anonymous -> false
-let is_projection primproj nargs = function
- | Some r when not !in_debugger && not !Flags.raw_print && !print_projections ->
- if primproj then Some 1
- else
+let is_projection primproj nargs cf =
+ if primproj then Some 1
+ else
+ match cf with
+ | Some r when not !in_debugger && not !Flags.raw_print && !print_projections ->
(try
let n = Recordops.find_projection_nparams r + 1 in
- if n <= nargs then Some n else None
- with Not_found -> None)
- | _ -> None
+ if n <= nargs then
+ (* For primitive projections, r.(p) and r.(@p) are reserved to the
+ non-eta-expanded version of the constant, we disallow printing
+ of the eta-expanded projection as a projection *)
+ if Environ.is_projection (destConstRef r) (Global.env()) then None
+ else Some n
+ else None
+ with Not_found -> None)
+ | _ -> None
let is_hole = function CHole _ -> true | _ -> false
@@ -455,6 +462,8 @@ let is_significant_implicit a =
let is_needed_for_correct_partial_application tail imp =
List.is_empty tail && not (maximal_insertion_of imp)
+exception Expl
+
(* Implicit args indexes are in ascending order *)
(* inctx is useful only if there is a last argument to be deduced from ctxt *)
let explicitize loc inctx impl (cf,primproj,f) args =
@@ -477,45 +486,60 @@ let explicitize loc inctx impl (cf,primproj,f) args =
tail
| a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
| args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*)
- | [], _ -> [] in
- match is_projection primproj (List.length args) cf with
- | Some i as ip ->
- if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
- let args = exprec 1 (args,impl) in
- if primproj then CApp (loc, (None, f), args)
- else
- let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in
- CAppExpl (loc,(ip,f',us),List.map fst args)
- else
- let (args1,args2) = List.chop i args in
- let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in
- let args1 = exprec 1 (args1,impl1) in
- let args2 = exprec (i+1) (args2,impl2) in
- CApp (loc,(Some (List.length args1),f),args1@args2)
- | None ->
+ | [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp ->
+ (* The non-explicit application cannot be parsed back with the same type *)
+ raise Expl
+ | [], _ -> []
+ in
+ let ip = is_projection primproj (List.length args) cf in
+ let expl () =
+ match ip with
+ | Some i ->
+ if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
+ if primproj then
+ let args = exprec 1 (args,impl) in
+ CApp (loc, (None, f), args)
+ else raise Expl
+ else
+ let (args1,args2) = List.chop i args in
+ let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in
+ let args1 = exprec 1 (args1,impl1) in
+ let args2 = exprec (i+1) (args2,impl2) in
+ let len = List.length args1 in
+ let ip = (* Printing primitive projection as application *)
+ if len == 1 && primproj && not !print_projections && not !Flags.raw_print then None
+ else Some len
+ in
+ CApp (loc,(ip,f),args1@args2)
+ | None ->
match cf with
- | Some (ConstRef p) when not !in_debugger && not primproj && Environ.is_projection p (Global.env ()) ->
- (* Eta-expanded version of projection, print explicited if the implicit application would be parsed
- as a primitive projection application. *)
+ | Some (ConstRef p) when not !in_debugger && not primproj
+ && Environ.is_projection p (Global.env ()) ->
+ (* Eta-expanded version of projection, print explicited if the implicit
+ application would be parsed as a primitive projection application. *)
let proj = Environ.lookup_projection p (Global.env ()) in
- let expl =
- if List.length args > proj.Declarations.proj_npars then
+ if List.length args > proj.Declarations.proj_npars &&
List.for_all is_status_implicit (List.firstn proj.Declarations.proj_npars impl)
- else false
- in
- if expl then
- let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in
- CAppExpl (loc,(None,f',us),args)
+ then raise Expl
else
let args = exprec 1 (args,impl) in
CApp (loc, (None, f), args)
| _ ->
let args = exprec 1 (args,impl) in
if List.is_empty args then f else CApp (loc, (None, f), args)
+ in
+ try expl ()
+ with Expl ->
+ let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in
+ let ip = if primproj || !print_projections then ip else None in
+ CAppExpl (loc, (ip, f', us), args)
+
+let is_start_implicit = function
+ | imp :: _ -> is_status_implicit imp (* && maximal_insertion_of imp *)
+ | [] -> false
let extern_global loc impl f us =
- if not !Constrintern.parsing_explicit &&
- not (List.is_empty impl) && List.for_all is_status_implicit impl
+ if not !Constrintern.parsing_explicit && is_start_implicit impl
then
CAppExpl (loc, (None, f, us), [])
else
@@ -530,7 +554,10 @@ let extern_app loc inctx impl (cf,primproj,f) us args =
(!print_implicits && not !print_implicits_explicit_args)) &&
List.exists is_status_implicit impl)
then
- CAppExpl (loc, (is_projection primproj (List.length args) cf,f,us), args)
+ if primproj then
+ CAppExpl (loc, (Some 1,f,us), args)
+ else
+ CAppExpl (loc, (is_projection primproj (List.length args) cf,f,us), args)
else
explicitize loc inctx impl (cf,primproj,CRef (f,us)) args
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7db2203c0..8f250e890 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1458,13 +1458,19 @@ let internalize globalenv env allow_patvar lvar c =
intern {env with tmp_scope = None;
scopes = find_delimiters_scope loc key :: env.scopes} e
| CAppExpl (loc, (isproj,ref,us), args) ->
- let (f,_,args_scopes,_),_,args =
+ let (f,_,args_scopes,_),isprojf,args =
let args = List.map (fun a -> (a,None)) args in
intern_applied_reference intern env (Environ.named_context globalenv)
- lvar us args ref in
- (* check_projection isproj (List.length args) f; *)
- (* Rem: GApp(_,f,[]) stands for @f *)
- GApp (loc, f, intern_args env args_scopes (List.map fst args))
+ lvar us args ref
+ in
+ (match isproj, isprojf with
+ | Some i, Some (r, n) -> (* Explicit application of primitive projection *)
+ let scopes = proj_scopes n args_scopes in
+ let args = intern_args env args_scopes (List.map fst args) in
+ GApp (loc, GProj (loc, r, List.hd args), List.tl args)
+ | _ ->
+ (* Rem: GApp(_,f,[]) stands for @f *)
+ GApp (loc, f, intern_args env args_scopes (List.map fst args)))
| CApp (loc, (isproj,f), args) ->
let isproj,f,args = match f with
@@ -1737,7 +1743,7 @@ let internalize globalenv env allow_patvar lvar c =
match isprojf with
| Some (r, n) ->
(match projection_implicits n (List.is_empty l) imp with
- | Some imp ->
+ | Some imp -> (* A primitive projection *)
let subscopes = proj_scopes n subscopes in
let imp =
if isproj != None then
diff --git a/library/impargs.ml b/library/impargs.ml
index 55e21b2c8..355cbe1fa 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -378,7 +378,9 @@ let set_manual_implicits env flags enriching autoimps l =
l, imp, m
in
let imps' = merge (k+1) l' imps in
- let m = Option.map (fun (b,f) -> set_maximality imps' b, f) m in
+ let m = Option.map (fun (b,f) ->
+ (* match imp with Some Manual -> (b,f) *)
+ (* | _ -> *)set_maximality imps' b, f) m in
Option.map (set_implicit id imp) m :: imps'
| (Anonymous,imp)::imps ->
let l', forced = try_forced k l in
diff --git a/pretyping/constrMatching.ml b/pretyping/constrMatching.ml
index e23a4e440..15053505e 100644
--- a/pretyping/constrMatching.ml
+++ b/pretyping/constrMatching.ml
@@ -209,7 +209,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
sorec stk env subst (PApp(h,Array.append a1 a2)) t
| PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app ->
- let p = Array.length args2 - Array.length args1 in
+ (let p = Array.length args2 - Array.length args1 in
if p >= 0 then
let args21, args22 = Array.chop p args2 in
let c = mkApp(c2,args21) in
@@ -218,11 +218,18 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
| None -> subst
| Some n -> merge_binding allow_bound_rels stk n c subst in
Array.fold_left2 (sorec stk env) subst args1 args22
- else raise PatternMatchingFailure
+ else (* Might be a projection on the right *)
+ match kind_of_term c2 with
+ | Proj _ ->
+ let subst = sorec stk env subst (PApp (PMeta meta, [|args1.(0)|])) c2 in
+ Array.fold_left2 (sorec stk env) subst (Array.tl args1) args2
+ | _ -> raise PatternMatchingFailure)
| PApp (c1,arg1), App (c2,arg2) ->
+ let diff = Array.length arg2 - Array.length arg1 in
(match c1, kind_of_term c2 with
- | PRef (ConstRef r), Proj (p,c) ->
+ (* eta-expanded version of projection against projection *)
+ | PRef (ConstRef r), Proj (p,c) when eq_constant r p ->
let pb = Environ.lookup_projection p env in
let npars = pb.Declarations.proj_npars in
let narg1 = Array.length arg1 in
@@ -232,9 +239,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c =
try Array.fold_left2 (sorec stk env) subst args arg2
with Invalid_argument _ -> raise PatternMatchingFailure
else raise PatternMatchingFailure
+ (* meta against projection *)
+ | PMeta meta, Proj (p,c) when diff != 0 ->
+ if diff == -1 then (* One more arg for the meta *)
+ Array.fold_left2 (sorec stk env) (sorec stk env subst (PApp (c1, [|arg1.(0)|])) c2)
+ (Array.tl arg1) arg2
+ else raise PatternMatchingFailure
| _ ->
- (try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
- with Invalid_argument _ -> raise PatternMatchingFailure))
+ try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2
+ with Invalid_argument _ -> raise PatternMatchingFailure)
| PApp (PMeta (Some n), [|c1|]), Proj (p2, c2) ->
let ty = Retyping.get_type_of env sigma c2 in
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 4a9c81eb3..02cb43db0 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -61,3 +61,115 @@ Fixpoint yn (n : nat) (y : Y) : Y :=
Lemma eta_ind' (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}.
Proof. reflexivity. Defined.
+
+
+(*
+ Rules for parsing and printing of primitive projections and their eta expansions.
+ If r : R A where R is a primitive record with implicit parameter A.
+ If p : forall {A} (r : R A) {A : Set}, list (A * B).
+*)
+
+Record R {A : Type} := { p : forall {X : Set}, A * X }.
+Arguments R : clear implicits.
+
+Record R' {A : Type} := { p' : forall X : Set, A * X }.
+Arguments R' : clear implicits.
+
+Unset Printing All.
+
+Parameter r : R nat.
+
+Check (r.(p)).
+Set Printing Projections.
+Check (r.(p)).
+Unset Printing Projections.
+Set Printing All.
+Check (r.(p)).
+Unset Printing All.
+
+(* Check (r.(p)).
+ Elaborates to a primitive application, X arg implicit.
+ Of type nat * ?ex
+ No Printing All: p r
+ Set Printing Projections.: r.(p)
+ Printing All: r.(@p) ?ex
+ *)
+
+Check p r.
+Set Printing Projections.
+Check p r.
+Unset Printing Projections.
+Set Printing All.
+Check p r.
+Unset Printing All.
+
+(* Same elaboration, printing for p r *)
+
+(** Explicit version of the primitive projection, under applied w.r.t implicit arguments
+ can be printed only using projection notation. r.(@p) *)
+Check r.(@p).
+Set Printing Projections.
+Check r.(@p).
+Unset Printing Projections.
+Set Printing All.
+Check r.(@p).
+Unset Printing All.
+
+(** Explicit version of the primitive projection, applied to its implicit arguments
+ can be printed only using projection notation r.(p), r.(@p) in fully explicit form *)
+Check r.(@p) nat.
+Set Printing Projections.
+Check r.(@p) nat.
+Unset Printing Projections.
+Set Printing All.
+Check r.(@p) nat.
+Unset Printing All.
+
+Parameter r' : R' nat.
+
+Check (r'.(p')).
+Set Printing Projections.
+Check (r'.(p')).
+Unset Printing Projections.
+Set Printing All.
+Check (r'.(p')).
+Unset Printing All.
+
+(* Check (r'.(p')).
+ Elaborates to a primitive application, X arg explicit.
+ Of type forall X : Set, nat * X
+ No Printing All: p' r'
+ Set Printing Projections.: r'.(p')
+ Printing All: r'.(p')
+ *)
+
+Check p' r'.
+Set Printing Projections.
+Check p' r'.
+Unset Printing Projections.
+Set Printing All.
+Check p' r'.
+Unset Printing All.
+
+(* Same elaboration, printing for p r *)
+
+(** Explicit version of the primitive projection, under applied w.r.t implicit arguments
+ can be printed only using projection notation. r.(@p) *)
+Check r'.(@p').
+Set Printing Projections.
+Check r'.(@p').
+Unset Printing Projections.
+Set Printing All.
+Check r'.(@p').
+Unset Printing All.
+
+(** Explicit version of the primitive projection, applied to its implicit arguments
+ can be printed only using projection notation r.(p), r.(@p) in fully explicit form *)
+Check p' r' nat.
+Set Printing Projections.
+Check p' r' nat.
+Unset Printing Projections.
+Set Printing All.
+Check p' r' nat.
+Unset Printing All.
+
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index c9d868c40..3eac15b03 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -82,7 +82,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
Section A.
Variable A:Type.
- Arguments Leaf [A].
+ Arguments Leaf {A}.
Definition empty : t A := Leaf.
@@ -812,7 +812,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
Variable A B C : Type.
Variable f : option A -> option B -> option C.
- Arguments Leaf [A].
+ Arguments Leaf {A}.
Fixpoint xmap2_l (m : t A) : t C :=
match m with
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index c8d18f766..093a2c140 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -151,7 +151,7 @@ Inductive option (A:Type) : Type :=
| Some : A -> option A
| None : option A.
-Arguments None [A].
+Arguments None {A}.
Definition option_map (A B:Type) (f:A->B) (o : option A) : option B :=
match o with
@@ -224,7 +224,7 @@ Inductive list (A : Type) : Type :=
| nil : list A
| cons : A -> list A -> list A.
-Arguments nil [A].
+Arguments nil {A}.
Infix "::" := cons (at level 60, right associativity) : list_scope.
Delimit Scope list_scope with list.
Bind Scope list_scope with list.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 1ddb59cf4..c3edcfdfd 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -285,7 +285,7 @@ Section Exc.
Definition value := @Some A.
Definition error := @None A.
End Exc.
-Arguments error [A].
+Arguments error {A}.
Definition except := False_rec. (* for compatibility with previous versions *)
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index ce1c0bef1..900cb1db5 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -53,7 +53,7 @@ Section Zn2Z.
End Zn2Z.
-Arguments W0 [znz].
+Arguments W0 {znz}.
(** From a cyclic representation [w], we iterate the [zn2z] construct
[n] times, gaining the type of binary trees of depth at most [n],
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 10:52:41 +0000