diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 8 | ||||
| -rw-r--r-- | interp/declare.ml | 3 | ||||
| -rw-r--r-- | interp/declare.mli | 1 | ||||
| -rw-r--r-- | interp/impargs.ml | 67 | ||||
| -rw-r--r-- | interp/impargs.mli | 9 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 5 |
6 files changed, 68 insertions, 25 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/declare.ml b/interp/declare.ml index 175f9c66df..4371b15c82 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -430,9 +430,6 @@ let assumption_message id = discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") -let register_message id = - Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is registered") - (** Monomorphic universes need to survive sections. *) let input_universe_context : Univ.ContextSet.t -> Libobject.obj = diff --git a/interp/declare.mli b/interp/declare.mli index 6f53d6872b..8f1e73c88c 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -74,7 +74,6 @@ val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool val definition_message : Id.t -> unit val assumption_message : Id.t -> unit -val register_message : Id.t -> unit val fixpoint_message : int array option -> Id.t list -> unit val cofixpoint_message : Id.t list -> unit val recursive_message : bool (** true = fixpoint *) -> 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 : diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 890c24e633..7d7e10a05b 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -908,11 +908,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) (* TODO: look at the consequences for alp *) alp, add_env alp sigma var (DAst.make @@ GVar id) -let force_cases_pattern c = - DAst.make ?loc:c.CAst.loc (DAst.get c) - let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c = - let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in + let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) let patl' = Id.List.assoc var binders in |