aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml328
-rw-r--r--interp/constrintern.ml191
-rw-r--r--interp/constrintern.mli4
-rw-r--r--interp/impargs.ml83
-rw-r--r--interp/impargs.mli5
-rw-r--r--interp/implicit_quantifiers.ml10
-rw-r--r--interp/notation_ops.ml36
-rw-r--r--interp/notation_ops.mli11
-rw-r--r--interp/reserve.ml4
9 files changed, 425 insertions, 247 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index cc0c1e4602..c198c4eb9b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -194,7 +194,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
@@ -281,6 +280,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 =
@@ -550,14 +560,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 +579,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 +606,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 +619,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 +681,63 @@ 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 (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
+ let args = adjust_implicit_arguments false (List.length args) 1 args impl in
+ mkFlattenedCApp (f,args)
let extern_args extern env args =
let map (arg, argscopes) = lazy (extern argscopes env arg) in
@@ -838,56 +915,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,
@@ -1104,46 +1144,45 @@ 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 && nallargs > 0 ->
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
+ let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
+ let args2impls = try List.skipn n argsimpls with Failure _ -> [] in
+ (* Note: NApp(NRef f,[]), hence n=0, encodes @f *)
(if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
- args2, subscopes, impls
- | GApp (f, args), None ->
+ args2, args2scopes, args2impls
+ | None when nallargs > 0 ->
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, [], [], []
+ | Some 0 when nallargs = 0 ->
+ begin match DAst.get f with
+ | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], []
+ | _ -> t, [], [], []
+ end
+ | 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
+ match keyrule with
| NotationRule (sc,ntn) ->
(match availability_of_entry_coercion custom (fst ntn) with
| None -> raise No_match
@@ -1171,22 +1210,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 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..b2c572d290 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -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))
@@ -713,6 +765,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 +790,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 +798,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 +888,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 *)
@@ -1144,7 +1209,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 +1615,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
@@ -1643,7 +1707,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
@@ -1892,6 +1956,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 +1999,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,18 +2023,18 @@ 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)
+ 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)))
@@ -2009,7 +2075,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) 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 +2119,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 +2130,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 +2138,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 +2157,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 +2167,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 +2227,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_restart_implicit env = intern {env with impl_binder_index = Some 0}
+ and intern_no_implicit env = intern (restart_no_binders env)
- and intern_type_restart_implicit env = intern {(set_type_scope env) with impl_binder_index = Some 0}
+ and intern_restart_binders env = intern (restart_lambda_binders env)
+
+ 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 +2267,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 +2405,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 +2422,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 +2447,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 +2458,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 +2507,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 +2519,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 +2550,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 +2581,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..ffbb982ab7 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -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_ops.ml b/interp/notation_ops.ml
index 265ca58ed9..d1eb50d370 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)
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index f9de6b7d6b..c62dac013b 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
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-04-29 10:38:18 +0000