diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 27 | ||||
| -rw-r--r-- | interp/impargs.ml | 61 | ||||
| -rw-r--r-- | interp/impargs.mli | 5 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 10 |
4 files changed, 62 insertions, 41 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f4ae5bf676..ab20f1b3ef 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -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,(true,true)) + | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in + impl + in + match bk with + | NonMaxImplicit -> impl_status false :: acc + | MaxImplicit -> impl_status true :: acc | Explicit -> None :: acc let impls_binder_list = @@ -426,7 +429,7 @@ let warn_unexpected_implicit_binder_declaration = Pp.(fun () -> str "Unexpected implicit binder declaration.") let check_implicit_meaningful ?loc k env = - if k = Implicit && env.impl_binder_index = None then + if k <> Explicit && env.impl_binder_index = None then warn_unexpected_implicit_binder_declaration ?loc () let intern_generalized_binder intern_type ntnvars @@ -444,7 +447,7 @@ let intern_generalized_binder intern_type ntnvars 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)))) + (Name id, MaxImplicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) fvs in let na = match na with @@ -2500,8 +2503,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/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 |