diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 110 | ||||
| -rw-r--r-- | interp/constrextern.mli | 13 | ||||
| -rw-r--r-- | interp/constrintern.ml | 132 | ||||
| -rw-r--r-- | interp/impargs.ml | 27 | ||||
| -rw-r--r-- | interp/impargs.mli | 2 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 2 |
6 files changed, 160 insertions, 126 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c85f4f2cf7..28f4f5aed6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -674,17 +674,15 @@ let match_coercion_app c = match DAst.get c with end | _ -> None -let rec remove_coercions inctx c = - match match_coercion_app c with +let remove_one_coercion inctx c = + try match match_coercion_app c with | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) -> let nargs = List.length args in - (try match Classops.hide_coercion r with + (match Classops.hide_coercion r with | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) -> - (* We skip a coercion *) + (* We skip the coercion *) let l = List.skipn (n - pars) args in let (a,l) = match l with a::l -> (a,l) | [] -> assert false in - (* Recursively remove the head coercions *) - let a' = remove_coercions true a in (* Don't flatten App's in case of funclass so that (atomic) notations on [a] work; should be compatible since printer does not care whether App's are @@ -693,10 +691,13 @@ let rec remove_coercions inctx c = been confused with ordinary application or would have need a surrounding context and the coercion to funclass would have been made explicit to match *) - if List.is_empty l then a' else DAst.make ?loc @@ GApp (a',l) - | _ -> c - with Not_found -> c) - | _ -> c + let a' = if List.is_empty l then a else DAst.make ?loc @@ GApp (a,l) in + let inctx = inctx || not (List.is_empty l) in + Some (n-pars+1, inctx, a') + | _ -> None) + | _ -> None + with Not_found -> + None let rec flatten_application c = match DAst.get c with | GApp (f, l) -> @@ -721,27 +722,11 @@ let extern_possible_prim_token (custom,scopes) r = | None -> raise No_match | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) -let filter_fully_applied r l = - let nargs = match DAst.get r with - | GApp (f,args) -> List.length args - | _ -> assert false in - List.filter (fun (keyrule,pat,n as _rule) -> n = Some nargs) l - -let extern_optimal extern extern_fully_applied r r' = - if r==r' then - (* No coercion: we look for a notation for r or a partial application of it *) - extern r - else - (* A coercion is removed: we prefer in order: - - a notation w/o a delimiter for the expression w/o coercions (or a partial application of it), if any - - a notation for the fully-applied expression with coercions, if any - - a notation with a delimiter for the expression w/o coercions (or a partial applied of it), if any *) - try - let c' = extern r' in - match c' with - | { CAst.v = CDelimiters _} -> (try extern_fully_applied r with No_match -> c') - | _ -> c' - with No_match -> extern_fully_applied r +let filter_enough_applied nargs l = + match nargs with + | None -> l + | Some nargs -> + List.filter (fun (keyrule,pat,n as _rule) -> match n with Some n -> n > nargs | None -> false) l (* Helper function for safe and optimal printing of primitive tokens *) (* such as those for Int63 *) @@ -807,22 +792,17 @@ let extern_ref vars ref us = let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) let rec extern inctx scopes vars r = - let r' = remove_coercions inctx r in - try - if !Flags.raw_print || !print_no_symbol then raise No_match; - let extern_fun = extern_possible_prim_token scopes in - extern_optimal extern_fun extern_fun r r' - with No_match -> - try - let r'' = flatten_application r' in - if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal - (fun r -> extern_notation scopes vars r (uninterp_notations r)) - (fun r -> extern_notation scopes vars r (filter_fully_applied r (uninterp_notations r))) - r r'' + match remove_one_coercion inctx (flatten_application r) with + | Some (nargs,inctx,r') -> + (try extern_notations scopes vars (Some nargs) r + with No_match -> extern inctx scopes vars r') + | None -> + + try extern_notations scopes vars None r with No_match -> - let loc = r'.CAst.loc in - match DAst.get r' with + + let loc = r.CAst.loc in + match DAst.get r with | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) @@ -1110,7 +1090,15 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in make ?loc (pll,extern inctx scopes vars c) -and extern_notation (custom,scopes as allscopes) vars t = function +and extern_notations scopes vars nargs t = + if !Flags.raw_print || !print_no_symbol then raise No_match; + try extern_possible_prim_token scopes t + with No_match -> + let t = flatten_application t in + extern_notation scopes vars t (filter_enough_applied nargs (uninterp_notations t)) + +and extern_notation (custom,scopes as allscopes) vars t rules = + match rules with | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> let loc = Glob_ops.loc_of_glob_constr t in @@ -1211,7 +1199,15 @@ let extern_glob_type vars c = (******************************************************************) (* Main translation function from constr -> constr_expr *) -let extern_constr_gen lax goal_concl_style scopt env sigma t = +let extern_constr ?lax ?(inctx=false) ?scope env sigma t = + let r = Detyping.detype Detyping.Later ?lax false Id.Set.empty env sigma t in + let vars = vars_of_env env in + extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r + +let extern_constr_in_scope ?lax ?inctx scope env sigma t = + extern_constr ?lax ?inctx ~scope env sigma t + +let extern_type ?lax ?(goal_concl_style=false) env sigma t = (* "goal_concl_style" means do alpha-conversion using the "goal" convention *) (* i.e.: avoid using the names of goal/section/rel variables and the short *) (* names of global definitions of current module when computing names for *) @@ -1220,30 +1216,18 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t = (* those goal/section/rel variables that occurs in the subterm under *) (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in - let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in - let vars = vars_of_env env in - extern false (InConstrEntrySomeLevel,(scopt,[])) vars r - -let extern_constr_in_scope goal_concl_style scope env sigma t = - extern_constr_gen false goal_concl_style (Some scope) env sigma t - -let extern_constr ?(lax=false) goal_concl_style env sigma t = - extern_constr_gen lax goal_concl_style None env sigma t - -let extern_type goal_concl_style env sigma t = - let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in - let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in + let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) -let extern_closed_glob ?lax goal_concl_style env sigma t = +let extern_closed_glob ?lax ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma t = let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in - extern false (InConstrEntrySomeLevel,(None,[])) vars r + extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r (******************************************************************) (* Main translation function from pattern -> constr_expr *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index e22dd2be86..fa263cbeb7 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -28,7 +28,8 @@ val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr -val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob_constr -> constr_expr +val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> + env -> Evd.evar_map -> closed_glob_constr -> constr_expr (** If [b=true] in [extern_constr b env c] then the variables in the first level of quantification clashing with the variables in [env] are renamed. @@ -36,10 +37,12 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob env, sigma *) -val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr -val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr +val extern_constr : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> + env -> Evd.evar_map -> constr -> constr_expr +val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name -> + env -> Evd.evar_map -> constr -> constr_expr val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid -val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr +val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> types -> constr_expr val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> rel_context -> local_binder_expr list @@ -92,5 +95,3 @@ val toggle_scope_printing : val toggle_notation_printing : ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit - - diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ff115a3e48..c699f79351 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -256,7 +256,9 @@ type intern_env = { unb: bool; tmp_scope: Notation_term.tmp_scope_name option; scopes: Notation_term.scope_name list; - impls: internalization_env } + impls: internalization_env; + impl_binder_index: int option; +} (**********************************************************************) (* Remembering the parsing scope of variables in notations *) @@ -317,27 +319,50 @@ let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body) (**********************************************************************) (* Utilities for binders *) -let build_impls = function - |Implicit -> (function - |Name id -> Some (id, Impargs.Manual, (true,true)) - |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true))) - |Explicit -> fun _ -> None - -let impls_type_list ?(args = []) = - let rec aux acc c = match DAst.get c with - | GProd (na,bk,_,c) -> aux ((build_impls bk na)::acc) c - | _ -> (Variable,[],List.append args (List.rev acc),[]) + +let warn_shadowed_implicit_name = + CWarnings.create ~name:"shadowed-implicit-name" ~category:"syntax" + Pp.(fun na -> str "Making shadowed name of implicit argument accessible by position.") + +let exists_name na l = + match na with + | Name id -> List.exists (function Some (ExplByName id',_,_) -> Id.equal id id' | _ -> false) l + | _ -> false + +let build_impls ?loc n bk na acc = + match bk with + | Implicit -> + let na = + 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 + | Explicit -> None :: acc + +let impls_binder_list = + let rec aux acc n = function + | (na,bk,None,_) :: binders -> aux (build_impls n bk na acc) (n+1) binders + | (na,bk,Some _,_) :: binders -> aux acc n binders + | [] -> (n,acc) in aux [] -let impls_term_list ?(args = []) = - let rec aux acc c = match DAst.get c with - | GLambda (na,bk,_,c) -> aux ((build_impls bk na)::acc) c +let impls_type_list n ?(args = []) = + let rec aux acc n c = match DAst.get c with + | GProd (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c + | _ -> (Variable,[],List.rev acc,[]) + in aux args n + +let impls_term_list n ?(args = []) = + let rec aux acc n c = match DAst.get c with + | GLambda (na,bk,_,c) -> aux (build_impls n bk na acc) (n+1) c | GRec (fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in - let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in - aux acc' bds.(nb) - |_ -> (Variable,[],List.append args (List.rev acc),[]) - in aux [] + let n,acc' = List.fold_left (fun (n,acc) (na, bk, _, _) -> (n+1,build_impls n bk na acc)) (n,acc) args.(nb) in + aux acc' n bds.(nb) + |_ -> (Variable,[],List.rev acc,[]) + in aux args n (* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *) let rec check_capture ty = let open CAst in function @@ -396,6 +421,14 @@ 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 = + CWarnings.create ~name:"unexpected-implicit-declaration" ~category:"syntax" + Pp.(fun () -> str "Unexpected implicit binder declaration.") + +let check_implicit_meaningful ?loc k env = + if k = Implicit && env.impl_binder_index = None then + warn_unexpected_implicit_binder_declaration ?loc () + let intern_generalized_binder intern_type ntnvars env {loc;v=na} b' t ty = let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in @@ -408,6 +441,7 @@ 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 bl = List.map CAst.(map (fun id -> (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) @@ -423,8 +457,10 @@ let intern_generalized_binder intern_type ntnvars | _ -> default_non_dependent_ident in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name - | _ -> na - in (push_name_env ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl + | _ -> na in + let impls = impls_type_list 1 ty' in + (push_name_env ntnvars impls env' (make ?loc na), + (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 @@ -432,9 +468,10 @@ let intern_assumption intern ntnvars env nal bk ty = | Default k -> let ty = intern_type env ty in check_capture ty nal; - let impls = impls_type_list ty in + 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; (push_name_env ntnvars impls env locna, (make ?loc (na,k,locate_if_hole ?loc na ty))::bl)) (env, []) nal @@ -457,7 +494,8 @@ 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 - (push_name_env ntnvars (impls_term_list term) env locna, + let impls = impls_term_list 1 term in + (push_name_env ntnvars impls env locna, (na,Explicit,term,ty)) let intern_cases_pattern_as_binder ?loc ntnvars env p = @@ -1105,7 +1143,8 @@ let interp_reference vars r = let (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} + tmp_scope = None; scopes = []; impls = empty_internalization_env; + impl_binder_index = None} Environ.empty_named_context_val (vars, Id.Map.empty) None [] r in r @@ -1872,10 +1911,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* We add the recursive functions to the environment *) let env_rec = List.fold_left_i (fun i en name -> let (_,bli,tyi,_) = idl_temp.(i) in - let bli = List.filter (fun (_, _, t, _) -> t = None) bli in - let fix_args = List.map (fun (na, bk, t, _) -> build_impls bk na) bli in - push_name_env ntnvars (impls_type_list ~args:fix_args tyi) - en (CAst.make @@ Name name)) 0 env lf in + let binder_index,fix_args = impls_binder_list 1 bli in + let impls = impls_type_list ~args:fix_args binder_index tyi in + push_name_env ntnvars impls en (CAst.make @@ Name name)) 0 env lf in let idl = Array.map2 (fun (_,_,_,_,bd) (n,bl,ty,before_impls) -> (* We add the binders common to body and type to the environment *) let env_body = restore_binders_impargs env_rec before_impls in @@ -1904,9 +1942,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (bl,intern_type env' ty,bl_impls)) dl in let env_rec = List.fold_left_i (fun i en name -> let (bli,tyi,_) = idl_tmp.(i) in - let bli = List.filter (fun (_, _, t, _) -> t = None) bli in - let cofix_args = List.map (fun (na, bk, _, _) -> build_impls bk na) bli in - push_name_env ntnvars (impls_type_list ~args:cofix_args tyi) + let binder_index,cofix_args = impls_binder_list 1 bli in + push_name_env ntnvars (impls_type_list ~args:cofix_args binder_index tyi) en (CAst.make @@ Name name)) 0 env lf in let idl = Array.map2 (fun (_,_,_,bd) (b,c,bl_impls) -> (* We add the binders common to body and type to the environment *) @@ -1927,11 +1964,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in expand_binders ?loc mkGLambda bl (intern env' c2) | CLetIn (na,c1,t,c2) -> - let inc1 = intern (reset_tmp_scope env) c1 in - let int = Option.map (intern_type env) t in + let inc1 = intern_restart_implicit (reset_tmp_scope env) c1 in + let int = Option.map (intern_type_restart_implicit env) t in DAst.make ?loc @@ GLetIn (na.CAst.v, inc1, int, - intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) + intern_restart_implicit (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))) @@ -2114,7 +2151,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* Parsing existential variables *) | CEvar (n, l) -> DAst.make ?loc @@ - GEvar (n, List.map (on_snd (intern env)) l) + GEvar (n, List.map (on_snd (intern_no_implicit env)) l) | CPatVar _ -> raise (InternalizationError (loc,IllegalMetavariable)) (* end *) @@ -2127,8 +2164,14 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = ) and intern_type env = intern (set_type_scope env) + and intern_no_implicit env = intern {env with impl_binder_index = None} + + and intern_restart_implicit env = intern {env with impl_binder_index = Some 0} + + and intern_type_restart_implicit env = intern {(set_type_scope env) with impl_binder_index = Some 0} + and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list = - intern_local_binder_aux intern ntnvars env bind + intern_local_binder_aux intern_restart_implicit ntnvars env bind (* Expands a multiple pattern into a disjunction of multiple patterns *) and intern_multiple_pattern env n pl = @@ -2160,7 +2203,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = and intern_case_item env forbidden_names_for_gen (tm,na,t) = (* the "match" part *) - let tm' = intern env tm in + let tm' = intern_no_implicit env tm in (* the "as" part *) let extra_id,na = let loc = tm'.CAst.loc in @@ -2229,7 +2272,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let id = name_of_implicit imp in let (_,a) = Id.Map.find id eargs in let eargs' = Id.Map.remove id eargs in - intern enva a :: aux (n+1) impl' subscopes' eargs' rargs + intern_no_implicit enva a :: aux (n+1) impl' subscopes' eargs' rargs with Not_found -> if List.is_empty rargs && Id.Map.is_empty eargs && not (maximal_insertion_of imp) then (* Less regular arguments than expected: complete *) @@ -2241,7 +2284,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = ) :: aux (n+1) impl' subscopes' eargs rargs end | (imp::impl', a::rargs') -> - intern enva a :: aux (n+1) impl' subscopes' eargs rargs' + intern_no_implicit enva a :: aux (n+1) impl' subscopes' eargs rargs' | (imp::impl', []) -> if not (Id.Map.is_empty eargs) then (let (id,(loc,_)) = Id.Map.choose eargs in @@ -2271,7 +2314,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | [] -> [] | a::args -> let (enva,subscopes) = apply_scope_env env subscopes in - (intern enva a) :: (intern_args env subscopes args) + (intern_no_implicit enva a) :: (intern_args env subscopes args) in try @@ -2307,7 +2350,7 @@ let intern_gen kind env sigma let tmp_scope = scope_of_type_kind sigma kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; - impls = impls} + impls; impl_binder_index = Some 0} pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c @@ -2389,7 +2432,8 @@ 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 - internalize env {ids; unb = false; tmp_scope; scopes = []; impls} + internalize env + {ids; unb = false; tmp_scope; scopes = []; impls; impl_binder_index = Some 0} pattern_mode (ltacvars, vl) c let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = @@ -2397,7 +2441,8 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = (* [vl] is intended to remember the scope of the free variables of [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} + let c = internalize env + {ids; unb = false; tmp_scope = None; scopes = []; impls; impl_binder_index = 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] *) @@ -2433,7 +2478,8 @@ let intern_context env impl_env binders = 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; - tmp_scope = None; scopes = []; impls = impl_env}, []) binders in + tmp_scope = None; scopes = []; impls = impl_env; + impl_binder_index = Some 0}, []) 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) diff --git a/interp/impargs.ml b/interp/impargs.ml index 2aa002ead1..df28b32f81 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -20,6 +20,7 @@ open Libobject open EConstr open Reductionops open Namegen +open Constrexpr module NamedDecl = Context.Named.Declaration @@ -289,7 +290,7 @@ type force_inference = bool (* true = always infer, never turn into evar/subgoal type implicit_status = (* None = Not implicit *) - (Id.t * implicit_explanation * (maximal_insertion * force_inference)) option + (explicitation * implicit_explanation * (maximal_insertion * force_inference)) option type implicit_side_condition = DefaultImpArgs | LessArgsThan of int @@ -299,9 +300,12 @@ let is_status_implicit = function | None -> false | _ -> true +let name_of_pos k = Id.of_string ("arg_" ^ string_of_int k) + let name_of_implicit = function | None -> anomaly (Pp.str "Not an implicit argument.") - | Some (id,_,_) -> id + | Some (ExplByName id,_,_) -> id + | Some (ExplByPos (k,_),_,_) -> name_of_pos k let maximal_insertion_of = function | Some (_,_,(b,_)) -> b @@ -336,7 +340,7 @@ 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 (id,imp,(set_maximality imps' f.maximal,true)) :: imps' + Some (ExplByName id,imp,(set_maximality imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps let set_manual_implicits flags enriching autoimps l = @@ -346,15 +350,14 @@ let set_manual_implicits flags enriching autoimps l = let imps' = merge (k+1) autoimps explimps in begin match autoimp, explimp.CAst.v with | (Name id,_), Some (_,max) -> - Some (id, Manual, (set_maximality imps' max, true)) + Some (ExplByName id, Manual, (set_maximality imps' max, true)) | (Name id,Some exp), None when enriching -> - Some (id, exp, (set_maximality imps' flags.maximal, true)) + Some (ExplByName id, exp, (set_maximality imps' flags.maximal, true)) | (Name _,_), None -> None | (Anonymous,_), Some (Name id,max) -> - Some (id,Manual,(max,true)) + Some (ExplByName id,Manual,(max,true)) | (Anonymous,_), Some (Anonymous,max) -> - let id = Id.of_string ("arg_" ^ string_of_int k) in - Some (id,Manual,(max,true)) + Some (ExplByPos (k,None),Manual,(max,true)) | (Anonymous,_), None -> None end :: imps' | [], [] -> [] @@ -464,7 +467,7 @@ let implicits_of_global ref = | [], _ -> [] | _, [] -> implicits | Some (_, x,y) :: implicits, Name id :: names -> - Some (id, x,y) :: rename implicits names + Some (ExplByName id, x,y) :: rename implicits names | imp :: implicits, _ :: names -> imp :: rename implicits names in List.map (fun (t, il) -> t, rename il rename_l) l @@ -494,7 +497,7 @@ 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 (id, Manual, (true, true)) + | Glob_term.Implicit -> Some (ExplByName id, Manual, (true, true)) | Glob_term.Explicit -> None in List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx) @@ -655,12 +658,12 @@ 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 (id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps) + Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps) | Name id :: autoimps, Implicit :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in let max = set_maximality imps' false in if max then warn_set_maximal_deprecated i; - Some (id, Manual, (max, true)) :: imps' + 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.")) diff --git a/interp/impargs.mli b/interp/impargs.mli index 8fa69e818a..ef3c2496f4 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -68,7 +68,7 @@ type maximal_insertion = bool (** true = maximal contextual insertion *) type force_inference = bool (** true = always infer, never turn into evar/subgoal *) -type implicit_status = (Id.t * implicit_explanation * +type implicit_status = (Constrexpr.explicitation * implicit_explanation * (maximal_insertion * force_inference)) option (** [None] = Not implicit *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ff2498386d..265ca58ed9 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1225,7 +1225,7 @@ let rec match_ inner u alp metas sigma a1 a2 = bind_bindinglist_env alp sigma id [DAst.make @@ GLocalAssum (Name id',Explicit,t1)] else match_names metas (alp,sigma) (Name id') na in - match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2 + match_in u alp metas sigma (mkGApp a1 [DAst.make @@ GVar id']) b2 | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ |