aboutsummaryrefslogtreecommitdiff
path: root/interp/notation_ops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation_ops.ml')
-rw-r--r--interp/notation_ops.ml64
1 files changed, 47 insertions, 17 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 265ca58ed9..54065e8b35 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -151,6 +151,24 @@ let rec subst_glob_vars l gc = DAst.map (function
let ldots_var = Id.of_string ".."
+type 'a binder_status_fun = {
+ no : 'a -> 'a;
+ restart_prod : 'a -> 'a;
+ restart_lambda : 'a -> 'a;
+ switch_prod : 'a -> 'a;
+ switch_lambda : 'a -> 'a;
+ slide : 'a -> 'a;
+}
+
+let default_binder_status_fun = {
+ no = (fun x -> x);
+ restart_prod = (fun x -> x);
+ restart_lambda = (fun x -> x);
+ switch_prod = (fun x -> x);
+ switch_lambda = (fun x -> x);
+ slide = (fun x -> x);
+}
+
let protect g e na =
let e',disjpat,na = g e na in
if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
@@ -163,10 +181,10 @@ let apply_cases_pattern_term ?loc (ids,disjpat) tm c =
let apply_cases_pattern ?loc (ids_disjpat,id) c =
apply_cases_pattern_term ?loc ids_disjpat (DAst.make ?loc (GVar id)) c
-let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
+let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_status_fun) e nc =
let lt x = DAst.make ?loc x in lt @@ match nc with
| NVar id -> GVar id
- | NApp (a,args) -> GApp (f e a, List.map (f e) args)
+ | NApp (a,args) -> let e = h.no e in GApp (f e a, List.map (f e) args)
| NList (x,y,iter,tail,swap) ->
let t = f e tail in let it = f e iter in
let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in
@@ -180,15 +198,18 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in
DAst.get (subst_glob_vars outerl it)
| NLambda (na,ty,c) ->
- let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+ let e = h.switch_lambda e in
+ let e',disjpat,na = g e na in GLambda (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
| NProd (na,ty,c) ->
- let e',disjpat,na = g e na in GProd (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+ let e = h.switch_prod e in
+ let e',disjpat,na = g e na in GProd (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
| NLetIn (na,b,t,c) ->
let e',disjpat,na = g e na in
(match disjpat with
- | None -> GLetIn (na,f e b,Option.map (f e) t,f e' c)
+ | None -> GLetIn (na,f (h.restart_lambda e) b,Option.map (f (h.restart_prod e)) t,f e' c)
| Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
| NCases (sty,rtntypopt,tml,eqnl) ->
+ let e = h.no e in
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
let e',t' = match t with
| None -> e',None
@@ -207,19 +228,22 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
List.map (fun patl -> CAst.make (idl,patl,f e rhs)) disjpatl) eqnl in
GCases (sty,Option.map (f e') rtntypopt,tml',List.flatten eqnl')
| NLetTuple (nal,(na,po),b,c) ->
+ let e = h.no e in
let e',nal = List.fold_left_map (protect g) e nal in
let e'',na = protect g e na in
GLetTuple (nal,(na,Option.map (f e'') po),f e b,f e' c)
| NIf (c,(na,po),b1,b2) ->
+ let e = h.no e in
let e',na = protect g e na in
GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2)
| NRec (fk,idl,dll,tl,bl) ->
+ let e = h.no e in
let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) ->
let e,na = protect g e na in
(e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
- | NCast (c,k) -> GCast (f e c,map_cast_type (f e) k)
+ | NCast (c,k) -> GCast (f e c,map_cast_type (f (h.slide e)) k)
| NSort x -> GSort x
| NHole (x, naming, arg) -> GHole (x, naming, arg)
| NRef x -> GRef (x,None)
@@ -234,6 +258,8 @@ let glob_constr_of_notation_constr ?loc x =
(******************************************************************************)
(* Translating a glob_constr into a notation, interpreting recursive patterns *)
+let print_parentheses = ref false
+
type found_variables = {
vars : Id.t list;
recursive_term_vars : (Id.t * Id.t) list;
@@ -1068,6 +1094,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin revert =
let rest = Id.List.assoc ldots_var terms in
let t = Id.List.assoc y terms in
let sigma = remove_sigma y (remove_sigma ldots_var sigma) in
+ if !print_parentheses && not (List.is_empty acc) then raise No_match;
aux sigma (t::acc) rest
with No_match when not (List.is_empty acc) ->
acc, match_fun metas sigma rest termin in
@@ -1340,35 +1367,37 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert =
let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
match DAst.get a1, a2 with
- | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
- | PatVar Anonymous, NHole _ -> sigma,(0,[])
+ | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[])
+ | PatVar Anonymous, NHole _ -> sigma,(false,0,[])
| PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 ->
let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
- sigma,(0,l)
+ sigma,(false,0,l)
| PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2)
when eq_constructor r1 r2 ->
let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) 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
+ if le2 > List.length l1
then
raise No_match
else
let l1',more_args = Util.List.chop le2 l1 in
- (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+ (* Convention: notations to @f don't keep implicit arguments *)
+ let no_implicit = le2 = 0 in
+ (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args)
| r1, NList (x,y,iter,termin,revert) ->
(match_cases_pattern_list (match_cases_pattern_no_more_args)
- metas (terms,termlists,(),()) a1 x y iter termin revert),(0,[])
+ metas (terms,termlists,(),()) a1 x y iter termin revert),(false,0,[])
| _ -> raise No_match
and match_cases_pattern_no_more_args metas sigma a1 a2 =
match match_cases_pattern metas sigma a1 a2 with
- | out,(_,[]) -> out
+ | out,(_,_,[]) -> out
| _ -> raise No_match
let match_ind_pattern metas sigma ind pats a2 =
match a2 with
| NRef (GlobRef.IndRef r2) when eq_ind ind r2 ->
- sigma,(0,pats)
+ sigma,(false,0,pats)
| NApp (NRef (GlobRef.IndRef r2),l2)
when eq_ind ind r2 ->
let le2 = List.length l2 in
@@ -1377,7 +1406,8 @@ let match_ind_pattern metas sigma ind pats a2 =
raise No_match
else
let l1',more_args = Util.List.chop le2 pats in
- (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+ let no_implicit = le2 = 0 in
+ (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args)
|_ -> raise No_match
let reorder_canonically_substitution terms termlists metas =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 06:03:08 +0000