diff options
Diffstat (limited to 'interp')
34 files changed, 127 insertions, 256 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 3ebbbdfb88..e4af0fcee0 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index bcb2f34377..8fce24249c 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index f1a8ed202f..3ed240d356 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 701c07dc8d..8573dccdf9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f09b316cd6..7b8b93377b 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1a81dc41a1..be8f99028c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -372,6 +372,9 @@ let check_hidden_implicit_parameters ?loc id impls = strbrk "a parameter of the inductive type; bound variables in " ++ 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} + let push_name_env ?(global_level=false) ntnvars implargs env = let open CAst in function @@ -386,15 +389,23 @@ let push_name_env ?(global_level=false) ntnvars implargs env = set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars; if global_level then Dumpglob.dump_definition CAst.(make ?loc id) true "var" else Dumpglob.dump_binding ?loc id; - {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} + pure_push_name_env (id,implargs) env + +let remember_binders_impargs env bl = + List.map_filter (fun (na,_,_,_) -> + match na with + | Anonymous -> None + | Name id -> Some (id,Id.Map.find id env.impls)) bl + +let restore_binders_impargs env l = + List.fold_right pure_push_name_env l env let intern_generalized_binder ?(global_level=false) 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 let ty, ids' = - if t then ty, ids else - Implicit_quantifiers.implicit_application ids - Implicit_quantifiers.combine_params_freevar ty + if t then ty, ids + else Implicit_quantifiers.implicit_application ids ty in let ty' = intern_type {env with ids = ids; unb = true} ty in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in @@ -1300,7 +1311,7 @@ let find_pattern_variable qid = if qualid_is_ident qid then qualid_basename qid else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid)) -let check_duplicate loc fields = +let check_duplicate ?loc fields = let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in let dups = List.duplicates eq fields in match dups with @@ -1345,7 +1356,7 @@ let sort_fields ~complete loc fields completer = try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in - let () = check_duplicate loc fields in + let () = check_duplicate ?loc fields in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) @@ -1835,7 +1846,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = in apply_impargs c env imp subscopes l loc - | CFix ({ CAst.loc = locid; v = iddef}, dl) -> + | CFix ({ CAst.loc = locid; v = iddef}, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in let dl = Array.of_list dl in let n = @@ -1857,14 +1868,18 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = rbefore) recarg in let (env',rbl) = List.fold_left intern_local_binder (env',rbefore) after in let bl = List.rev (List.map glob_local_binder_of_extended rbl) in - (n, bl, intern_type env' ty, env')) dl in - let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') -> - let env'' = List.fold_left_i (fun i en name -> - let (_,bli,tyi,_) = idl_temp.(i) in - let fix_args = (List.map (fun (na, bk, _, _) -> (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 - (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in + let bl_impls = remember_binders_impargs env' bl in + (n, bl, intern_type env' ty, bl_impls)) dl in + (* 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 fix_args = (List.map (fun (na, bk, _, _) -> 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 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 + (n,bl,ty,intern {env_body with tmp_scope = None} bd)) dl idl_temp in DAst.make ?loc @@ GRec (GFix (Array.map (fun (ro,_,_,_) -> ro) idl,n), @@ -1884,15 +1899,18 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let idl_tmp = Array.map (fun ({ CAst.loc; v = id },bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in - (List.rev (List.map glob_local_binder_of_extended rbl), - intern_type env' ty,env')) dl in - let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') -> - let env'' = List.fold_left_i (fun i en name -> - let (bli,tyi,_) = idl_tmp.(i) 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) - en (CAst.make @@ Name name)) 0 env' lf in - (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in + let bl = List.rev (List.map glob_local_binder_of_extended rbl) in + let bl_impls = remember_binders_impargs env' bl in + (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 cofix_args = List.map (fun (na, bk, _, _) -> build_impls bk na) bli in + push_name_env ntnvars (impls_type_list ~args:cofix_args 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 *) + let env_body = restore_binders_impargs env_rec bl_impls in + (b,c,intern {env_body with tmp_scope = None} bd)) dl idl_tmp in DAst.make ?loc @@ GRec (GCoFix n, Array.of_list lf, @@ -2435,10 +2453,8 @@ 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 - let na = match na with Name n -> Some n | Anonymous -> None in - (ExplByPos (n, na), (true, true, true)) :: impls - else impls + if k == Implicit then CAst.make (Some (na,true)) :: impls + else CAst.make None :: impls in (push_rel d env, sigma, d::params, succ n, impls) | Some b -> @@ -2447,7 +2463,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = let d = LocalDef (make_annot na r, c, t) in (push_rel d env, sigma, d::params, n, impls)) (env,sigma,[],k+1,[]) (List.rev bl) - in sigma, ((env, par), impls) + in sigma, ((env, par), List.rev impls) let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params = let int_env,bl = intern_context global_level env impl_env params in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 0d4bc91f57..6c1f4898d9 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -61,10 +61,10 @@ type internalization_env = var_internalization_data Id.Map.t val empty_internalization_env : internalization_env val compute_internalization_data : env -> evar_map -> var_internalization_type -> - types -> Impargs.manual_explicitation list -> var_internalization_data + types -> Impargs.manual_implicits -> var_internalization_data val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type -> - Id.t list -> types list -> Impargs.manual_explicitation list list -> + Id.t list -> types list -> Impargs.manual_implicits list -> internalization_env type ltac_sign = { @@ -189,3 +189,7 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b (** Placeholder for global option, should be moved to a parameter *) val get_asymmetric_patterns : unit -> bool + +val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit +(** Check that a list of record field definitions doesn't contain + duplicates. *) diff --git a/interp/declare.ml b/interp/declare.ml index 17de06ed57..77313a54de 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/declare.mli b/interp/declare.mli index e2485d7cf0..0f64235048 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/deprecation.ml b/interp/deprecation.ml index b6f0dceb89..3b02ba4664 100644 --- a/interp/deprecation.ml +++ b/interp/deprecation.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/deprecation.mli b/interp/deprecation.mli index aab87c11a2..f8083c2a5b 100644 --- a/interp/deprecation.mli +++ b/interp/deprecation.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 274f9b851a..e1269025a4 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 554da7603f..18955985a0 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/genintern.ml b/interp/genintern.ml index 1b736b7977..e74f8d5f10 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/genintern.mli b/interp/genintern.mli index 4100f39029..5619a7b648 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/impargs.ml b/interp/impargs.ml index f3cdd64633..9977b29310 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -20,7 +20,6 @@ open Lib open Libobject open EConstr open Reductionops -open Constrexpr open Namegen module NamedDecl = Context.Named.Declaration @@ -341,77 +340,30 @@ let rec prepare_implicits f = function Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps -(* -If found, returns Some (x,(b,fi,fo)) and l with the entry removed, -otherwise returns None and l unchanged. - *) -let assoc_by_pos k l = - let rec aux = function - (ExplByPos (k', x), b) :: tl when Int.equal k k' -> Some (x,b), tl - | hd :: tl -> let (x, tl) = aux tl in x, hd :: tl - | [] -> raise Not_found - in try aux l with Not_found -> None, l - -let check_correct_manual_implicits autoimps l = - List.iter (function - | ExplByName id,(b,fi,forced) -> - if not forced then - user_err - (str "Wrong or non-dependent implicit argument name: " ++ Id.print id ++ str ".") - | ExplByPos (i,_id),_t -> - if i<1 || i>List.length autoimps then - user_err - (str "Bad implicit argument number: " ++ int i ++ str ".") - else - user_err - (str "Cannot set implicit argument number " ++ int i ++ - str ": it has no name.")) l - -(* Take a list l of explicitations, and map them to positions. *) -let flatten_explicitations l autoimps = - let rec aux k l = function - | (Name id,_)::imps -> - let value, l' = - try - let eq = Constrexpr_ops.explicitation_eq in - let flags = List.assoc_f eq (ExplByName id) l in - Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l - with Not_found -> assoc_by_pos k l - in value :: aux (k+1) l' imps - | (Anonymous,_)::imps -> - let value, l' = assoc_by_pos k l - in value :: aux (k+1) l' imps - | [] when List.is_empty l -> [] - | [] -> - check_correct_manual_implicits autoimps l; - [] - in aux 1 l autoimps - let set_manual_implicits flags enriching autoimps l = - if not (List.distinct l) then - user_err Pp.(str "Some parameters are referred more than once."); (* 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 with - | (Name id,_), Some (_, (b, fi, _)) -> - Some (id, Manual, (set_maximality imps' b, fi)) + begin match autoimp, explimp.CAst.v with + | (Name id,_), Some (_,max) -> + Some (id, Manual, (set_maximality imps' max, true)) | (Name id,Some exp), None when enriching -> Some (id, exp, (set_maximality imps' flags.maximal, true)) | (Name _,_), None -> None - | (Anonymous,_), Some (Some id, (b, fi, true)) -> - Some (id,Manual,(b,fi)) - | (Anonymous,_), Some (None, (b, fi, true)) -> + | (Anonymous,_), Some (Name id,max) -> + Some (id,Manual,(max,true)) + | (Anonymous,_), Some (Anonymous,max) -> let id = Id.of_string ("arg_" ^ string_of_int k) in - Some (id,Manual,(b,fi)) - | (Anonymous,_), Some (_, (_, _, false)) -> None + Some (id,Manual,(max,true)) | (Anonymous,_), None -> None end :: imps' | [], [] -> [] - (* flatten_explicitations returns a list of the same length as autoimps *) - | _ -> assert false - in merge 1 autoimps (flatten_explicitations l autoimps) + | [], _ -> assert false + (* possibly more automatic than manual implicit arguments n + when the conclusion is an unfoldable constant *) + | autoimps, [] -> merge k autoimps [CAst.make None] + in merge 1 autoimps l let compute_semi_auto_implicits env sigma f t = if not f.auto then [DefaultImpArgs, []] @@ -642,9 +594,7 @@ let declare_mib_implicits kn = (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) (* Declare manual implicits *) -type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool) - -type manual_implicits = manual_explicitation list +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 @@ -669,8 +619,6 @@ 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 @@ -685,9 +633,8 @@ let declare_manual_implicits local ref ?enriching l = 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 + if List.exists (fun x -> x.CAst.v <> None) l then + declare_manual_implicits local ref ?enriching l (* TODO: either turn these warnings on and document them, or handle these cases sensibly *) @@ -750,12 +697,6 @@ let extract_impargs_data impls = | [] -> [] in aux 0 impls -let lift_implicits n = - List.map (fun x -> - match fst x with - ExplByPos (k, id) -> ExplByPos (k + n, id), snd x - | _ -> x) - let make_implicits_list l = [DefaultImpArgs, l] let rec drop_first_implicits p l = diff --git a/interp/impargs.mli b/interp/impargs.mli index 1099074c63..90a7944642 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -84,13 +84,7 @@ val force_inference_of : implicit_status -> bool val positions_of_implicits : implicits_list -> int list -(** A [manual_explicitation] is a tuple of a positional or named explicitation with - maximal insertion, force inference and force usage flags. Forcing usage makes - the argument implicit even if the automatic inference considers it not inferable. *) -type manual_explicitation = Constrexpr.explicitation * - (maximal_insertion * force_inference * bool) - -type manual_implicits = manual_explicitation list +type manual_implicits = (Name.t * bool) option CAst.t list val compute_implicits_with_manual : env -> Evd.evar_map -> types -> bool -> manual_implicits -> implicit_status list @@ -131,8 +125,6 @@ val implicits_of_global : GlobRef.t -> implicits_list list val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list -val lift_implicits : int -> manual_implicits -> manual_implicits - val make_implicits_list : implicit_status list -> implicits_list list val drop_first_implicits : int -> implicits_list -> implicits_list diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index bac46c2d2f..9f6281ae15 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -23,9 +23,6 @@ open Libobject open Nameops open Context.Rel.Declaration -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) -let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) - module RelDecl = Context.Rel.Declaration (*i*) @@ -66,9 +63,6 @@ let declare_generalizable ~local gen = let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table -let ids_of_list l = - List.fold_right Id.Set.add l Id.Set.empty - let is_global id = try ignore (Nametab.locate_extended (qualid_of_ident id)); true with Not_found -> false @@ -105,26 +99,6 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c -let ids_of_names l = - List.fold_left (fun acc x -> match x.CAst.v with Name na -> na :: acc | Anonymous -> acc) [] l - -let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = - let rec aux bdvars l c = match c with - ((CLocalAssum (n, _, c)) :: tl) -> - let bound = ids_of_names n in - let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - - | ((CLocalDef (n, c, t)) :: tl) -> - let bound = match n.CAst.v with Anonymous -> [] | Name n -> [n] in - let l' = free_vars_of_constr_expr c ~bound:bdvars l in - let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in - aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl - - | CLocalPattern _ :: tl -> assert false - | [] -> bdvars, l - in aux bound l binders - let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = let rec vars bound vs c = match DAst.get c with | GVar id -> @@ -149,7 +123,7 @@ let next_name_away_from na avoid = | Anonymous -> make_fresh avoid (Global.env ()) (Id.of_string "anon") | Name id -> make_fresh avoid (Global.env ()) id -let combine_params avoid fn applied needed = +let combine_params avoid applied needed = let named, applied = List.partition (function @@ -167,47 +141,30 @@ let combine_params avoid fn applied needed = (fun x -> match x with (t, Some {CAst.loc;v=ExplByName id}) -> id, t | _ -> assert false) named in - let is_unset (_, decl) = match decl with - | LocalAssum _ -> true - | LocalDef _ -> false - in - let needed = List.filter is_unset needed in let rec aux ids avoid app need = match app, need with - [], [] -> List.rev ids, avoid - | app, (_, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need when Id.List.mem_assoc id named -> + | _, (_, LocalDef _) :: need -> aux ids avoid app need + + | [], [] -> List.rev ids, avoid + + | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named -> aux (Id.List.assoc id named :: ids) avoid app need - | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need -> + | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need -> aux (x :: ids) avoid app need - | _, (Some cl, _ as d) :: need -> - let t', avoid' = fn avoid d in - aux (t' :: ids) avoid' app need - | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need - | [], (None, _ as decl) :: need -> - let t', avoid' = fn avoid decl in - aux (t' :: ids) avoid' app need + | _, (Some _, decl) :: need | [], (None, decl) :: need -> + let id' = next_name_away_from (RelDecl.get_name decl) avoid in + let t' = CAst.make @@ CRef (qualid_of_ident id',None) in + aux (t' :: ids) (Id.Set.add id' avoid) app need | (x,_) :: _, [] -> user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") - in aux [] avoid applied needed - -let combine_params_freevar avoid (_, decl) = - let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) - -let destClassApp cl = - let open CAst in - let loc = cl.loc in - match cl.v with - | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst) - | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst) - | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) - | _ -> raise Not_found + in + aux [] avoid applied needed let destClassAppExpl cl = let open CAst in @@ -217,7 +174,7 @@ let destClassAppExpl cl = | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) | _ -> raise Not_found -let implicit_application env ?(allow_partial=true) f ty = +let implicit_application env ty = let is_class = try let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in @@ -230,24 +187,13 @@ let implicit_application env ?(allow_partial=true) f ty = match is_class with | None -> ty, env | Some ({CAst.loc;v=(id, par, inst)}, gr) -> - let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in + let avoid = Id.Set.union env (Id.Set.of_list (free_vars_of_constr_expr ty ~bound:env [])) in let env = Global.env () in let sigma = Evd.from_env env in let c = class_info env sigma gr in let (ci, rd) = c.cl_context in - if not allow_partial then - begin - let opt_succ x n = match x with - | None -> succ n - | Some _ -> n - in - let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in - let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in - if not (Int.equal needlen applen) then - mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd - end; let pars = List.rev (List.combine ci rd) in - let args, avoid = combine_params avoid f par pars in + let args, avoid = combine_params avoid par pars in CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid let warn_ignoring_implicit_status = @@ -257,32 +203,23 @@ let warn_ignoring_implicit_status = Name.print na ++ strbrk " and following binders") let implicits_of_glob_constr ?(with_products=true) l = - let add_impl i na bk l = match bk with - | Implicit -> - let name = - match na with - | Name id -> Some id - | Anonymous -> None - in - (ExplByPos (i, name), (true, true, true)) :: l - | _ -> l + let add_impl ?loc na bk l = match bk with + | Implicit -> CAst.make ?loc (Some (na,true)) :: l + | _ -> CAst.make ?loc None :: l in - let rec aux i c = - let abs na bk b = - add_impl i na bk (aux (succ i) b) - in + let rec aux c = match DAst.get c with | GProd (na, bk, t, b) -> - if with_products then abs na bk b + 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 | _ -> () in [] - | GLambda (na, bk, t, b) -> abs na bk b - | GLetIn (na, b, t, c) -> aux i c + | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b) + | GLetIn (na, b, t, c) -> aux c | GRec (fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in - List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) + List.fold_right (fun (na,bk,t,_) l -> add_impl ?loc:c.CAst.loc na bk l) args.(nb) (aux bds.(nb)) | _ -> [] - in aux 1 l + in aux l diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 437fef1753..4f9c47ec36 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -11,22 +11,14 @@ open Names open Glob_term open Constrexpr -open Libnames val declare_generalizable : local:bool -> lident list option -> unit -val ids_of_list : Id.t list -> Id.Set.t -val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t -val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t - (** Fragile, should be used only for construction a set of identifiers to avoid *) val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t -> Id.t list -> Id.t list -val free_vars_of_binders : - ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list - (** Returns the generalizable free ids in left-to-right order with the location of their first occurrence *) @@ -37,15 +29,4 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits -val combine_params_freevar : - Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> - Constrexpr.constr_expr * Id.Set.t - -val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> - Constrexpr.constr_expr * Id.Set.t) -> - constr_expr -> constr_expr * Id.Set.t - -(* Should be likely located elsewhere *) -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) -val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a +val implicit_application : Id.Set.t -> constr_expr -> constr_expr * Id.Set.t diff --git a/interp/modintern.ml b/interp/modintern.ml index 2f516f4f3c..955288244e 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/modintern.mli b/interp/modintern.mli index 529c438c1a..75ab38c64a 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation.ml b/interp/notation.ml index cc06d5abfc..d58125e29b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation.mli b/interp/notation.mli index b32561d908..bd9b50977b 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 08619d912e..fdf12faa04 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 58fa221b16..7919d0061f 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 5024f5c26f..908455bd05 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/reserve.ml b/interp/reserve.ml index edbdf1dbba..e81439c3d5 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/reserve.mli b/interp/reserve.mli index a10858e71f..e180fc8071 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 91491bdf8d..74fe5d1c80 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index e41ef78913..d2770a2e73 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/stdarg.ml b/interp/stdarg.ml index bf3a8fe215..555eb34aed 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/stdarg.mli b/interp/stdarg.mli index c974a4403c..dffbca0054 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 8df04187f1..302bb6ece2 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index e6e3b9cffa..0065b45b14 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) |