diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 8 | ||||
| -rw-r--r-- | interp/impargs.ml | 67 | ||||
| -rw-r--r-- | interp/impargs.mli | 9 |
3 files changed, 67 insertions, 17 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 24894fc9f5..7f1dc70d95 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1188,7 +1188,6 @@ let check_constructor_length env loc cstr len_pl pl0 = (error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr))) -open Term open Declarations (* Similar to Cases.adjust_local_defs but on RCPat *) @@ -1197,16 +1196,15 @@ let insert_local_defs_in_pattern (ind,j) l = if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then (* Optimisation *) l else - let typi = mip.mind_nf_lc.(j-1) in - let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in - let (decls,_) = decompose_prod_assum typi in + let (ctx, _) = mip.mind_nf_lc.(j-1) in + let decls = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in let rec aux decls args = match decls, args with | Context.Rel.Declaration.LocalDef _ :: decls, args -> (DAst.make @@ RCPatAtom None) :: aux decls args | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *) | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args | _ -> assert false in - aux (List.rev decls) l + aux decls l let add_local_defs_and_check_length loc env g pl args = match g with | ConstructRef cstr -> diff --git a/interp/impargs.ml b/interp/impargs.ml index 6fd52d98dd..0f9bff7f1d 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -452,9 +452,10 @@ let compute_mib_implicits flags kn = let ind = (kn,i) in let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), - Array.mapi (fun j c -> + Array.mapi (fun j (ctx, cty) -> + let c = of_constr (Term.it_mkProd_or_LetIn cty ctx) in (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) - (Array.map of_constr mip.mind_nf_lc)) + mip.mind_nf_lc) in Array.mapi imps_one_inductive mib.mind_packets @@ -674,7 +675,7 @@ let check_inclusion l = user_err Pp.(str "Sequences of implicit arguments must be of different lengths."); aux nl | _ -> () in - aux (List.map (fun (imps,_) -> List.length imps) l) + aux (List.map snd l) let check_rigidity isrigid = if not isrigid then @@ -685,6 +686,8 @@ let projection_implicits env p impls = CList.skipn_at_least npars impls let declare_manual_implicits local ref ?enriching l = + assert (List.for_all (fun (_, (max, fi, fu)) -> fi && fu) l); + assert (List.for_all (fun (ex, _) -> match ex with ExplByPos (_,_) -> true | _ -> false) l); let flags = !implicit_args in let env = Global.env () in let sigma = Evd.from_env env in @@ -692,29 +695,71 @@ 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 req = + if is_local local ref then ImplLocal + else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) + in add_anonymous_leaf (inImplicits (req,[ref,l])) + +let maybe_declare_manual_implicits local ref ?enriching l = + match l with + | [] -> () + | _ -> declare_manual_implicits local ref ?enriching l + +(* TODO: either turn these warnings on and document them, or handle these cases sensibly *) + +let warn_set_maximal_deprecated = + CWarnings.create ~name:"set-maximal-deprecated" ~category:"deprecated" + (fun i -> strbrk ("Argument number " ^ string_of_int i ^ " is a trailing implicit so must be maximal")) + +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 -> + Some (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' + | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ -> + 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 + | [], _::_ -> assert false + in aux 0 (autoimps, l) + +let set_implicits local ref l = + let flags = !implicit_args in + let env = Global.env () in + let sigma = Evd.from_env env in + let t, _ = Typeops.type_of_global_in_context env ref in + let t = of_constr t in + let autoimpls = compute_implicits_names env sigma t in let l' = match l with | [] -> assert false | [l] -> - [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] + [DefaultImpArgs, compute_implicit_statuses autoimpls l] | _ -> check_rigidity (is_rigid env sigma t); - let l = List.map (fun imps -> (imps,List.length imps)) l in + (* Sort by number of implicits, decreasing *) + let is_implicit = function + | NotImplicit -> 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 check_inclusion l; let nargs = List.length autoimpls in List.map (fun (imps,n) -> (LessArgsThan (nargs-n), - set_manual_implicits flags enriching autoimpls imps)) l in + compute_implicit_statuses autoimpls imps)) l in let req = if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) in add_anonymous_leaf (inImplicits (req,[ref,l'])) -let maybe_declare_manual_implicits local ref ?enriching l = - match l with - | [] -> () - | _ -> declare_manual_implicits local ref ?enriching [l] - let extract_impargs_data impls = let rec aux p = function | (DefaultImpArgs, imps)::_ -> [None,imps] diff --git a/interp/impargs.mli b/interp/impargs.mli index 43c26b024f..0070423530 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -112,13 +112,20 @@ val declare_implicits : bool -> GlobRef.t -> unit Unsets implicits if [l] is empty. *) val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> - manual_implicits list -> unit + manual_implicits -> unit (** If the list is empty, do nothing, otherwise declare the implicits. *) 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 implicits_of_global : GlobRef.t -> implicits_list list val extract_impargs_data : |