diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 188 | ||||
| -rw-r--r-- | interp/constrintern.mli | 4 | ||||
| -rw-r--r-- | interp/impargs.ml | 61 | ||||
| -rw-r--r-- | interp/impargs.mli | 5 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 10 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 36 | ||||
| -rw-r--r-- | interp/notation_ops.mli | 11 |
7 files changed, 224 insertions, 91 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f4ae5bf676..2ceea58297 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 @@ -1892,6 +1957,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 +2000,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 +2024,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 +2076,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 +2120,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 +2131,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 +2139,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 +2158,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 +2168,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 +2228,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 +2268,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 +2406,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 +2423,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 +2448,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 +2459,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 +2508,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 +2520,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 +2551,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 +2582,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..9b50d9ca71 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,24 @@ 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) id = + let str1 = "Argument " ^ Names.Id.to_string id ^ " 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 id 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 id; + b') (*s Computation of implicit arguments *) @@ -302,6 +317,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 @@ -340,19 +360,19 @@ let rec prepare_implicits 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' + Some (ExplByName id,imp,(set_maximality Silent id imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits 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) id 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) id imps' flags.maximal, true)) | (Name _,_), None -> None | (Anonymous,_), Some (Name id,max) -> Some (ExplByName id,Manual,(max,true)) @@ -497,8 +517,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 +629,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 +657,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)) @@ -647,22 +668,16 @@ let maybe_declare_manual_implicits local ref ?enriching l = 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 compute_implicit_statuses autoimps l = let rec aux i = function - | _ :: autoimps, NotImplicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps) - | Name id :: autoimps, MaximallyImplicit :: manualimps -> + | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps) + | Name id :: autoimps, MaxImplicit :: manualimps -> Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps) - | Name id :: autoimps, Implicit :: manualimps -> + | Name id :: 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; + let max = set_maximality Error id imps' false in Some (ExplByName id, Manual, (max, true)) :: imps' - | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ -> + | Anonymous :: _, (NonMaxImplicit | MaxImplicit) :: _ -> user_err ~hdr:"set_implicits" (strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit.")) | autoimps, [] -> List.map (fun _ -> None) autoimps @@ -684,7 +699,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 |