aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml16
-rw-r--r--interp/constrexpr_ops.ml20
-rw-r--r--interp/constrextern.ml559
-rw-r--r--interp/constrintern.ml241
-rw-r--r--interp/constrintern.mli4
-rw-r--r--interp/impargs.ml83
-rw-r--r--interp/impargs.mli5
-rw-r--r--interp/implicit_quantifiers.ml12
-rw-r--r--interp/notation.ml76
-rw-r--r--interp/notation.mli12
-rw-r--r--interp/notation_ops.ml57
-rw-r--r--interp/notation_ops.mli15
-rw-r--r--interp/reserve.ml4
13 files changed, 700 insertions, 404 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index b96ef7c4e5..4bdacda529 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -19,11 +19,21 @@ type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.g
type ident_decl = lident * universe_decl_expr option
type name_decl = lname * universe_decl_expr option
+type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
+
+type entry_level = int
+type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | LevelSome
+
type notation_entry = InConstrEntry | InCustomEntry of string
-type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int
+type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * entry_level
type notation_key = string
+
+(* A notation associated to a given parsing rule *)
type notation = notation_entry_level * notation_key
+(* A notation associated to a given interpretation *)
+type specific_notation = notation_with_optional_scope * notation
+
type 'a or_by_notation_r =
| AN of 'a
| ByNotation of (string * string option)
@@ -78,7 +88,7 @@ type cases_pattern_expr_r =
(** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
| CPatAtom of qualid option
| CPatOr of cases_pattern_expr list
- | CPatNotation of notation * cases_pattern_notation_substitution
+ | CPatNotation of notation_with_optional_scope option * notation * cases_pattern_notation_substitution
* cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
(notation n applied with substitution l1)
applied to arguments l2 *)
@@ -119,7 +129,7 @@ and constr_expr_r =
| CEvar of Glob_term.existential_name * (Id.t * constr_expr) list
| CSort of Glob_term.glob_sort
| CCast of constr_expr * constr_expr Glob_term.cast_type
- | CNotation of notation * constr_notation_substitution
+ | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
| CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
| CPrim of prim_token
| CDelimiters of string * constr_expr
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index b4798127f9..401853b625 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -75,7 +75,8 @@ let rec cases_pattern_expr_eq p1 p2 =
Option.equal qualid_eq r1 r2
| CPatOr a1, CPatOr a2 ->
List.equal cases_pattern_expr_eq a1 a2
- | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) ->
+ | CPatNotation (inscope1, n1, s1, l1), CPatNotation (inscope2, n2, s2, l2) ->
+ Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
notation_eq n1 n2 &&
cases_pattern_notation_substitution_eq s1 s2 &&
List.equal cases_pattern_expr_eq l1 l2
@@ -160,7 +161,8 @@ let rec constr_expr_eq e1 e2 =
Glob_ops.glob_sort_eq s1 s2
| CCast(t1,c1), CCast(t2,c2) ->
constr_expr_eq t1 t2 && cast_expr_eq c1 c2
- | CNotation(n1, s1), CNotation(n2, s2) ->
+ | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) ->
+ Option.equal notation_with_optional_scope_eq inscope1 inscope2 &&
notation_eq n1 n2 &&
constr_notation_substitution_eq s1 s2
| CPrim i1, CPrim i2 ->
@@ -271,7 +273,7 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
| CPatCstr (_,patl1,patl2) ->
List.fold_left (cases_pattern_fold_names f)
(Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2
- | CPatNotation (_,(patl,patll),patl') ->
+ | CPatNotation (_,_,(patl,patll),patl') ->
List.fold_left (cases_pattern_fold_names f)
(List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
| CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
@@ -320,7 +322,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
| CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
| CCast (a,CastCoerce) -> f n acc a
- | CNotation (_,(l,ll,bl,bll)) ->
+ | CNotation (_,_,(l,ll,bl,bll)) ->
(* The following is an approximation: we don't know exactly if
an ident is binding nor to which subterms bindings apply *)
let acc = List.fold_left (f n) acc (l@List.flatten ll) in
@@ -399,9 +401,9 @@ let map_constr_expr_with_binders g f e = CAst.map (function
| CLetIn (na,a,t,b) ->
CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
| CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c)
- | CNotation (n,(l,ll,bl,bll)) ->
+ | CNotation (inscope,n,(l,ll,bl,bll)) ->
(* This is an approximation because we don't know what binds what *)
- CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
+ CNotation (inscope,n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
List.map (fun bl -> snd (map_local_binders f g e bl)) bll))
| CGeneralization (b,a,c) -> CGeneralization (b,a,f e c)
| CDelimiters (s,a) -> CDelimiters (s,f e a)
@@ -574,7 +576,7 @@ let mkAppPattern ?loc p lp =
CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern"
(Pp.str "Nested applications not supported.")
| CPatCstr (r, l1, l2) -> CPatCstr (r, l1 , l2@lp)
- | CPatNotation (n, s, l) -> CPatNotation (n , s, l@lp)
+ | CPatNotation (inscope, n, s, l) -> CPatNotation (inscope, n , s, l@lp)
| _ -> CErrors.user_err
?loc:p.loc ~hdr:"compound_pattern"
(Pp.str "Such pattern cannot have arguments."))
@@ -591,8 +593,8 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
(mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
| CAppExpl ((None,r,i),args) ->
CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[])
- | CNotation (ntn,(c,cl,[],[])) ->
- CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c,
+ | CNotation (inscope,ntn,(c,cl,[],[])) ->
+ CPatNotation (inscope,ntn,(List.map coerce_to_cases_pattern_expr c,
List.map (List.map coerce_to_cases_pattern_expr) cl),[])
| CPrim p ->
CPatPrim p
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index cc0c1e4602..4ec9f17c71 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -63,6 +63,28 @@ let print_universes = Detyping.print_universes
(* This suppresses printing of primitive tokens (e.g. numeral) and notations *)
let print_no_symbol = ref false
+(* This tells to skip types if a variable has this type by default *)
+let print_use_implicit_types =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Printing";"Use";"Implicit";"Types"]
+ ~value:true
+
+(**********************************************************************)
+
+let hole = CAst.make @@ CHole (None, IntroAnonymous, None)
+
+let is_reserved_type na t =
+ not !Flags.raw_print && print_use_implicit_types () &&
+ match na with
+ | Anonymous -> false
+ | Name id ->
+ try
+ let pat = Reserve.find_reserved_type id in
+ let _ = match_notation_constr false t ([],pat) in
+ true
+ with Not_found | No_match -> false
+
(**********************************************************************)
(* Turning notations and scopes on and off for printing *)
module IRuleSet = Set.Make(struct
@@ -75,10 +97,10 @@ let inactive_notations_table =
let inactive_scopes_table =
Summary.ref ~name:"inactive_scopes_table" CString.Set.empty
-let show_scope scopt =
- match scopt with
- | None -> str ""
- | Some sc -> spc () ++ str "in scope" ++ spc () ++ str sc
+let show_scope inscope =
+ match inscope with
+ | LastLonelyNotation -> str ""
+ | NotationInScope sc -> spc () ++ str "in scope" ++ spc () ++ str sc
let _show_inactive_notations () =
begin
@@ -97,8 +119,8 @@ let _show_inactive_notations () =
let _ = Feedback.msg_notice (str "Inactive notations:") in
IRuleSet.iter
(function
- | NotationRule (scopt, ntn) ->
- Feedback.msg_notice (pr_notation ntn ++ show_scope scopt)
+ | NotationRule (inscope, ntn) ->
+ Feedback.msg_notice (pr_notation ntn ++ show_scope inscope)
| SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn))))
!inactive_notations_table
@@ -107,18 +129,19 @@ let deactivate_notation nr =
| SynDefRule kn ->
(* shouldn't we check whether it is well defined? *)
inactive_notations_table := IRuleSet.add nr !inactive_notations_table
- | NotationRule (scopt, ntn) ->
- match availability_of_notation (scopt, ntn) (scopt, []) with
+ | NotationRule (inscope, ntn) ->
+ let scopt = match inscope with NotationInScope sc -> Some sc | LastLonelyNotation -> None in
+ match availability_of_notation (inscope, ntn) (scopt, []) with
| None -> user_err ~hdr:"Notation"
(pr_notation ntn ++ spc () ++ str "does not exist"
- ++ (match scopt with
- | None -> spc () ++ str "in the empty scope."
- | Some _ -> show_scope scopt ++ str "."))
+ ++ (match inscope with
+ | LastLonelyNotation -> spc () ++ str "in the empty scope."
+ | NotationInScope _ -> show_scope inscope ++ str "."))
| Some _ ->
if IRuleSet.mem nr !inactive_notations_table then
Feedback.msg_warning
(str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
- ++ str "is already inactive" ++ show_scope scopt ++ str ".")
+ ++ str "is already inactive" ++ show_scope inscope ++ str ".")
else inactive_notations_table := IRuleSet.add nr !inactive_notations_table
let reactivate_notation nr =
@@ -127,9 +150,9 @@ let reactivate_notation nr =
IRuleSet.remove nr !inactive_notations_table
with Not_found ->
match nr with
- | NotationRule (scopt, ntn) ->
+ | NotationRule (inscope, ntn) ->
Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
- ++ str "is already active" ++ show_scope scopt ++
+ ++ str "is already active" ++ show_scope inscope ++
str ".")
| SynDefRule kn ->
let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in
@@ -157,8 +180,8 @@ let reactivate_scope sc =
let is_inactive_rule nr =
IRuleSet.mem nr !inactive_notations_table ||
match nr with
- | NotationRule (Some sc, ntn) -> CString.Set.mem sc !inactive_scopes_table
- | NotationRule (None, ntn) -> false
+ | NotationRule (NotationInScope sc, ntn) -> CString.Set.mem sc !inactive_scopes_table
+ | NotationRule (LastLonelyNotation, ntn) -> false
| SynDefRule _ -> false
(* args: notation, scope, activate/deactivate *)
@@ -169,10 +192,13 @@ let toggle_scope_printing ~scope ~activate =
deactivate_scope scope
let toggle_notation_printing ?scope ~notation ~activate =
+ let inscope = match scope with
+ | None -> LastLonelyNotation
+ | Some sc -> NotationInScope sc in
if activate then
- reactivate_notation (NotationRule (scope, notation))
+ reactivate_notation (NotationRule (inscope, notation))
else
- deactivate_notation (NotationRule (scope, notation))
+ deactivate_notation (NotationRule (inscope, notation))
(* This governs printing of projections using the dot notation symbols *)
let print_projections = ref false
@@ -194,7 +220,6 @@ let without_specific_symbols l =
let get_record_print =
Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"record printing"
~key:["Printing";"Records"]
~value:true
@@ -255,11 +280,11 @@ let insert_pat_alias ?loc p = function
let rec insert_coercion ?loc l c = match l with
| [] -> c
- | ntn::l -> CAst.make ?loc @@ CNotation (ntn,([insert_coercion ?loc l c],[],[],[]))
+ | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_coercion ?loc l c],[],[],[]))
let rec insert_pat_coercion ?loc l c = match l with
| [] -> c
- | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[])
+ | (inscope,ntn)::l -> CAst.make ?loc @@ CPatNotation (Some inscope,ntn,([insert_pat_coercion ?loc l c],[]),[])
(**********************************************************************)
(* conversion of references *)
@@ -281,6 +306,17 @@ let get_extern_reference () = !my_extern_reference
let extern_reference ?loc vars l = !my_extern_reference vars l
(**********************************************************************)
+(* utilities *)
+
+let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) =
+ match args, subscopes with
+ | [], _ -> []
+ | a :: args, scopt :: subscopes ->
+ (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all
+ | a :: args, [] ->
+ (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all
+
+(**********************************************************************)
(* mapping patterns to cases_pattern_expr *)
let add_patt_for_params ind l =
@@ -338,19 +374,19 @@ let make_notation_gen loc ntn mknot mkprim destprim l bl =
| None -> mknot (loc,ntn,l,bl) end
| _ -> mknot (loc,ntn,l,bl)
-let make_notation loc ntn (terms,termlists,binders,binderlists as subst) =
+let make_notation loc (inscope,ntn) (terms,termlists,binders,binderlists as subst) =
if not (List.is_empty termlists) || not (List.is_empty binderlists) then
- CAst.make ?loc @@ CNotation (ntn,subst)
+ CAst.make ?loc @@ CNotation (Some inscope,ntn,subst)
else
make_notation_gen loc ntn
- (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (ntn,(l,[],bl,[])))
+ (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (Some inscope,ntn,(l,[],bl,[])))
(fun (loc,p) -> CAst.make ?loc @@ CPrim p)
destPrim terms binders
-let make_pat_notation ?loc ntn (terms,termlists as subst) args =
- if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else
+let make_pat_notation ?loc (inscope,ntn) (terms,termlists as subst) args =
+ if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (Some inscope,ntn,subst,args)) else
make_notation_gen loc ntn
- (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args))
+ (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (Some inscope,ntn,(l,[]),args))
(fun (loc,p) -> CAst.make ?loc @@ CPatPrim p)
destPatPrim terms []
@@ -367,6 +403,36 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
(List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
) impl_st
+let extern_record_pattern cstrsp args =
+ try
+ if !Flags.raw_print then raise Exit;
+ let projs = Recordops.lookup_projections (fst cstrsp) in
+ if PrintingRecord.active (fst cstrsp) then
+ ()
+ else if PrintingConstructor.active (fst cstrsp) then
+ raise Exit
+ else if not (get_record_print ()) then
+ raise Exit;
+ let rec ip projs args acc =
+ match projs, args with
+ | [], [] -> acc
+ | proj :: q, pat :: tail ->
+ let acc =
+ match proj, pat with
+ | _, { CAst.v = CPatAtom None } ->
+ (* we don't want to have 'x := _' in our patterns *)
+ acc
+ | Some c, _ ->
+ let loc = pat.CAst.loc in
+ (extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc
+ | _ -> raise No_match in
+ ip q tail acc
+ | _ -> assert false
+ in
+ Some (List.rev (ip projs args []))
+ with
+ Not_found | No_match | Exit -> None
+
(* Better to use extern_glob_constr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
try
@@ -401,27 +467,9 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
| PatCstr(cstrsp,args,na) ->
let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
let p =
- try
- if !Flags.raw_print then raise Exit;
- let projs = Recordops.lookup_projections (fst cstrsp) in
- let rec ip projs args acc =
- match projs, args with
- | [], [] -> acc
- | proj :: q, pat :: tail ->
- let acc =
- match proj, pat with
- | _, { CAst.v = CPatAtom None } ->
- (* we don't want to have 'x := _' in our patterns *)
- acc
- | Some c, _ ->
- ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc)
- | _ -> raise No_match in
- ip q tail acc
- | _ -> assert false
- in
- CPatRecord(List.rev (ip projs args []))
- with
- Not_found | No_match | Exit ->
+ match extern_record_pattern cstrsp args with
+ | Some l -> CPatRecord l
+ | None ->
let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in
if Constrintern.get_asymmetric_patterns () then
if pattern_printable_in_both_syntax cstrsp
@@ -437,15 +485,15 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
in
insert_pat_coercion coercion pat
-and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
+and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop,more_args))
(custom, (tmp_scope, scopes) as allscopes) vars =
function
- | NotationRule (sc,ntn) ->
+ | NotationRule (_,ntn as specific_ntn) ->
begin
match availability_of_entry_coercion custom (fst ntn) with
| None -> raise No_match
| Some coercion ->
- match availability_of_notation (sc,ntn) (tmp_scope,scopes) with
+ match availability_of_notation specific_ntn (tmp_scope,scopes) with
(* Uninterpretation is not allowed in current context *)
| None -> raise No_match
(* Uninterpretation is allowed in current context *)
@@ -460,16 +508,20 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
let subscope = (subentry,(scopt,scl@scopes')) in
List.map (extern_cases_pattern_in_scope subscope vars) c)
substlist in
- let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
+ let subscopes = find_arguments_scope gr in
+ let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in
+ let more_args = fill_arg_scopes more_args more_args_scopes allscopes in
+ let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2
else
- match drop_implicits_in_patt gr nb_to_drop l2 with
+ if no_implicit then l2 else
+ match drop_implicits_in_patt gr nb_to_drop l2 with
|Some true_args -> true_args
|None -> raise No_match
in
insert_pat_coercion coercion
(insert_pat_delimiters ?loc
- (make_pat_notation ?loc ntn (l,ll) l2') key)
+ (make_pat_notation ?loc specific_ntn (l,ll) l2') key)
end
| SynDefRule kn ->
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
@@ -480,10 +532,14 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
List.rev_map (fun (c,(subentry,(scopt,scl))) ->
extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
subst in
- let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
+ let subscopes = find_arguments_scope gr in
+ let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in
+ let more_args = fill_arg_scopes more_args more_args_scopes allscopes in
+ let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
let l2' = if Constrintern.get_asymmetric_patterns () then l2
else
- match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
+ if no_implicit then l2 else
+ match drop_implicits_in_patt gr nb_to_drop l2 with
|Some true_args -> true_args
|None -> raise No_match
in
@@ -550,14 +606,14 @@ let is_gvar id c = match DAst.get c with
| GVar id' -> Id.equal id id'
| _ -> false
-let is_projection nargs = function
- | Some r when not !Flags.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
+let is_projection nargs r =
+ if not !Flags.in_debugger && not !Flags.raw_print && !print_projections then
+ try
+ let n = Recordops.find_projection_nparams r + 1 in
+ if n <= nargs then Some n
+ else None
+ with Not_found -> None
+ else None
let is_hole = function CHole _ | CEvar _ -> true | _ -> false
@@ -569,11 +625,12 @@ let is_needed_for_correct_partial_application tail 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 inctx impl (cf,f) args =
- let impl = if !Constrintern.parsing_explicit then [] else impl in
- let n = List.length args in
+(* Take a list of arguments starting at position [q] and their implicit status *)
+(* Decide for each implicit argument if it skipped or made explicit *)
+(* If the removal of implicit arguments is not possible, raise [Expl] *)
+(* [inctx] tells if the term is in a context which will enforce the external type *)
+(* [n] is the total number of arguments block to which the [args] belong *)
+let adjust_implicit_arguments inctx n q args impl =
let rec exprec q = function
| a::args, imp::impl when is_status_implicit imp ->
let tail = exprec (q+1) (args,impl) in
@@ -595,10 +652,11 @@ let explicitize inctx impl (cf,f) args =
(* The non-explicit application cannot be parsed back with the same type *)
raise Expl
| [], _ -> []
- in
+ in exprec q (args,impl)
+
+let extern_projection (cf,f) args impl =
let ip = is_projection (List.length args) cf in
- let expl () =
- match ip with
+ match ip with
| Some i ->
(* Careful: It is possible to have declared implicits ending
before the principal argument *)
@@ -607,33 +665,61 @@ let explicitize inctx impl (cf,f) args =
with Failure _ -> false
in
if is_impl
- then raise Expl
+ then None
else
let (args1,args2) = List.chop i args in
let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in
- let args1 = exprec 1 (args1,impl1) in
- let args2 = exprec (i+1) (args2,impl2) in
- let ip = Some (List.length args1) in
- CApp ((ip,f),args1@args2)
- | None ->
- let args = exprec 1 (args,impl) in
- if List.is_empty args then f.CAst.v else
- match f.CAst.v with
- | CApp (g,args') ->
- (* may happen with notations for a prefix of an n-ary
- application *)
- CApp (g,args'@args)
- | _ -> CApp ((None, f), args) in
- try expl ()
- with Expl ->
- let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in
- let ip = if !print_projections then ip else None in
- CAppExpl ((ip, f', us), List.map Lazy.force args)
+ Some (i,(args1,impl1),(args2,impl2))
+ | None -> None
let is_start_implicit = function
| imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
| [] -> false
+let extern_record ref args =
+ try
+ if !Flags.raw_print then raise Exit;
+ let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
+ let struc = Recordops.lookup_structure (fst cstrsp) in
+ if PrintingRecord.active (fst cstrsp) then
+ ()
+ else if PrintingConstructor.active (fst cstrsp) then
+ raise Exit
+ else if not (get_record_print ()) then
+ raise Exit;
+ let projs = struc.Recordops.s_PROJ in
+ let locals = struc.Recordops.s_PROJKIND in
+ let rec cut args n =
+ if Int.equal n 0 then args
+ else
+ match args with
+ | [] -> raise No_match
+ | _ :: t -> cut t (n - 1) in
+ let args = cut args struc.Recordops.s_EXPECTEDPARAM in
+ let rec ip projs locs args acc =
+ match projs with
+ | [] -> acc
+ | None :: q -> raise No_match
+ | Some c :: q ->
+ match locs with
+ | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
+ | { Recordops.pk_true_proj = false } :: locs' ->
+ (* we don't want to print locals *)
+ ip q locs' args acc
+ | { Recordops.pk_true_proj = true } :: locs' ->
+ match args with
+ | [] -> raise No_match
+ (* we give up since the constructor is not complete *)
+ | arg :: tail ->
+ let arg = Lazy.force arg in
+ let loc = arg.CAst.loc in
+ let ref = extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c) in
+ ip q locs' tail ((ref, arg) :: acc)
+ in
+ Some (List.rev (ip projs locals args []))
+ with
+ | Not_found | No_match | Exit -> None
+
let extern_global impl f us =
if not !Constrintern.parsing_explicit && is_start_implicit impl
then
@@ -641,26 +727,65 @@ let extern_global impl f us =
else
CRef (f,us)
-let extern_app inctx impl (cf,f) us args =
- if List.is_empty args then
- (* If coming from a notation "Notation a := @b" *)
- CAppExpl ((None, f, us), [])
- else if not !Constrintern.parsing_explicit &&
- ((!Flags.raw_print ||
- (!print_implicits && not !print_implicits_explicit_args)) &&
- List.exists is_status_implicit impl)
- then
+(* Implicit args indexes are in ascending order *)
+(* inctx is useful only if there is a last argument to be deduced from ctxt *)
+let extern_applied_ref inctx impl (cf,f) us args =
+ let isproj = is_projection (List.length args) cf in
+ try
+ if not !Constrintern.parsing_explicit &&
+ ((!Flags.raw_print ||
+ (!print_implicits && not !print_implicits_explicit_args)) &&
+ List.exists is_status_implicit impl)
+ then raise Expl;
+ let impl = if !Constrintern.parsing_explicit then [] else impl in
+ let n = List.length args in
+ let ref = CRef (f,us) in
+ let f = CAst.make ref in
+ match extern_projection (cf,f) args impl with
+ (* Try a [t.(f args1) args2] projection-style notation *)
+ | Some (i,(args1,impl1),(args2,impl2)) ->
+ let args1 = adjust_implicit_arguments inctx n 1 args1 impl1 in
+ let args2 = adjust_implicit_arguments inctx n (i+1) args2 impl2 in
+ let ip = Some (List.length args1) in
+ CApp ((ip,f),args1@args2)
+ (* A normal application node with each individual implicit
+ arguments either dropped or made explicit *)
+ | None ->
+ let args = adjust_implicit_arguments inctx n 1 args impl in
+ if args = [] then ref else CApp ((None, f), args)
+ with Expl ->
+ (* A [@f args] node *)
let args = List.map Lazy.force args in
- CAppExpl ((is_projection (List.length args) cf,f,us), args)
- else
- explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args
+ let isproj = if !print_projections then isproj else None in
+ CAppExpl ((isproj,f,us), args)
-let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) = match args, subscopes with
-| [], _ -> []
-| a :: args, scopt :: subscopes ->
- (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all
-| a :: args, [] ->
- (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all
+let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs =
+ try
+ let syndefargs = List.map (fun a -> (a,None)) syndefargs in
+ let extraargs = adjust_implicit_arguments false n (n-List.length extraargs+1) extraargs extraimpl in
+ let args = syndefargs @ extraargs in
+ if args = [] then cf else CApp ((None, CAst.make cf), args)
+ with Expl ->
+ let args = syndefargs @ List.map Lazy.force extraargs in
+ CAppExpl ((None,f,None), args)
+
+let mkFlattenedCApp (head,args) =
+ match head.CAst.v with
+ | CApp (g,args') ->
+ (* may happen with notations for a prefix of an n-ary application *)
+ (* or after removal of a coercion to funclass *)
+ CApp (g,args'@args)
+ | _ ->
+ CApp ((None, head), args)
+
+let extern_applied_notation n impl f args =
+ if List.is_empty args then
+ f.CAst.v
+ else
+ try
+ let args = adjust_implicit_arguments false n (n-List.length args+1) args impl in
+ mkFlattenedCApp (f,args)
+ with Expl -> raise No_match
let extern_args extern env args =
let map (arg, argscopes) = lazy (extern argscopes env arg) in
@@ -709,6 +834,12 @@ let rec flatten_application c = match DAst.get c with
end
| a -> c
+let same_binder_type ty nal c =
+ match nal, DAst.get c with
+ | _::_, GProd (_,_,ty',_) -> glob_constr_eq ty ty'
+ | [], _ -> true
+ | _ -> assert false
+
(**********************************************************************)
(* mapping glob_constr to numerals (in presence of coercions, choose the *)
(* one with no delimiter if possible) *)
@@ -838,56 +969,19 @@ let rec extern inctx scopes vars r =
| GRef (ref,us) ->
let subscopes = find_arguments_scope ref in
let args = fill_arg_scopes args subscopes scopes in
- begin
- try
- if !Flags.raw_print then raise Exit;
- let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in
- let struc = Recordops.lookup_structure (fst cstrsp) in
- if PrintingRecord.active (fst cstrsp) then
- ()
- else if PrintingConstructor.active (fst cstrsp) then
- raise Exit
- else if not (get_record_print ()) then
- raise Exit;
- let projs = struc.Recordops.s_PROJ in
- let locals = struc.Recordops.s_PROJKIND in
- let rec cut args n =
- if Int.equal n 0 then args
- else
- match args with
- | [] -> raise No_match
- | _ :: t -> cut t (n - 1) in
- let args = cut args struc.Recordops.s_EXPECTEDPARAM in
- let rec ip projs locs args acc =
- match projs with
- | [] -> acc
- | None :: q -> raise No_match
- | Some c :: q ->
- match locs with
- | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
- | { Recordops.pk_true_proj = false } :: locs' ->
- (* we don't want to print locals *)
- ip q locs' args acc
- | { Recordops.pk_true_proj = true } :: locs' ->
- match args with
- | [] -> raise No_match
- (* we give up since the constructor is not complete *)
- | (arg, scopes) :: tail ->
- let head = extern true scopes vars arg in
- ip q locs' tail ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), head) :: acc)
- in
- CRecord (List.rev (ip projs locals args []))
- with
- | Not_found | No_match | Exit ->
- let args = extern_args (extern true) vars args in
- extern_app inctx
- (select_stronger_impargs (implicits_of_global ref))
- (Some ref,extern_reference ?loc vars ref) (extern_universes us) args
- end
-
- | _ ->
- explicitize inctx [] (None,sub_extern false scopes vars f)
- (List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
+ let args = extern_args (extern true) vars args in
+ (* Try a "{|...|}" record notation *)
+ (match extern_record ref args with
+ | Some l -> CRecord l
+ | None ->
+ (* Otherwise... *)
+ extern_applied_ref inctx
+ (select_stronger_impargs (implicits_of_global ref))
+ (ref,extern_reference ?loc vars ref) (extern_universes us) args)
+ | _ ->
+ let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in
+ let head = sub_extern false scopes vars f in
+ mkFlattenedCApp (head,args))
| GLetIn (na,b,t,c) ->
CLetIn (make ?loc na,sub_extern false scopes vars b,
@@ -895,12 +989,10 @@ let rec extern inctx scopes vars r =
extern inctx scopes (add_vname vars na) c)
| GProd (na,bk,t,c) ->
- let t = extern_typ scopes vars t in
- factorize_prod scopes (add_vname vars na) na bk t c
+ factorize_prod scopes vars na bk t c
| GLambda (na,bk,t,c) ->
- let t = extern_typ scopes vars t in
- factorize_lambda inctx scopes (add_vname vars na) na bk t c
+ factorize_lambda inctx scopes vars na bk t c
| GCases (sty,rtntypopt,tml,eqns) ->
let vars' =
@@ -929,17 +1021,19 @@ let rec extern inctx scopes vars r =
) x))
tml
in
- let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in
+ let eqns = List.map (extern_eqn (inctx || rtntypopt <> None) scopes vars) (factorize_eqns eqns) in
CCases (sty,rtntypopt',tml,eqns)
| GLetTuple (nal,(na,typopt),tm,b) ->
- CLetTuple (List.map CAst.make nal,
+ let inctx = inctx || typopt <> None in
+ CLetTuple (List.map CAst.make nal,
(Option.map (fun _ -> (make na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern false scopes vars tm,
extern inctx scopes (List.fold_left add_vname vars nal) b)
| GIf (c,(na,typopt),b1,b2) ->
+ let inctx = inctx || typopt <> None in
CIf (sub_extern false scopes vars c,
(Option.map (fun _ -> (CAst.make na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
@@ -962,7 +1056,7 @@ let rec extern inctx scopes vars r =
| Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x)))
in
((CAst.make fi), n, bl, extern_typ scopes vars0 ty,
- extern false scopes vars1 def)) idv
+ sub_extern true scopes vars1 def)) idv
in
CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
| GCoFix n ->
@@ -973,7 +1067,7 @@ let rec extern inctx scopes vars r =
let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i),
- sub_extern false scopes vars1 bv.(i))) idv
+ sub_extern true scopes vars1 bv.(i))) idv
in
CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl))
@@ -999,7 +1093,10 @@ and extern_typ (subentry,(_,scopes)) =
and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes))
-and factorize_prod scopes vars na bk aty c =
+and factorize_prod scopes vars na bk t c =
+ let implicit_type = is_reserved_type na t in
+ let aty = extern_typ scopes vars t in
+ let vars = add_vname vars na in
let store, get = set_temporary_memory () in
match na, DAst.get c with
| Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
@@ -1016,18 +1113,25 @@ and factorize_prod scopes vars na bk aty c =
| _ -> CProdN ([binder],b))
| _ -> assert false)
| _, _ ->
- let c = extern_typ scopes vars c in
- match na, c.v with
+ let c' = extern_typ scopes vars c in
+ match na, c'.v with
| Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b)
- when binding_kind_eq bk bk' && constr_expr_eq aty ty
- && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
- CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b)
+ when binding_kind_eq bk bk'
+ && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *)
+ && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) ->
+ let ty = if implicit_type then ty else aty in
+ CProdN (CLocalAssum(make na::nal,Default bk,ty)::bl,b)
| _, CProdN (bl,b) ->
- CProdN (CLocalAssum([make na],Default bk,aty)::bl,b)
+ let ty = if implicit_type then hole else aty in
+ CProdN (CLocalAssum([make na],Default bk,ty)::bl,b)
| _, _ ->
- CProdN ([CLocalAssum([make na],Default bk,aty)],c)
+ let ty = if implicit_type then hole else aty in
+ CProdN ([CLocalAssum([make na],Default bk,ty)],c')
-and factorize_lambda inctx scopes vars na bk aty c =
+and factorize_lambda inctx scopes vars na bk t c =
+ let implicit_type = is_reserved_type na t in
+ let aty = extern_typ scopes vars t in
+ let vars = add_vname vars na in
let store, get = set_temporary_memory () in
match na, DAst.get c with
| Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
@@ -1044,16 +1148,20 @@ and factorize_lambda inctx scopes vars na bk aty c =
| _ -> CLambdaN ([binder],b))
| _ -> assert false)
| _, _ ->
- let c = sub_extern inctx scopes vars c in
- match c.v with
+ let c' = sub_extern inctx scopes vars c in
+ match c'.v with
| CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b)
- when binding_kind_eq bk bk' && constr_expr_eq aty ty
- && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
+ when binding_kind_eq bk bk'
+ && not (occur_name na ty) (* avoid na in ty escapes scope *)
+ && (constr_expr_eq aty ty || (constr_expr_eq ty hole && same_binder_type t nal c)) ->
+ let aty = if implicit_type then ty else aty in
CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b)
| CLambdaN (bl,b) ->
- CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b)
+ let ty = if implicit_type then hole else aty in
+ CLambdaN (CLocalAssum([make na],Default bk,ty)::bl,b)
| _ ->
- CLambdaN ([CLocalAssum([make na],Default bk,aty)],c)
+ let ty = if implicit_type then hole else aty in
+ CLambdaN ([CLocalAssum([make na],Default bk,ty)],c')
and extern_local_binder scopes vars = function
[] -> ([],[],[])
@@ -1067,15 +1175,17 @@ and extern_local_binder scopes vars = function
Option.map (extern false scopes vars) ty) :: l)
| GLocalAssum (na,bk,ty) ->
+ let implicit_type = is_reserved_type na ty in
let ty = extern_typ scopes vars ty in
(match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with
(assums,ids,CLocalAssum(nal,k,ty')::l)
- when constr_expr_eq ty ty' &&
+ when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) &&
match na with Name id -> not (occur_var_constr_expr id ty')
| _ -> true ->
(na::assums,na::ids,
CLocalAssum(CAst.make na::nal,k,ty')::l)
| (assums,ids,l) ->
+ let ty = if implicit_type then hole else ty in
(na::assums,na::ids,
CLocalAssum([CAst.make na],Default bk,ty) :: l))
@@ -1104,51 +1214,47 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
let loc = Glob_ops.loc_of_glob_constr t in
try
if is_inactive_rule keyrule then raise No_match;
- (* Adjusts to the number of arguments expected by the notation *)
- let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with
- | GApp (f,args), Some n
- when List.length args >= n ->
+ let f,args =
+ match DAst.get t with
+ | GApp (f,args) -> f,args
+ | _ -> t,[] in
+ let nallargs = List.length args in
+ let argsscopes,argsimpls =
+ match DAst.get f with
+ | GRef (ref,_) ->
+ let subscopes = find_arguments_scope ref in
+ let impls = select_impargs_size nallargs (implicits_of_global ref) in
+ subscopes, impls
+ | _ ->
+ [], [] in
+ (* Adjust to the number of arguments expected by the notation *)
+ let (t,args,argsscopes,argsimpls) = match n with
+ | Some n when nallargs >= n ->
let args1, args2 = List.chop n args in
- let subscopes, impls =
- match DAst.get f with
- | GRef (ref,us) ->
- let subscopes =
- try List.skipn n (find_arguments_scope ref)
- with Failure _ -> [] in
- let impls =
- let impls =
- select_impargs_size
- (List.length args) (implicits_of_global ref) in
- try List.skipn n impls with Failure _ -> [] in
- subscopes,impls
- | _ ->
- [], [] in
- (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
- args2, subscopes, impls
- | GApp (f, args), None ->
+ let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
+ let args2impls =
+ if n = 0 then
+ (* Note: NApp(NRef f,[]), hence n=0, encodes @f and
+ conventionally deactivates implicit arguments *)
+ []
+ else try List.skipn n argsimpls with Failure _ -> [] in
+ DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
+ | None ->
begin match DAst.get f with
- | GRef (ref,us) ->
- let subscopes = find_arguments_scope ref in
- let impls =
- select_impargs_size
- (List.length args) (implicits_of_global ref) in
- f, args, subscopes, impls
+ | GRef (ref,us) -> f, args, argsscopes, argsimpls
| _ -> t, [], [], []
end
- | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], []
- | _, None -> t, [], [], []
| _ -> raise No_match in
(* Try matching ... *)
let terms,termlists,binders,binderlists =
match_notation_constr !print_universes t pat in
(* Try availability of interpretation ... *)
- let e =
- match keyrule with
- | NotationRule (sc,ntn) ->
+ match keyrule with
+ | NotationRule (_,ntn as specific_ntn) ->
(match availability_of_entry_coercion custom (fst ntn) with
| None -> raise No_match
| Some coercion ->
- match availability_of_notation (sc,ntn) scopes with
+ match availability_of_notation specific_ntn scopes with
(* Uninterpretation is not allowed in current context *)
| None -> raise No_match
(* Uninterpretation is allowed in current context *)
@@ -1171,22 +1277,25 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
List.map (fun (bl,(subentry,(scopt,scl))) ->
pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
binderlists in
- insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key))
+ let c = make_notation loc specific_ntn (l,ll,bl,bll) in
+ let c = insert_coercion coercion (insert_delimiters c key) in
+ let args = fill_arg_scopes args argsscopes allscopes in
+ let args = extern_args (extern true) vars args in
+ CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args)
| SynDefRule kn ->
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
| Some coercion ->
let l =
List.map (fun (c,(subentry,(scopt,scl))) ->
- extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
+ extern true (subentry,(scopt,scl@snd scopes)) vars c)
terms in
- let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in
- insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in
- if List.is_empty args then e
- else
- let args = fill_arg_scopes args argsscopes allscopes in
- let args = extern_args (extern true) vars args in
- CAst.make ?loc @@ explicitize false argsimpls (None,e) args
+ let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in
+ let a = CRef (cf,None) in
+ let args = fill_arg_scopes args argsscopes allscopes in
+ let args = extern_args (extern true) vars args in
+ let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in
+ insert_coercion coercion c
with
No_match -> extern_notation allscopes vars t rules
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c699f79351..c39e61083d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -226,7 +226,7 @@ let contract_curly_brackets ntn (l,ll,bl,bll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | { CAst.v = CNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l ->
+ | { CAst.v = CNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -242,7 +242,7 @@ let contract_curly_brackets_pat ntn (l,ll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | { CAst.v = CPatNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l ->
+ | { CAst.v = CPatNotation (None,(InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -257,7 +257,7 @@ type intern_env = {
tmp_scope: Notation_term.tmp_scope_name option;
scopes: Notation_term.scope_name list;
impls: internalization_env;
- impl_binder_index: int option;
+ binder_block_names: (abstraction_kind option (* None = unknown *) * Id.Set.t) option;
}
(**********************************************************************)
@@ -330,15 +330,18 @@ let exists_name na l =
| _ -> false
let build_impls ?loc n bk na acc =
- match bk with
- | Implicit ->
+ let impl_status max =
let na =
- if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
- else na in
+ if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
+ else na in
let impl = match na with
- | Name id -> Some (ExplByName id,Manual,(true,true))
- | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in
- impl :: acc
+ | Name id -> Some (ExplByName id,Manual,(max,true))
+ | Anonymous -> Some (ExplByPos (n,None),Manual,(max,true)) in
+ impl
+ in
+ match bk with
+ | NonMaxImplicit -> impl_status false :: acc
+ | MaxImplicit -> impl_status true :: acc
| Explicit -> None :: acc
let impls_binder_list =
@@ -373,6 +376,49 @@ let rec check_capture ty = let open CAst in function
| [] ->
()
+(** Status of the internalizer wrt "Arguments" of names *)
+
+let restart_no_binders env =
+ { env with binder_block_names = None}
+ (* Not in relation with the "Arguments" of a name *)
+
+let restart_prod_binders env =
+ { env with binder_block_names = Some (Some AbsPi, Id.Set.empty) }
+ (* In a position binding a type to a name *)
+
+let restart_lambda_binders env =
+ { env with binder_block_names = Some (Some AbsLambda, Id.Set.empty) }
+ (* In a position binding a body to a name *)
+
+let switch_prod_binders env =
+ match env.binder_block_names with
+ | Some (o,ids) when o <> Some AbsLambda -> restart_prod_binders env
+ | _ -> restart_no_binders env
+ (* In a position switching to a type *)
+
+let switch_lambda_binders env =
+ match env.binder_block_names with
+ | Some (o,ids) when o <> Some AbsPi -> restart_lambda_binders env
+ | _ -> restart_no_binders env
+ (* In a position switching to a term *)
+
+let slide_binders env =
+ match env.binder_block_names with
+ | Some (o,ids) when o <> Some AbsPi -> restart_prod_binders env
+ | _ -> restart_no_binders env
+ (* In a position of cast *)
+
+let binder_status_fun = {
+ no = (fun x -> x);
+ restart_prod = on_snd restart_prod_binders;
+ restart_lambda = on_snd restart_lambda_binders;
+ switch_prod = on_snd switch_prod_binders;
+ switch_lambda = on_snd switch_lambda_binders;
+ slide = on_snd slide_binders;
+}
+
+(**)
+
let locate_if_hole ?loc na c = match DAst.get c with
| GHole (_,naming,arg) ->
(try match na with
@@ -397,7 +443,11 @@ let check_hidden_implicit_parameters ?loc id impls =
strbrk "the type of a constructor shall use a different name.")
let pure_push_name_env (id,implargs) env =
- {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
+ {env with
+ ids = Id.Set.add id env.ids;
+ impls = Id.Map.add id implargs env.impls;
+ binder_block_names = Option.map (fun (b,ids) -> (b,Id.Set.add id ids)) env.binder_block_names;
+ }
let push_name_env ntnvars implargs env =
let open CAst in
@@ -421,13 +471,15 @@ let remember_binders_impargs env bl =
let restore_binders_impargs env l =
List.fold_right pure_push_name_env l env
-let warn_unexpected_implicit_binder_declaration =
+let warn_ignoring_unexpected_implicit_binder_declaration =
CWarnings.create ~name:"unexpected-implicit-declaration" ~category:"syntax"
- Pp.(fun () -> str "Unexpected implicit binder declaration.")
+ Pp.(fun () -> str "Ignoring implicit binder declaration in unexpected position.")
let check_implicit_meaningful ?loc k env =
- if k = Implicit && env.impl_binder_index = None then
- warn_unexpected_implicit_binder_declaration ?loc ()
+ if k <> Explicit && env.binder_block_names = None then
+ (warn_ignoring_unexpected_implicit_binder_declaration ?loc (); Explicit)
+ else
+ k
let intern_generalized_binder intern_type ntnvars
env {loc;v=na} b' t ty =
@@ -441,10 +493,10 @@ let intern_generalized_binder intern_type ntnvars
let env' = List.fold_left
(fun env {loc;v=x} -> push_name_env ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x))
env fvs in
- check_implicit_meaningful ?loc b' env;
+ let b' = check_implicit_meaningful ?loc b' env in
let bl = List.map
CAst.(map (fun id ->
- (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
+ (Name id, MaxImplicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
fvs
in
let na = match na with
@@ -463,7 +515,7 @@ let intern_generalized_binder intern_type ntnvars
(make ?loc (na,b',ty')) :: List.rev bl)
let intern_assumption intern ntnvars env nal bk ty =
- let intern_type env = intern (set_type_scope env) in
+ let intern_type env = intern (restart_prod_binders (set_type_scope env)) in
match bk with
| Default k ->
let ty = intern_type env ty in
@@ -471,7 +523,7 @@ let intern_assumption intern ntnvars env nal bk ty =
let impls = impls_type_list 1 ty in
List.fold_left
(fun (env, bl) ({loc;v=na} as locna) ->
- check_implicit_meaningful ?loc k env;
+ let k = check_implicit_meaningful ?loc k env in
(push_name_env ntnvars impls env locna,
(make ?loc (na,k,locate_if_hole ?loc na ty))::bl))
(env, []) nal
@@ -492,8 +544,8 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) =
- let term = intern env def in
- let ty = Option.map (intern env) ty in
+ let term = intern (reset_tmp_scope (restart_lambda_binders env)) def in
+ let ty = Option.map (intern (set_type_scope (restart_prod_binders env))) ty in
let impls = impls_term_list 1 term in
(push_name_env ntnvars impls env locna,
(na,Explicit,term,ty))
@@ -585,6 +637,14 @@ let rec expand_binders ?loc mk bl c =
(**********************************************************************)
(* Syntax extensions *)
+let check_not_notation_variable f ntnvars =
+ (* Check bug #4690 *)
+ match DAst.get f with
+ | GVar id when Id.Map.mem id ntnvars ->
+ user_err (str "Prefix @ is not applicable to notation variables.")
+ | _ ->
+ ()
+
let option_mem_assoc id = function
| Some (id',c) -> Id.equal id id'
| None -> false
@@ -713,6 +773,19 @@ let flatten_binders bl =
| a -> [a] in
List.flatten (List.map dispatch bl)
+let rec adjust_env env = function
+ (* We need to adjust scopes, binder blocks ... to the env expected
+ at the recursive occurrence; We do an underapproximation... *)
+ | NProd (_,_,c) -> adjust_env (switch_prod_binders env) c
+ | NLambda (_,_,c) -> adjust_env (switch_lambda_binders env) c
+ | NLetIn (_,_,_,c) -> adjust_env env c
+ | NVar id when Id.equal id ldots_var -> env
+ | NCast (c,_) -> adjust_env env c
+ | NApp _ -> restart_no_binders env
+ | NVar _ | NRef _ | NHole _ | NCases _ | NLetTuple _ | NIf _
+ | NRec _ | NSort _ | NInt _ | NFloat _
+ | NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *)
+
let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
let (terms,termlists,binders,binderlists) = subst in
(* when called while defining a notation, avoid capturing the private binders
@@ -725,7 +798,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
let rec aux_letin env = function
| [],terminator,_ -> aux (terms,None,None) (renaming,env) terminator
| AddPreBinderIter (y,binder)::rest,terminator,iter ->
- let env,binders = intern_local_binder_aux intern ntnvars (env,[]) binder in
+ let env,binders = intern_local_binder_aux intern ntnvars (adjust_env env iter,[]) binder in
let binder,extra = flatten_generalized_binders_if_any y binders in
aux (terms,Some (y,binder),Some (extra@rest,terminator,iter)) (renaming,env) iter
| AddBinderIter (y,binder)::rest,terminator,iter ->
@@ -733,7 +806,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
| AddTermIter nterms::rest,terminator,iter ->
aux (nterms,None,Some (rest,terminator,iter)) (renaming,env) iter
| AddLetIn (na,c,t)::rest,terminator,iter ->
- let env,(na,_,c,t) = intern_letin_binder intern ntnvars env (na,c,t) in
+ let env,(na,_,c,t) = intern_letin_binder intern ntnvars (adjust_env env iter) (na,c,t) in
DAst.make ?loc (GLetIn (na,c,t,aux_letin env (rest,terminator,iter))) in
aux_letin env (Option.get iteropt)
| NVar id -> subst_var subst' (renaming, env) id
@@ -823,7 +896,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c'))
| t ->
glob_constr_of_notation_constr_with_binders ?loc
- (traverse_binder intern_pat ntnvars subst avoid) (aux subst') subinfos t
+ (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t
and subst_var (terms, binderopt, _terminopt) (renaming, env) id =
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
@@ -1006,11 +1079,11 @@ let find_appl_head_data c =
c, impls, scopes, []
| GApp (r, l) ->
begin match DAst.get r with
- | GRef (ref,_) when l != [] ->
+ | GRef (ref,_) ->
let n = List.length l in
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
- c, List.map (drop_first_implicits n) impls,
+ c, (if n = 0 then [] else List.map (drop_first_implicits n) impls),
List.skipn_at_least n scopes,[]
| _ -> c,[],[],[]
end
@@ -1144,7 +1217,7 @@ let interp_reference vars r =
intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None)
{ids = Id.Set.empty; unb = false ;
tmp_scope = None; scopes = []; impls = empty_internalization_env;
- impl_binder_index = None}
+ binder_block_names = None}
Environ.empty_named_context_val
(vars, Id.Map.empty) None [] r
in r
@@ -1550,7 +1623,6 @@ let is_non_zero_pat c = match c with
let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
~depr:false
- ~name:"no parameters in constructors"
~key:["Asymmetric";"Patterns"]
~value:false
@@ -1595,10 +1667,11 @@ let drop_notations_pattern looked_for genv =
let () = assert (List.is_empty vars) in
let (_,argscs) = find_remaining_scopes [] pats g in
Some (g, [], List.map2 (in_pat_sc scopes) argscs pats)
- | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *)
+ | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
test_kind top g;
let () = assert (List.is_empty vars) in
- Some (g, List.map (in_pat false scopes) pats, [])
+ let (_,argscs) = find_remaining_scopes [] pats g in
+ Some (g, List.map2 (in_pat_sc scopes) argscs pats, [])
| NApp (NRef g,args) ->
(* Convention: do not deactivate implicit arguments and scopes for further arguments *)
test_kind top g;
@@ -1616,7 +1689,7 @@ let drop_notations_pattern looked_for genv =
test_kind top g;
Dumpglob.add_glob ?loc:qid.loc g;
let (_,argscs) = find_remaining_scopes [] pats g in
- Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
+ Some (g,[],List.map2 (in_pat_sc scopes) argscs pats)
with Not_found -> None
and in_pat top scopes pt =
let open CAst in
@@ -1643,7 +1716,7 @@ let drop_notations_pattern looked_for genv =
| Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
| None -> raise (InternalizationError (loc,NotAConstructor head))
end
- | CPatCstr (qid, Some expl_pl, pl) ->
+ | CPatCstr (qid, Some expl_pl, pl) ->
let g = try Nametab.locate qid
with Not_found ->
raise (InternalizationError (loc,NotAConstructor qid)) in
@@ -1655,13 +1728,13 @@ let drop_notations_pattern looked_for genv =
(* but not scopes in expl_pl *)
let (argscs1,_) = find_remaining_scopes expl_pl pl g in
DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
- | CPatNotation ((InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
+ | CPatNotation (_,(InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a ->
let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in
let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in
rcp_of_glob scopes pat
- | CPatNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
+ | CPatNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
in_pat top scopes a
- | CPatNotation (ntn,fullargs,extrargs) ->
+ | CPatNotation (_,ntn,fullargs,extrargs) ->
let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in
let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in
@@ -1716,7 +1789,15 @@ let drop_notations_pattern looked_for genv =
let (argscs1,argscs2) = find_remaining_scopes pl args g in
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
- DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, [])
+ let args = List.map2 (fun x -> in_pat false (x,snd scopes)) argscs2 args in
+ let pat =
+ if List.length pl = 0 then
+ (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then
+ implicit arguments are not inherited *)
+ RCPatCstr (g, pl @ args, [])
+ else
+ RCPatCstr (g, pl, args) in
+ DAst.make ?loc @@ pat
| NList (x,y,iter,terminator,revert) ->
if not (List.is_empty args) then user_err ?loc
(strbrk "Application of arguments to a recursive notation not supported in patterns.");
@@ -1892,6 +1973,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
with Not_found ->
raise (InternalizationError (locid,UnboundFixName (false,iddef)))
in
+ let env = restart_lambda_binders env in
let idl_temp = Array.map
(fun (id,recarg,bl,ty,_) ->
let recarg = Option.map (function { CAst.v = v } -> match v with
@@ -1934,6 +2016,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
with Not_found ->
raise (InternalizationError (locid,UnboundFixName (true,iddef)))
in
+ let env = restart_lambda_binders env in
let idl_tmp = Array.map
(fun ({ CAst.loc; v = id },bl,ty,_) ->
let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
@@ -1957,23 +2040,23 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
Array.map (fun (_,_,bd) -> bd) idl)
| CProdN ([],c2) -> anomaly (Pp.str "The AST is malformed, found prod without binders.")
| CProdN (bl,c2) ->
- let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in
+ let (env',bl) = List.fold_left intern_local_binder (switch_prod_binders env,[]) bl in
expand_binders ?loc mkGProd bl (intern_type env' c2)
| CLambdaN ([],c2) -> anomaly (Pp.str "The AST is malformed, found lambda without binders.")
| CLambdaN (bl,c2) ->
- let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in
+ let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope (switch_lambda_binders env),[]) bl in
expand_binders ?loc mkGLambda bl (intern env' c2)
| CLetIn (na,c1,t,c2) ->
- let inc1 = intern_restart_implicit (reset_tmp_scope env) c1 in
- let int = Option.map (intern_type_restart_implicit env) t in
+ let inc1 = intern_restart_binders (reset_tmp_scope env) c1 in
+ let int = Option.map (intern_type_restart_binders env) t in
DAst.make ?loc @@
GLetIn (na.CAst.v, inc1, int,
- intern_restart_implicit (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
- | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
+ intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
+ | CNotation (_,(InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a ->
let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
- | CNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
- | CNotation (ntn,args) ->
+ | CNotation (_,(InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
+ | CNotation (_,ntn,args) ->
intern_notation intern env ntnvars loc ntn args
| CGeneralization (b,a,c) ->
intern_generalization intern env ntnvars loc b a c
@@ -1988,6 +2071,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv)
lvar us args ref
in
+ check_not_notation_variable f ntnvars;
(* Rem: GApp(_,f,[]) stands for @f *)
if args = [] then DAst.make ?loc @@ GApp (f,[]) else
smart_gapp f loc (intern_args env args_scopes (List.map fst args))
@@ -2004,12 +2088,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CRef (ref,us) ->
intern_applied_reference ~isproj intern env
(Environ.named_context_val globalenv) lvar us args ref
- | CNotation (ntn,([],[],[],[])) ->
+ | CNotation (_,ntn,ntnargs) ->
assert (Option.is_empty isproj);
- let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in
+ let c = intern_notation intern env ntnvars loc ntn ntnargs in
let x, impl, scopes, l = find_appl_head_data c in
(x,impl,scopes,l), args
- | _ -> assert (Option.is_empty isproj); (intern env f,[],[],[]), args in
+ | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in
apply_impargs c env impargs args_scopes
(merge_impargs l args) loc
@@ -2053,7 +2137,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
tms ([],Id.Set.empty,Id.Map.empty,[]) in
let env' = Id.Set.fold
(fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var))
- (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
+ (Id.Set.union ex_ids as_in_vars)
+ (reset_hidden_inductive_implicit_test (restart_lambda_binders env)) in
(* PatVars before a real pattern do not need to be matched *)
let stripped_match_from_in =
let rec aux = function
@@ -2063,7 +2148,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
in aux match_from_in in
let rtnpo = Option.map (replace_vars_constr_expr aliases) rtnpo in
let rtnpo = match stripped_match_from_in with
- | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *)
+ | [] -> Option.map (intern_type (slide_binders env')) rtnpo (* Only PatVar in "in" clauses *)
| l ->
(* Build a return predicate by expansion of the patterns of the "in" clause *)
let thevars, thepats = List.split l in
@@ -2071,7 +2156,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let sub_tms = List.map (fun id -> (DAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in
let main_sub_eqn = CAst.make @@
([],thepats, (* "|p1,..,pn" *)
- Option.cata (intern_type env')
+ Option.cata (intern_type_no_implicit env')
(DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None))
rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
let catch_all_sub_eqn =
@@ -2090,7 +2175,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let p' = Option.map (fun u ->
let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
(CAst.make na') in
- intern_type env'' u) po in
+ intern_type (slide_binders env'') u) po in
DAst.make ?loc @@
GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b',
intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
@@ -2100,7 +2185,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let p' = Option.map (fun p ->
let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
(CAst.make na') in
- intern_type env'' p) po in
+ intern_type (slide_binders env'') p) po in
DAst.make ?loc @@
GIf (c', (na', p'), intern env b1, intern env b2)
| CHole (k, naming, solve) ->
@@ -2160,18 +2245,20 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
GSort s
| CCast (c1, c2) ->
DAst.make ?loc @@
- GCast (intern env c1, map_cast_type (intern_type env) c2)
+ GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2)
)
and intern_type env = intern (set_type_scope env)
- and intern_no_implicit env = intern {env with impl_binder_index = None}
+ and intern_type_no_implicit env = intern (restart_no_binders (set_type_scope env))
+
+ and intern_no_implicit env = intern (restart_no_binders env)
- and intern_restart_implicit env = intern {env with impl_binder_index = Some 0}
+ and intern_restart_binders env = intern (restart_lambda_binders env)
- and intern_type_restart_implicit env = intern {(set_type_scope env) with impl_binder_index = Some 0}
+ and intern_type_restart_binders env = intern (restart_prod_binders (set_type_scope env))
and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list =
- intern_local_binder_aux intern_restart_implicit ntnvars env bind
+ intern_local_binder_aux intern ntnvars env bind
(* Expands a multiple pattern into a disjunction of multiple patterns *)
and intern_multiple_pattern env n pl =
@@ -2198,7 +2285,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in
List.map (fun (asubst,pl) ->
let rhs = replace_vars_constr_expr asubst rhs in
- let rhs' = intern {env with ids = env_ids} rhs in
+ let rhs' = intern_no_implicit {env with ids = env_ids} rhs in
CAst.make ?loc (eqn_ids,pl,rhs')) pll
and intern_case_item env forbidden_names_for_gen (tm,na,t) =
@@ -2336,7 +2423,12 @@ let extract_ids env =
let scope_of_type_kind sigma = function
| IsType -> Notation.current_type_scope_name ()
| OfType typ -> compute_type_scope sigma typ
- | WithoutTypeConstraint -> None
+ | WithoutTypeConstraint | UnknownIfTermOrType -> None
+
+let allowed_binder_kind_of_type_kind = function
+ | IsType -> Some AbsPi
+ | OfType _ | WithoutTypeConstraint -> Some AbsLambda
+ | UnknownIfTermOrType -> None
let empty_ltac_sign = {
ltac_vars = Id.Set.empty;
@@ -2348,9 +2440,10 @@ let intern_gen kind env sigma
?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
c =
let tmp_scope = scope_of_type_kind sigma kind in
+ let k = allowed_binder_kind_of_type_kind kind in
internalize env {ids = extract_ids env; unb = false;
tmp_scope = tmp_scope; scopes = [];
- impls; impl_binder_index = Some 0}
+ impls; binder_block_names = Some (k,Id.Map.domain impls)}
pattern_mode (ltacvars, Id.Map.empty) c
let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c
@@ -2372,8 +2465,8 @@ let interp_gen kind env sigma ?(impls=empty_internalization_env) c =
let c = intern_gen kind ~impls env sigma c in
understand ~expected_type:kind env sigma c
-let interp_constr env sigma ?(impls=empty_internalization_env) c =
- interp_gen WithoutTypeConstraint env sigma c
+let interp_constr ?(expected_type=WithoutTypeConstraint) env sigma ?(impls=empty_internalization_env) c =
+ interp_gen expected_type env sigma c
let interp_type env sigma ?(impls=empty_internalization_env) c =
interp_gen IsType env sigma ~impls c
@@ -2383,8 +2476,8 @@ let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ =
(* Not all evars expected to be resolved *)
-let interp_open_constr env sigma c =
- understand_tcc env sigma (intern_constr env sigma c)
+let interp_open_constr ?(expected_type=WithoutTypeConstraint) env sigma c =
+ understand_tcc env sigma (intern_gen expected_type env sigma c)
(* Not all evars expected to be resolved and computation of implicit args *)
@@ -2432,8 +2525,10 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
{ Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
let tmp_scope = scope_of_type_kind sigma kind in
let impls = empty_internalization_env in
+ let k = allowed_binder_kind_of_type_kind kind in
internalize env
- {ids; unb = false; tmp_scope; scopes = []; impls; impl_binder_index = Some 0}
+ {ids; unb = false; tmp_scope; scopes = []; impls;
+ binder_block_names = Some (k,Id.Set.empty)}
pattern_mode (ltacvars, vl) c
let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
@@ -2442,7 +2537,7 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
let c = internalize env
- {ids; unb = false; tmp_scope = None; scopes = []; impls; impl_binder_index = None}
+ {ids; unb = false; tmp_scope = None; scopes = []; impls; binder_block_names = None}
false (empty_ltac_sign, vl) a in
(* Splits variables into those that are binding, bound, or both *)
(* Translate and check that [c] has all its free variables bound in [vars] *)
@@ -2473,13 +2568,17 @@ let my_intern_constr env lvar acc c =
let intern_context env impl_env binders =
try
let lvar = (empty_ltac_sign, Id.Map.empty) in
+ let ids =
+ (* We assume all ids around are parts of the prefix of the current
+ context being interpreted *)
+ extract_ids env in
let lenv, bl = List.fold_left
(fun (lenv, bl) b ->
let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
(env, bl))
- ({ids = extract_ids env; unb = false;
+ ({ids; unb = false;
tmp_scope = None; scopes = []; impls = impl_env;
- impl_binder_index = Some 0}, []) binders in
+ binder_block_names = Some (Some AbsPi,ids)}, []) binders in
(lenv.impls, List.map glob_local_binder_of_extended bl)
with InternalizationError (loc,e) ->
user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
@@ -2500,8 +2599,10 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
let r = Retyping.relevance_of_type env sigma t in
let d = LocalAssum (make_annot na r,t) in
let impls =
- if k == Implicit then CAst.make (Some (na,true)) :: impls
- else CAst.make None :: impls
+ match k with
+ | NonMaxImplicit -> CAst.make (Some (na,false)) :: impls
+ | MaxImplicit -> CAst.make (Some (na,true)) :: impls
+ | Explicit -> CAst.make None :: impls
in
(push_rel d env, sigma, d::params, succ n, impls)
| Some b ->
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 8cce7cd9af..670563f02f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -97,7 +97,7 @@ val intern_context : env -> internalization_env -> local_binder_expr list -> int
(** Main interpretation functions, using type class inference,
expecting evars and pending problems to be all resolved *)
-val interp_constr : env -> evar_map -> ?impls:internalization_env ->
+val interp_constr : ?expected_type:typing_constraint -> env -> evar_map -> ?impls:internalization_env ->
constr_expr -> constr Evd.in_evar_universe_context
val interp_casted_constr : env -> evar_map -> ?impls:internalization_env ->
@@ -109,7 +109,7 @@ val interp_type : env -> evar_map -> ?impls:internalization_env ->
(** Main interpretation function expecting all postponed problems to
be resolved, but possibly leaving evars. *)
-val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr
+val interp_open_constr : ?expected_type:typing_constraint -> env -> evar_map -> constr_expr -> evar_map * constr
(** Accepting unresolved evars *)
diff --git a/interp/impargs.ml b/interp/impargs.ml
index e2c732809a..78c4b21920 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -14,6 +14,7 @@ open Util
open Names
open Constr
open Globnames
+open Glob_term
open Declarations
open Lib
open Libobject
@@ -80,10 +81,28 @@ let with_implicit_protection f x =
let () = implicit_args := oflags in
iraise reraise
-let set_maximality imps b =
+type on_trailing_implicit = Error | Info | Silent
+
+
+let msg_trailing_implicit (fail : on_trailing_implicit) na i =
+ let pos = match na with
+ | Anonymous -> "number " ^ string_of_int i
+ | Name id -> Names.Id.to_string id in
+ let str1 = "Argument " ^ pos ^ " is a trailing implicit, " in
+ match fail with
+ | Error ->
+ user_err (strbrk (str1 ^ "so it can't be declared non maximal. Please use { } instead of [ ]."))
+ | Info ->
+ Flags.if_verbose Feedback.msg_info (strbrk (str1 ^ "so it has been declared maximally inserted."))
+ | Silent -> ()
+
+let set_maximality fail na i imps b =
(* Force maximal insertion on ending implicits (compatibility) *)
- let is_set x = match x with None -> false | _ -> true in
- b || List.for_all is_set imps
+ b || (
+ let is_set x = match x with None -> false | _ -> true in
+ let b' = List.for_all is_set imps in
+ if b' then msg_trailing_implicit fail na i;
+ b')
(*s Computation of implicit arguments *)
@@ -302,6 +321,11 @@ let is_status_implicit = function
let name_of_pos k = Id.of_string ("arg_" ^ string_of_int k)
+let binding_kind_of_status = function
+ | Some (_, _, (false, _)) -> NonMaxImplicit
+ | Some (_, _, (true, _)) -> MaxImplicit
+ | None -> Explicit
+
let name_of_implicit = function
| None -> anomaly (Pp.str "Not an implicit argument.")
| Some (ExplByName id,_,_) -> id
@@ -335,24 +359,24 @@ let positions_of_implicits (_,impls) =
(* Manage user-given implicit arguments *)
-let rec prepare_implicits f = function
+let rec prepare_implicits i f = function
| [] -> []
| (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
| (Name id, Some imp)::imps ->
- let imps' = prepare_implicits f imps in
- Some (ExplByName id,imp,(set_maximality imps' f.maximal,true)) :: imps'
- | _::imps -> None :: prepare_implicits f imps
+ let imps' = prepare_implicits (i+1) f imps in
+ Some (ExplByName id,imp,(set_maximality Silent (Name id) i imps' f.maximal,true)) :: imps'
+ | _::imps -> None :: prepare_implicits (i+1) f imps
-let set_manual_implicits flags enriching autoimps l =
+let set_manual_implicits silent flags enriching autoimps l =
(* Compare with automatic implicits to recover printing data and names *)
let rec merge k autoimps explimps = match autoimps, explimps with
| autoimp::autoimps, explimp::explimps ->
let imps' = merge (k+1) autoimps explimps in
begin match autoimp, explimp.CAst.v with
| (Name id,_), Some (_,max) ->
- Some (ExplByName id, Manual, (set_maximality imps' max, true))
+ Some (ExplByName id, Manual, (set_maximality (if silent then Silent else Error) (Name id) k imps' max, true))
| (Name id,Some exp), None when enriching ->
- Some (ExplByName id, exp, (set_maximality imps' flags.maximal, true))
+ Some (ExplByName id, exp, (set_maximality (if silent then Silent else Info) (Name id) k imps' flags.maximal, true))
| (Name _,_), None -> None
| (Anonymous,_), Some (Name id,max) ->
Some (ExplByName id,Manual,(max,true))
@@ -370,7 +394,7 @@ let set_manual_implicits flags enriching autoimps l =
let compute_semi_auto_implicits env sigma f t =
if not f.auto then [DefaultImpArgs, []]
else let l = compute_implicits_flags env sigma f false t in
- [DefaultImpArgs, prepare_implicits f l]
+ [DefaultImpArgs, prepare_implicits 1 f l]
(*s Constants. *)
@@ -497,8 +521,9 @@ let impls_of_context ctx =
let map decl =
let id = NamedDecl.get_id decl in
match Id.Map.get id !sec_implicits with
- | Glob_term.Implicit -> Some (ExplByName id, Manual, (true, true))
- | Glob_term.Explicit -> None
+ | NonMaxImplicit -> Some (ExplByName id, Manual, (false, true))
+ | MaxImplicit -> Some (ExplByName id, Manual, (true, true))
+ | Explicit -> None
in
List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
@@ -608,7 +633,7 @@ type manual_implicits = (Name.t * bool) option CAst.t list
let compute_implicits_with_manual env sigma typ enriching l =
let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
- set_manual_implicits !implicit_args enriching autoimpls l
+ set_manual_implicits true !implicit_args enriching autoimpls l
let check_inclusion l =
(* Check strict inclusion *)
@@ -636,7 +661,7 @@ let declare_manual_implicits local ref ?enriching l =
let t = of_constr t in
let enriching = Option.default flags.auto enriching in
let autoimpls = compute_auto_implicits env sigma flags enriching t in
- let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in
+ let l = [DefaultImpArgs, set_manual_implicits false flags enriching autoimpls l] in
let req =
if is_local local ref then ImplLocal
else ImplInteractive(flags,ImplManual (List.length autoimpls))
@@ -646,28 +671,22 @@ let maybe_declare_manual_implicits local ref ?enriching l =
if List.exists (fun x -> x.CAst.v <> None) l then
declare_manual_implicits local ref ?enriching l
-
-let msg_trailing_implicit id =
- user_err (strbrk ("Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]."))
-
-type implicit_kind = Implicit | MaximallyImplicit | NotImplicit
+let explicit_kind i = function
+ | Name id -> ExplByName id
+ | Anonymous -> ExplByPos (i,None)
let compute_implicit_statuses autoimps l =
let rec aux i = function
- | _ :: autoimps, NotImplicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
- | Name id :: autoimps, MaximallyImplicit :: manualimps ->
- Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
- | Name id :: autoimps, Implicit :: manualimps ->
+ | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
+ | na :: autoimps, MaxImplicit :: manualimps ->
+ Some (explicit_kind i na, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
+ | na :: autoimps, NonMaxImplicit :: manualimps ->
let imps' = aux (i+1) (autoimps, manualimps) in
- let max = set_maximality imps' false in
- if max then msg_trailing_implicit id;
- Some (ExplByName id, Manual, (max, true)) :: imps'
- | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ ->
- user_err ~hdr:"set_implicits"
- (strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit."))
+ let max = set_maximality Error na i imps' false in
+ Some (explicit_kind i na, Manual, (max, true)) :: imps'
| autoimps, [] -> List.map (fun _ -> None) autoimps
| [], _::_ -> assert false
- in aux 0 (autoimps, l)
+ in aux 1 (autoimps, l)
let set_implicits local ref l =
let flags = !implicit_args in
@@ -684,7 +703,7 @@ let set_implicits local ref l =
check_rigidity (is_rigid env sigma t);
(* Sort by number of implicits, decreasing *)
let is_implicit = function
- | NotImplicit -> false
+ | Explicit -> false
| _ -> true in
let l = List.map (fun imps -> (imps,List.count is_implicit imps)) l in
let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index ef3c2496f4..65e7fd8aaf 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -77,6 +77,7 @@ type implicit_side_condition
type implicits_list = implicit_side_condition * implicit_status list
val is_status_implicit : implicit_status -> bool
+val binding_kind_of_status : implicit_status -> Glob_term.binding_kind
val is_inferable_implicit : bool -> int -> implicit_status -> bool
val name_of_implicit : implicit_status -> Id.t
val maximal_insertion_of : implicit_status -> bool
@@ -113,12 +114,10 @@ val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
manual_implicits -> unit
-type implicit_kind = Implicit | MaximallyImplicit | NotImplicit
-
(** [set_implicits local ref l]
Manual declaration of implicit arguments.
`l` is a list of possible sequences of implicit statuses. *)
-val set_implicits : bool -> GlobRef.t -> implicit_kind list list -> unit
+val set_implicits : bool -> GlobRef.t -> Glob_term.binding_kind list list -> unit
val implicits_of_global : GlobRef.t -> implicits_list list
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 8b457ab37b..e6f12f7eb2 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -92,7 +92,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
let rec aux bdvars l c = match CAst.(c.v) with
| CRef (qid,_) when qualid_is_ident qid ->
found c.CAst.loc (qualid_basename qid) bdvars l
- | CNotation ((InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+ | CNotation (_,(InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
| _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
@@ -203,8 +203,9 @@ let warn_ignoring_implicit_status =
let implicits_of_glob_constr ?(with_products=true) l =
let add_impl ?loc na bk l = match bk with
- | Implicit -> CAst.make ?loc (Some (na,true)) :: l
- | _ -> CAst.make ?loc None :: l
+ | NonMaxImplicit -> CAst.make ?loc (Some (na,false)) :: l
+ | MaxImplicit -> CAst.make ?loc (Some (na,true)) :: l
+ | Explicit -> CAst.make ?loc None :: l
in
let rec aux c =
match DAst.get c with
@@ -212,8 +213,9 @@ let implicits_of_glob_constr ?(with_products=true) l =
if with_products then add_impl na bk (aux b)
else
let () = match bk with
- | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
- | _ -> ()
+ | NonMaxImplicit
+ | MaxImplicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
+ | Explicit -> ()
in []
| GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b)
| GLetIn (na, b, t, c) -> aux c
diff --git a/interp/notation.ml b/interp/notation.ml
index 93969f3718..2086e08f79 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -49,6 +49,11 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with
| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2
| (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false
+let notation_with_optional_scope_eq inscope1 inscope2 = match (inscope1,inscope2) with
+ | LastLonelyNotation, LastLonelyNotation -> true
+ | NotationInScope s1, NotationInScope s2 -> String.equal s1 s2
+ | (LastLonelyNotation | NotationInScope _), _ -> false
+
let notation_eq (from1,ntn1) (from2,ntn2) =
notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
@@ -63,6 +68,15 @@ module NotationOrd =
module NotationSet = Set.Make(NotationOrd)
module NotationMap = CMap.Make(NotationOrd)
+module SpecificNotationOrd =
+ struct
+ type t = specific_notation
+ let compare = pervasives_compare
+ end
+
+module SpecificNotationSet = Set.Make(SpecificNotationOrd)
+module SpecificNotationMap = CMap.Make(SpecificNotationOrd)
+
(**********************************************************************)
(* Scope of symbols *)
@@ -148,21 +162,21 @@ let normalize_scope sc =
(**********************************************************************)
(* The global stack of scopes *)
-type scope_elem = Scope of scope_name | SingleNotation of notation
-type scopes = scope_elem list
+type scope_item = OpenScopeItem of scope_name | LonelyNotationItem of notation
+type scopes = scope_item list
let scope_eq s1 s2 = match s1, s2 with
-| Scope s1, Scope s2 -> String.equal s1 s2
-| SingleNotation s1, SingleNotation s2 -> notation_eq s1 s2
-| Scope _, SingleNotation _
-| SingleNotation _, Scope _ -> false
+| OpenScopeItem s1, OpenScopeItem s2 -> String.equal s1 s2
+| LonelyNotationItem s1, LonelyNotationItem s2 -> notation_eq s1 s2
+| OpenScopeItem _, LonelyNotationItem _
+| LonelyNotationItem _, OpenScopeItem _ -> false
let scope_stack = ref []
let current_scopes () = !scope_stack
let scope_is_open_in_scopes sc l =
- List.exists (function Scope sc' -> String.equal sc sc' | _ -> false) l
+ List.exists (function OpenScopeItem sc' -> String.equal sc sc' | _ -> false) l
let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
@@ -188,7 +202,7 @@ let discharge_scope (_,(local,_,_ as o)) =
let classify_scope (local,_,_ as o) =
if local then Dispose else Substitute o
-let inScope : bool * bool * scope_elem -> obj =
+let inScope : bool * bool * scope_item -> obj =
declare_object {(default_object "SCOPE") with
cache_function = cache_scope;
open_function = open_scope;
@@ -197,11 +211,11 @@ let inScope : bool * bool * scope_elem -> obj =
classify_function = classify_scope }
let open_close_scope (local,opening,sc) =
- Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc)))
+ Lib.add_anonymous_leaf (inScope (local,opening,OpenScopeItem (normalize_scope sc)))
let empty_scope_stack = []
-let push_scope sc scopes = Scope sc :: scopes
+let push_scope sc scopes = OpenScopeItem sc :: scopes
let push_scopes = List.fold_right push_scope
@@ -254,7 +268,7 @@ let find_delimiters_scope ?loc key =
(* Uninterpretation tables *)
type interp_rule =
- | NotationRule of scope_name option * notation
+ | NotationRule of specific_notation
| SynDefRule of KerName.t
(* We define keys for glob_constr and aconstr to split the syntax entries
@@ -1064,17 +1078,17 @@ let check_required_module ?loc sc (sp,d) =
the scope stack [scopes], and if yes, using delimiters or not *)
let find_with_delimiters = function
- | None -> None
- | Some scope ->
+ | LastLonelyNotation -> None
+ | NotationInScope scope ->
match (String.Map.find scope !scope_map).delimiters with
| Some key -> Some (Some scope, Some key)
| None -> None
let rec find_without_delimiters find (ntn_scope,ntn) = function
- | Scope scope :: scopes ->
+ | OpenScopeItem scope :: scopes ->
(* Is the expected ntn/numpr attached to the most recently open scope? *)
begin match ntn_scope with
- | Some scope' when String.equal scope scope' ->
+ | NotationInScope scope' when String.equal scope scope' ->
Some (None,None)
| _ ->
(* If the most recently open scope has a notation/numeral printer
@@ -1084,9 +1098,9 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
else
find_without_delimiters find (ntn_scope,ntn) scopes
end
- | SingleNotation ntn' :: scopes ->
+ | LonelyNotationItem ntn' :: scopes ->
begin match ntn_scope, ntn with
- | None, Some ntn when notation_eq ntn ntn' ->
+ | LastLonelyNotation, Some ntn when notation_eq ntn ntn' ->
Some (None, None)
| _ ->
find_without_delimiters find (ntn_scope,ntn) scopes
@@ -1123,7 +1137,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation =
scope_map := String.Map.add scope sc !scope_map
end;
begin match scopt with
- | None -> scope_stack := SingleNotation ntn :: !scope_stack
+ | None -> scope_stack := LonelyNotationItem ntn :: !scope_stack
| Some _ -> ()
end
@@ -1133,15 +1147,15 @@ let declare_uninterpretation rule (metas,c as pat) =
let rec find_interpretation ntn find = function
| [] -> raise Not_found
- | Scope scope :: scopes ->
+ | OpenScopeItem scope :: scopes ->
(try let n = find scope in (n,Some scope)
with Not_found -> find_interpretation ntn find scopes)
- | SingleNotation ntn'::scopes when notation_eq ntn' ntn ->
+ | LonelyNotationItem ntn'::scopes when notation_eq ntn' ntn ->
(try let n = find default_scope in (n,None)
with Not_found ->
(* e.g. because single notation only for constr, not cases_pattern *)
find_interpretation ntn find scopes)
- | SingleNotation _::scopes ->
+ | LonelyNotationItem _::scopes ->
find_interpretation ntn find scopes
let find_notation ntn sc =
@@ -1244,7 +1258,7 @@ let availability_of_notation (ntn_scope,ntn) scopes =
commonly from the lowest level of the source entry to the highest
level of the target entry. *)
-type entry_coercion = notation list
+type entry_coercion = (notation_with_optional_scope * notation) list
module EntryCoercionOrd =
struct
@@ -1295,7 +1309,7 @@ let rec insert_coercion_path path = function
else if shorter_path path path' then path::allpaths
else path'::insert_coercion_path path paths
-let declare_entry_coercion (entry,_ as ntn) entry' =
+let declare_entry_coercion (scope,(entry,_) as specific_ntn) entry' =
let entry, lev = decompose_custom_entry entry in
let entry', lev' = decompose_custom_entry entry' in
(* Transitive closure *)
@@ -1304,19 +1318,19 @@ let declare_entry_coercion (entry,_ as ntn) entry' =
List.fold_right (fun ((lev'',lev'''),path) l ->
if notation_entry_eq entry entry''' && level_ord lev lev''' &&
not (notation_entry_eq entry' entry'')
- then ((entry'',entry'),((lev'',lev'),path@[ntn]))::l else l) paths l)
+ then ((entry'',entry'),((lev'',lev'),path@[specific_ntn]))::l else l) paths l)
!entry_coercion_map [] in
let toaddright =
EntryCoercionMap.fold (fun (entry'',entry''') paths l ->
List.fold_right (fun ((lev'',lev'''),path) l ->
if entry' = entry'' && level_ord lev' lev'' && entry <> entry'''
- then ((entry,entry'''),((lev,lev'''),path@[ntn]))::l else l) paths l)
+ then ((entry,entry'''),((lev,lev'''),path@[specific_ntn]))::l else l) paths l)
!entry_coercion_map [] in
entry_coercion_map :=
List.fold_right (fun (pair,path) ->
let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in
EntryCoercionMap.add pair (insert_coercion_path path olds))
- (((entry,entry'),((lev,lev'),[ntn]))::toaddright@toaddleft)
+ (((entry,entry'),((lev,lev'),[specific_ntn]))::toaddright@toaddleft)
!entry_coercion_map
let entry_has_global_map = ref String.Map.empty
@@ -1389,7 +1403,7 @@ let availability_of_prim_token n printer_scope local_scopes =
with Not_found -> false
in
let scopes = make_current_scopes local_scopes in
- Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
+ Option.map snd (find_without_delimiters f (NotationInScope printer_scope,None) scopes)
(* Miscellaneous *)
@@ -1705,11 +1719,11 @@ let pr_scopes prglob =
let rec find_default ntn = function
| [] -> None
- | Scope scope :: scopes ->
+ | OpenScopeItem scope :: scopes ->
if NotationMap.mem ntn (find_scope scope).notations then
Some scope
else find_default ntn scopes
- | SingleNotation ntn' :: scopes ->
+ | LonelyNotationItem ntn' :: scopes ->
if notation_eq ntn ntn' then Some default_scope
else find_default ntn scopes
@@ -1863,13 +1877,13 @@ let collect_notation_in_scope scope sc known =
let collect_notations stack =
fst (List.fold_left
(fun (all,knownntn as acc) -> function
- | Scope scope ->
+ | OpenScopeItem scope ->
if String.List.mem_assoc scope all then acc
else
let (l,knownntn) =
collect_notation_in_scope scope (find_scope scope) knownntn in
((scope,l)::all,knownntn)
- | SingleNotation ntn ->
+ | LonelyNotationItem ntn ->
if List.mem_f notation_eq ntn knownntn then (all,knownntn)
else
try
diff --git a/interp/notation.mli b/interp/notation.mli
index ea5125f7ec..26c45d5896 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -25,11 +25,15 @@ val notation_entry_eq : notation_entry -> notation_entry -> bool
val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool
(** Equality on [notation_entry_level]. *)
+val notation_with_optional_scope_eq : notation_with_optional_scope -> notation_with_optional_scope -> bool
+
val notation_eq : notation -> notation -> bool
(** Equality on [notation]. *)
module NotationSet : Set.S with type elt = notation
module NotationMap : CMap.ExtS with type key = notation and module Set := NotationSet
+module SpecificNotationSet : Set.S with type elt = specific_notation
+module SpecificNotationMap : CMap.ExtS with type key = specific_notation and module Set := SpecificNotationSet
(** {6 Scopes } *)
(** A scope is a set of interpreters for symbols + optional
@@ -213,7 +217,7 @@ val availability_of_prim_token :
(** Binds a notation in a given scope to an interpretation *)
type interp_rule =
- | NotationRule of scope_name option * notation
+ | NotationRule of specific_notation
| SynDefRule of KerName.t
val declare_notation_interpretation : notation -> scope_name option ->
@@ -236,7 +240,7 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list
(** Test if a notation is available in the scopes
context [scopes]; if available, the result is not None; the first
argument is itself not None if a delimiters is needed *)
-val availability_of_notation : scope_name option * notation -> subscopes ->
+val availability_of_notation : specific_notation -> subscopes ->
(scope_name option * delimiters option) option
(** {6 Miscellaneous} *)
@@ -299,8 +303,8 @@ val locate_notation : (glob_constr -> Pp.t) -> notation_key ->
val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
-type entry_coercion = notation list
-val declare_entry_coercion : notation -> notation_entry_level -> unit
+type entry_coercion = (notation_with_optional_scope * notation) list
+val declare_entry_coercion : specific_notation -> notation_entry_level -> unit
val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option
val declare_custom_entry_has_global : string -> int -> unit
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 265ca58ed9..59a58d643c 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -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)
@@ -1340,35 +1364,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 +1403,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 =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index f9de6b7d6b..2ab8b620df 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -35,12 +35,21 @@ val notation_constr_of_glob_constr : notation_interp_env ->
(** Re-interpret a notation as a [glob_constr], taking care of binders *)
+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;
+}
+
val apply_cases_pattern : ?loc:Loc.t ->
(Id.t list * cases_pattern_disjunction) * Id.t -> glob_constr -> glob_constr
val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t ->
('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t) ->
- ('a -> notation_constr -> glob_constr) ->
+ ('a -> notation_constr -> glob_constr) -> ?h:'a binder_status_fun ->
'a -> notation_constr -> glob_constr
val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_constr
@@ -60,12 +69,12 @@ val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
val match_notation_constr_cases_pattern :
'a cases_pattern_g -> interpretation ->
(('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
- (int * 'a cases_pattern_g list)
+ (bool * int * 'a cases_pattern_g list)
val match_notation_constr_ind_pattern :
inductive -> 'a cases_pattern_g list -> interpretation ->
(('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
- (int * 'a cases_pattern_g list)
+ (bool * int * 'a cases_pattern_g list)
(** {5 Matching a notation pattern against a [glob_constr]} *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index e81439c3d5..4a731e57a3 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -104,8 +104,8 @@ let declare_reserved_type idl t =
let find_reserved_type id = Id.Map.find (root_of_id id) !reserve_table
let constr_key c =
- try RefKey (canonical_gr (global_of_constr (fst (Constr.decompose_app c))))
- with Not_found -> Oth
+ try RefKey (canonical_gr (fst @@ Constr.destRef (fst (Constr.decompose_app c))))
+ with Constr.DestKO -> Oth
let revert_reserved_type t =
try
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 07:20:18 +0000