diff options
Diffstat (limited to 'interp')
32 files changed, 796 insertions, 571 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml new file mode 100644 index 0000000000..ca6ea94f09 --- /dev/null +++ b/interp/constrexpr.ml @@ -0,0 +1,152 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Libnames +open Misctypes +open Decl_kinds + +(** {6 Concrete syntax for terms } *) + +(** [constr_expr] is the abstract syntax tree produced by the parser *) +type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl + +type ident_decl = lident * universe_decl_expr option +type name_decl = lname * universe_decl_expr option + +type notation = string + +type explicitation = + | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *) + | ExplByName of Id.t + +type binder_kind = + | Default of binding_kind + | Generalized of binding_kind * binding_kind * bool + (** Inner binding, outer bindings, typeclass-specific flag + for implicit generalization of superclasses *) + +type abstraction_kind = AbsLambda | AbsPi + +type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) + +(** Representation of integer literals that appear in Coq scripts. + We now use raw strings of digits in base 10 (big-endian), and a separate + sign flag. Note that this representation is not unique, due to possible + multiple leading zeros, and -0 = +0 *) + +type sign = bool +type raw_natural_number = string + +type prim_token = + | Numeral of raw_natural_number * sign + | String of string + +type instance_expr = Glob_term.glob_level list + +type cases_pattern_expr_r = + | CPatAlias of cases_pattern_expr * lname + | CPatCstr of reference + * cases_pattern_expr list option * cases_pattern_expr list + (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) + | CPatAtom of reference option + | CPatOr of cases_pattern_expr list + | CPatNotation of notation * cases_pattern_notation_substitution + * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents + (notation n applied with substitution l1) + applied to arguments l2 *) + | CPatPrim of prim_token + | CPatRecord of (reference * cases_pattern_expr) list + | CPatDelimiters of string * cases_pattern_expr + | CPatCast of cases_pattern_expr * constr_expr +and cases_pattern_expr = cases_pattern_expr_r CAst.t + +and cases_pattern_notation_substitution = + cases_pattern_expr list * (** for constr subterms *) + cases_pattern_expr list list (** for recursive notations *) + +and constr_expr_r = + | CRef of reference * instance_expr option + | CFix of lident * fix_expr list + | CCoFix of lident * cofix_expr list + | CProdN of local_binder_expr list * constr_expr + | CLambdaN of local_binder_expr list * constr_expr + | CLetIn of lname * constr_expr * constr_expr option * constr_expr + | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list + | CApp of (proj_flag * constr_expr) * + (constr_expr * explicitation CAst.t option) list + | CRecord of (reference * constr_expr) list + + (* representation of the "let" and "match" constructs *) + | CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *) + * constr_expr option (* return-clause *) + * case_expr list + * branch_expr list (* branches *) + + | CLetTuple of lname list * (lname option * constr_expr option) * + constr_expr * constr_expr + | CIf of constr_expr * (lname option * constr_expr option) + * constr_expr * constr_expr + | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option + | CPatVar of patvar + | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list + | CSort of Glob_term.glob_sort + | CCast of constr_expr * constr_expr cast_type + | CNotation of notation * constr_notation_substitution + | CGeneralization of binding_kind * abstraction_kind option * constr_expr + | CPrim of prim_token + | CDelimiters of string * constr_expr + | CProj of reference * constr_expr +and constr_expr = constr_expr_r CAst.t + +and case_expr = constr_expr (* expression that is being matched *) + * lname option (* as-clause *) + * cases_pattern_expr option (* in-clause *) + +and branch_expr = + (cases_pattern_expr list list * constr_expr) CAst.t + +and fix_expr = + lident * (lident option * recursion_order_expr) * + local_binder_expr list * constr_expr * constr_expr + +and cofix_expr = + lident * local_binder_expr list * constr_expr * constr_expr + +and recursion_order_expr = + | CStructRec + | CWfRec of constr_expr + | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) + +(* Anonymous defs allowed ?? *) +and local_binder_expr = + | CLocalAssum of lname list * binder_kind * constr_expr + | CLocalDef of lname * constr_expr * constr_expr option + | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t + +and constr_notation_substitution = + constr_expr list * (** for constr subterms *) + constr_expr list list * (** for recursive notations *) + cases_pattern_expr list * (** for binders *) + local_binder_expr list list (** for binder lists (recursive notations) *) + +type constr_pattern_expr = constr_expr + +(** Concrete syntax for modules and module types *) + +type with_declaration_ast = + | CWith_Module of Id.t list CAst.t * qualid CAst.t + | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr + +type module_ast_r = + | CMident of qualid + | CMapply of module_ast * module_ast + | CMwith of module_ast * with_declaration_ast +and module_ast = module_ast_r CAst.t diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 4ee13c961f..1be1dd96cb 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -601,7 +601,34 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> asymmetric_patterns:=a); } -(************************************************************************) -(* Deprecated *) -let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c -let prod_constr_expr c bl = mkCProdN ?loc:(local_binders_loc bl) bl c +(** Local universe and constraint declarations. *) + +let interp_univ_constraints env evd cstrs = + let interp (evd,cstrs) (u, d, u') = + let ul = Pretyping.interp_known_glob_level evd u in + let u'l = Pretyping.interp_known_glob_level evd u' in + let cstr = (ul,d,u'l) in + let cstrs' = Univ.Constraint.add cstr cstrs in + try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in + evd, cstrs' + with Univ.UniverseInconsistency e -> + CErrors.user_err ~hdr:"interp_constraint" + (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e) + in + List.fold_left interp (evd,Univ.Constraint.empty) cstrs + +let interp_univ_decl env decl = + let open UState in + let pl : lident list = decl.univdecl_instance in + let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in + let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in + let decl = { univdecl_instance = pl; + univdecl_extensible_instance = decl.univdecl_extensible_instance; + univdecl_constraints = cstrs; + univdecl_extensible_constraints = decl.univdecl_extensible_constraints } + in evd, decl + +let interp_univ_decl_opt env l = + match l with + | None -> Evd.from_env env, UState.default_univ_decl + | Some decl -> interp_univ_decl env decl diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index d038bd71ab..b4f0886acf 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -60,14 +60,6 @@ val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr (** Apply a list of pattern arguments to a pattern *) -(** @deprecated variant of mkCLambdaN *) -val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr -[@@ocaml.deprecated "deprecated variant of mkCLambdaN"] - -(** @deprecated variant of mkCProdN *) -val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr -[@@ocaml.deprecated "deprecated variant of mkCProdN"] - (** {6 Destructors}*) val coerce_reference_to_id : reference -> Id.t @@ -124,3 +116,10 @@ val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a (** Placeholder for global option, should be moved to a parameter *) val asymmetric_patterns : bool ref + +(** Local universe and constraint declarations. *) +val interp_univ_decl : Environ.env -> universe_decl_expr -> + Evd.evar_map * UState.universe_decl + +val interp_univ_decl_opt : Environ.env -> universe_decl_expr option -> + Evd.evar_map * UState.universe_decl diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 19444988b9..86f6ce9ae8 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -14,7 +14,6 @@ open CErrors open Util open Names open Nameops -open Constr open Termops open Libnames open Globnames @@ -29,7 +28,6 @@ open Pattern open Nametab open Notation open Detyping -open Misctypes open Decl_kinds module NamedDecl = Context.Named.Declaration @@ -479,7 +477,8 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function if is_inactive_rule keyrule then raise No_match; let loc = t.loc in match DAst.get t with - | PatCstr (cstr,_,na) -> + | PatCstr (cstr,args,na) -> + let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in let p = apply_notation_to_pattern ?loc (ConstructRef cstr) (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na @@ -590,11 +589,17 @@ let explicitize inctx impl (cf,f) args = let expl () = match ip with | Some i -> - if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then - raise Expl + (* Careful: It is possible to have declared implicits ending + before the principal argument *) + let is_impl = + try is_status_implicit (List.nth impl (i-1)) + with Failure _ -> false + in + if is_impl + then raise Expl else let (args1,args2) = List.chop i args in - let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in + let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in let args1 = exprec 1 (args1,impl1) in let args2 = exprec (i+1) (args2,impl2) in let ip = Some (List.length args1) in @@ -925,7 +930,7 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes) and factorize_prod scopes vars na bk aty c = let store, get = set_temporary_memory () in match na, DAst.get c with - | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) + | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 -> (match get () with | [{CAst.v=(ids,disj_of_patl,b)}] -> @@ -953,7 +958,7 @@ and factorize_prod scopes vars na bk aty c = and factorize_lambda inctx scopes vars na bk aty c = let store, get = set_temporary_memory () in match na, DAst.get c with - | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) + | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 -> (match get () with | [{CAst.v=(ids,disj_of_patl,b)}] -> @@ -1203,7 +1208,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | PIf (c,b1,b2) -> GIf (glob_of_pat avoid env sigma c, (Anonymous,None), glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2) - | PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) -> + | PCase ({cip_style=Constr.LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) -> let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b) | PCase (info,p,tm,bl) -> @@ -1222,9 +1227,37 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p) | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in - GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat) - | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *) - | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))) + GCases (Constr.RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat) + | PFix ((ln,i),(lna,tl,bl)) -> + let def_avoid, def_env, lfi = + Array.fold_left + (fun (avoid, env, l) na -> + let id = Namegen.next_name_away na avoid in + (Id.Set.add id avoid, Name id :: env, id::l)) + (avoid, env, []) lna in + let n = Array.length tl in + let v = Array.map3 + (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t)) + bl tl ln in + GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) + | PCoFix (ln,(lna,tl,bl)) -> + let def_avoid, def_env, lfi = + Array.fold_left + (fun (avoid, env, l) na -> + let id = Namegen.next_name_away na avoid in + (Id.Set.add id avoid, Name id :: env, id::l)) + (avoid, env, []) lna in + let ntys = Array.length tl in + let v = Array.map2 + (fun c t -> share_pattern_names glob_of_pat 0 [] def_avoid def_env sigma c (Patternops.lift_pattern ntys t)) + bl tl in + GRec(GCoFix ln,Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) | PSort s -> GSort s let extern_constr_pattern env sigma pat = diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 8ab70283c8..73c108319f 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -13,13 +13,11 @@ open Termops open EConstr open Environ open Libnames -open Globnames open Glob_term open Pattern open Constrexpr open Notation_term open Notation -open Misctypes open Ltac_pretype (** Translation of pattern, cases pattern, glob_constr and term into syntax @@ -40,7 +38,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob 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_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference +val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference val extern_type : 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 -> @@ -58,9 +56,9 @@ val print_projections : bool ref (** Customization of the global_reference printer *) val set_extern_reference : - (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -> unit + (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) -> unit val get_extern_reference : - unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) + unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) (** WARNING: The following functions are evil due to side-effects. Think of the following case as used in the printer: diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f2cd07c94e..848180743f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -14,6 +14,7 @@ open Util open CAst open Names open Nameops +open Constr open Namegen open Libnames open Globnames @@ -433,7 +434,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in (na,bk,Some c,t) | GLocalPattern (_,_,_,_) -> - Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.") + Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") ) let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd") @@ -525,7 +526,7 @@ let rec expand_binders ?loc mk bl c = let tm = DAst.make ?loc (GVar id) in (* Distribute the disjunctive patterns over the shared right-hand side *) let eqnl = List.map (fun pat -> CAst.make ?loc (ids,[pat],c)) disjpat in - let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in + let c = DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c) (**********************************************************************) @@ -819,11 +820,11 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) -> + | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent -> + | NtnTypeBinder NtnBinderParsedAsConstr AsIdent -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') @@ -980,17 +981,17 @@ let intern_reference ref = in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option = +let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option = match info with - | Misctypes.UAnonymous -> None - | Misctypes.UUnknown -> None - | Misctypes.UNamed id -> Some (id, 0) + | UAnonymous -> None + | UUnknown -> None + | UNamed id -> Some (id, 0) -let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort = +let glob_sort_of_level (level: glob_level) : glob_sort = match level with - | Misctypes.GProp -> Misctypes.GProp - | Misctypes.GSet -> Misctypes.GSet - | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info] + | GProp -> GProp + | GSet -> GSet + | GType info -> GType [sort_info_of_level_info info] (* Is it a global reference or a syntactic definition? *) let intern_qualid qid intern env ntnvars us args = @@ -998,7 +999,7 @@ let intern_qualid qid intern env ntnvars us args = match intern_extended_global_of_qualid qid with | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> - let (ids,c) = Syntax_def.search_syntactic_definition sp in + let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments ?loc; let args1,args2 = List.chop nids args in @@ -1024,7 +1025,7 @@ let intern_qualid qid intern env ntnvars us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end - | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v) @@ -1077,7 +1078,7 @@ let interp_reference vars r = (** Private internalization patterns *) type 'a raw_cases_pattern_expr_r = | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname - | RCPatCstr of Globnames.global_reference + | RCPatCstr of GlobRef.t * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *) | RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option @@ -1140,9 +1141,18 @@ let check_number_of_pattern loc n l = if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = - if List.exists (fun ids' -> not (List.eq_set (fun {loc;v=id} {v=id'} -> Id.equal id id') ids ids')) idsl then - user_err ?loc (str - "The components of this disjunctive pattern must bind the same variables.") + let eq_id {v=id} {v=id'} = Id.equal id id' in + (* Collect remaining patterns which do not have the same variables as the first pattern *) + let idsl = List.filter (fun ids' -> not (List.eq_set eq_id ids ids')) idsl in + match idsl with + | ids'::_ -> + (* Look for an [id] which is either in [ids] and not in [ids'] or in [ids'] and not in [ids] *) + let ids'' = List.subtract eq_id ids ids' in + let ids'' = if ids'' = [] then List.subtract eq_id ids' ids else ids'' in + user_err ?loc + (strbrk "The components of this disjunctive pattern must bind the same variables (" ++ + Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).") + | [] -> () (** Use only when params were NOT asked to the user. @return if letin are included *) @@ -1314,7 +1324,7 @@ let sort_fields ~complete loc fields completer = | [] -> (idx, acc_first_idx, acc) | (Some field_glob_id) :: projs -> let field_glob_ref = ConstRef field_glob_id in - let first_field = eq_gr field_glob_ref first_field_glob_ref in + let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in begin match proj_kinds with | [] -> anomaly (Pp.str "Number of projections mismatch.") | (_, regular) :: proj_kinds -> @@ -1352,7 +1362,7 @@ let sort_fields ~complete loc fields completer = user_err ?loc ~hdr:"intern" (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in let remaining_projs, (field_index, _) = - let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in + let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in try CList.extract_first the_proj remaining_projs with Not_found -> user_err ?loc @@ -1965,7 +1975,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = if List.for_all (irrefutable globalenv) thepats then [] else [CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *) DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in - Some (DAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) + Some (DAst.make @@ GCases(RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in DAst.make ?loc @@ diff --git a/interp/constrintern.mli b/interp/constrintern.mli index f5e32dc4cd..4dd719e1f3 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -13,7 +13,6 @@ open Evd open Environ open Misctypes open Libnames -open Globnames open Glob_term open Pattern open EConstr @@ -143,7 +142,7 @@ val intern_constr_pattern : constr_pattern_expr -> patvar list * constr_pattern (** Raise Not_found if syndef not bound to a name and error if unexisting ref *) -val intern_reference : reference -> global_reference +val intern_reference : reference -> GlobRef.t (** Expands abbreviations (syndef); raise an error if not existing *) val interp_reference : ltac_sign -> reference -> glob_constr @@ -175,11 +174,11 @@ val interp_context_evars : (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) -val locate_reference : Libnames.qualid -> Globnames.global_reference +val locate_reference : Libnames.qualid -> GlobRef.t val is_global : Id.t -> bool -val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference -val global_reference : Id.t -> Globnames.global_reference -val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference +val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> GlobRef.t +val global_reference : Id.t -> GlobRef.t +val global_reference_in_absolute_module : DirPath.t -> Id.t -> GlobRef.t (** Interprets a term as the left-hand side of a notation. The returned map is guaranteed to have the same domain as the input one. *) diff --git a/interp/declare.ml b/interp/declare.ml index c55a6c69ba..bc2d2068a2 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -487,7 +487,7 @@ let add_universe src (dp, i) = Option.iter (fun poly -> let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in Global.push_context_set poly ctx; - Universes.add_global_universe level poly; + UnivNames.add_global_universe level poly; if poly then Lib.add_section_context ctx) optpoly @@ -538,7 +538,7 @@ let input_universe : universe_decl -> Libobject.obj = let declare_univ_binders gr pl = if Global.is_polymorphic gr then - Universes.register_universe_binders gr pl + UnivNames.register_universe_binders gr pl else let l = match gr with | ConstRef c -> Label.to_id @@ Constant.label c @@ -564,7 +564,7 @@ let do_universe poly l = in let l = List.map (fun {CAst.v=id} -> - let lev = Universes.new_univ_id () in + let lev = UnivGen.new_univ_id () in (id, lev)) l in let src = if poly then BoundUniv else UnqualifiedUniv in @@ -595,7 +595,7 @@ let input_constraints : constraint_decl -> Libobject.obj = let do_constraint poly l = let u_of_id x = let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - Universes.is_polymorphic level, level + UnivNames.is_polymorphic level, level in let in_section = Lib.sections_are_opened () in let () = diff --git a/interp/declare.mli b/interp/declare.mli index 084d746e68..4a9f542783 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -83,10 +83,10 @@ val recursive_message : bool (** true = fixpoint *) -> val exists_name : Id.t -> bool (** Global universe contexts, names and constraints *) -val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit +val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit val do_universe : polymorphic -> Misctypes.lident list -> unit -val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> +val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> unit diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index bc6a1ef3aa..74618a2905 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -254,7 +254,7 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc -> let dump_definition {CAst.loc;v=id} sec s = dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id) -let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty = +let dump_constraint { CAst.loc; v = n } sec ty = match n with | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty | Names.Anonymous -> () diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 43c100008c..bf83d2df40 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -24,7 +24,7 @@ val feedback_glob : unit -> unit val pause : unit -> unit val continue : unit -> unit -val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit +val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit val dump_definition : Misctypes.lident -> bool -> string -> unit @@ -38,9 +38,9 @@ val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit val dump_notation : (Constrexpr.notation * Notation.notation_location) Loc.located -> Notation_term.scope_name option -> bool -> unit -val dump_constraint : - Vernacexpr.typeclass_constraint -> bool -> string -> unit + +val dump_constraint : Misctypes.lname -> bool -> string -> unit val dump_string : string -> unit -val type_of_global_ref : Globnames.global_reference -> string +val type_of_global_ref : Names.GlobRef.t -> string diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml new file mode 100644 index 0000000000..80697461a6 --- /dev/null +++ b/interp/genredexpr.ml @@ -0,0 +1,66 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Reduction expressions *) + +(** The parsing produces initially a list of [red_atom] *) + +type 'a red_atom = + | FBeta + | FMatch + | FFix + | FCofix + | FZeta + | FConst of 'a list + | FDeltaBut of 'a list + +(** This list of atoms is immediately converted to a [glob_red_flag] *) + +type 'a glob_red_flag = { + rBeta : bool; + rMatch : bool; + rFix : bool; + rCofix : bool; + rZeta : bool; + rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*) + rConst : 'a list +} + +(** Generic kinds of reductions *) + +type ('a,'b,'c) red_expr_gen = + | Red of bool + | Hnf + | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option + | Cbv of 'b glob_red_flag + | Cbn of 'b glob_red_flag + | Lazy of 'b glob_red_flag + | Unfold of 'b Locus.with_occurrences list + | Fold of 'a list + | Pattern of 'a Locus.with_occurrences list + | ExtraRedExpr of string + | CbvVm of ('b,'c) Util.union Locus.with_occurrences option + | CbvNative of ('b,'c) Util.union Locus.with_occurrences option + +type ('a,'b,'c) may_eval = + | ConstrTerm of 'a + | ConstrEval of ('a,'b,'c) red_expr_gen * 'a + | ConstrContext of Misctypes.lident * 'a + | ConstrTypeOf of 'a + +open Libnames +open Constrexpr +open Misctypes + +type r_trm = constr_expr +type r_pat = constr_pattern_expr +type r_cst = reference or_by_notation + +type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen diff --git a/interp/impargs.ml b/interp/impargs.ml index 9ad62c0de3..8aa1e62504 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -139,7 +139,7 @@ let argument_less = function | Hyp _, Conclusion -> true | Conclusion, _ -> false -let update pos rig (na,st) = +let update pos rig st = let e = if rig then match st with @@ -163,7 +163,7 @@ let update pos rig (na,st) = | Some (DepFlex fpos as x) -> if argument_less (pos,fpos) then DepFlex pos else x | Some Manual -> assert false - in na, Some e + in Some e (* modified is_rigid_reference with a truncated env *) let is_flexible_reference env sigma bound depth f = @@ -214,6 +214,8 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in acc +(* compute the list of implicit arguments *) + let rec is_rigid_head sigma t = match kind sigma t with | Rel _ | Evar _ -> false | Ind _ | Const _ | Var _ | Sort _ -> true @@ -226,51 +228,69 @@ let rec is_rigid_head sigma t = match kind sigma t with | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _ | Prod _ | Meta _ | Cast _ -> assert false -(* calcule la liste des arguments implicites *) +let is_rigid env sigma t = + let open Context.Rel.Declaration in + let t = whd_all env sigma t in + match kind sigma t with + | Prod (na,a,b) -> + let (_,t) = splay_prod (push_rel (LocalAssum (na,a)) env) sigma b in + is_rigid_head sigma t + | _ -> true -let find_displayed_name_in all avoid na (env, b) = +let find_displayed_name_in sigma all avoid na (env, b) = let envnames_b = (env, b) in let flag = RenamingElsewhereFor envnames_b in - if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b - else compute_displayed_name_in Evd.empty flag avoid na b + if all then compute_and_force_displayed_name_in sigma flag avoid na b + else compute_displayed_name_in sigma flag avoid na b + +let compute_implicits_names_gen all env sigma t = + let open Context.Rel.Declaration in + let rec aux env avoid names t = + let t = whd_all env sigma t in + match kind sigma t with + | Prod (na,a,b) -> + let na',avoid' = find_displayed_name_in sigma all avoid na (names,b) in + aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b + | _ -> List.rev names + in aux env Id.Set.empty [] t + +let compute_implicits_names = compute_implicits_names_gen true -let compute_implicits_gen strict strongly_strict revpat contextual all env sigma (t : EConstr.t) = - let rigid = ref true in +let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t = let open Context.Rel.Declaration in - let rec aux env avoid n names (t : EConstr.t) = + let rec aux env n t = let t = whd_all env sigma t in match kind sigma t with - | Prod (na,a,b) -> - let na',avoid' = find_displayed_name_in all avoid na (names,b) in - add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1)) - (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b) - | _ -> - rigid := is_rigid_head sigma t; - let names = List.rev names in - let v = Array.map (fun na -> na,None) (Array.of_list names) in - if contextual then - add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v - else v + | Prod (na,a,b) -> + add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1)) + (aux (push_rel (LocalAssum (na,a)) env) (n+1) b) + | _ -> + let v = Array.make n None in + if contextual then + add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v + else v in match kind sigma (whd_all env sigma t) with - | Prod (na,a,b) -> - let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in - let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in - !rigid, Array.to_list v - | _ -> true, [] + | Prod (na,a,b) -> + let v = aux (push_rel (LocalAssum (na,a)) env) 1 b in + Array.to_list v + | _ -> [] -let compute_implicits_flags env sigma f all t = - compute_implicits_gen +let compute_implicits_explanation_flags env sigma f t = + compute_implicits_explanation_gen (f.strict || f.strongly_strict) f.strongly_strict - f.reversible_pattern f.contextual all env sigma t + f.reversible_pattern f.contextual env sigma t -let compute_auto_implicits env sigma flags enriching t = - if enriching then compute_implicits_flags env sigma flags true t - else compute_implicits_gen false false false true true env sigma t +let compute_implicits_flags env sigma f all t = + List.combine + (compute_implicits_names_gen all env sigma t) + (compute_implicits_explanation_flags env sigma f t) -let compute_implicits_names env sigma t = - let _, impls = compute_implicits_gen false false false false true env sigma t in - List.map fst impls +let compute_auto_implicits env sigma flags enriching t = + List.combine + (compute_implicits_names env sigma t) + (if enriching then compute_implicits_explanation_flags env sigma flags t + else compute_implicits_explanation_gen false false false true env sigma t) (* Extra information about implicit arguments *) @@ -329,13 +349,16 @@ let rec prepare_implicits f = function Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps -let set_implicit id imp insmax = - (id,(match imp with None -> Manual | Some imp -> imp),insmax) - -let rec assoc_by_pos k = function - (ExplByPos (k', x), b) :: tl when Int.equal k k' -> (x,b), tl - | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl - | [] -> raise Not_found +(* +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 @@ -352,70 +375,65 @@ let check_correct_manual_implicits autoimps l = (str "Cannot set implicit argument number " ++ int i ++ str ": it has no name.")) l -let set_manual_implicits env flags enriching autoimps l = - let try_forced k l = - try - let (id, (b, fi, fo)), l' = assoc_by_pos k l in - if fo then - let id = match id with Some id -> id | None -> Id.of_string ("arg_" ^ string_of_int k) in - l', Some (id,Manual,(b,fi)) - else l, None - with Not_found -> l, None - in +(* 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 = 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 l = function - | (Name id,imp)::imps -> - let l',imp,m = - try - let eq = explicitation_eq in - let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in - List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi)) - with Not_found -> - try - let (id, (b, fi, fo)), l' = assoc_by_pos k l in - l', (Some Manual), (Some (b,fi)) - with Not_found -> - let m = match enriching, imp with - | true, Some _ -> Some (flags.maximal, true) - | _ -> None - in - l, imp, m - in - let imps' = merge (k+1) l' imps in - let m = Option.map (fun (b,f) -> - (* match imp with Some Manual -> (b,f) *) - (* | _ -> *)set_maximality imps' b, f) m in - Option.map (set_implicit id imp) m :: imps' - | (Anonymous,imp)::imps -> - let l', forced = try_forced k l in - forced :: merge (k+1) l' imps - | [] when begin match l with [] -> true | _ -> false end -> [] - | [] -> - check_correct_manual_implicits autoimps l; - [] - in - merge 1 l autoimps - -let compute_semi_auto_implicits env sigma f manual t = - match manual with - | [] -> - if not f.auto then [DefaultImpArgs, []] - else let _,l = compute_implicits_flags env sigma f false t in - [DefaultImpArgs, prepare_implicits f l] - | _ -> - let _,autoimpls = compute_auto_implicits env sigma f f.auto t in - [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] + 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)) + | (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)) -> + let id = Id.of_string ("arg_" ^ string_of_int k) in + Some (id,Manual,(b,fi)) + | (Anonymous,_), Some (_, (_, _, false)) -> None + | (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) + +let compute_semi_auto_implicits env sigma f t = + if not f.auto then [DefaultImpArgs, []] + else let l = compute_implicits_flags env sigma f false t in + [DefaultImpArgs, prepare_implicits f l] (*s Constants. *) -let compute_constant_implicits flags manual cst = +let compute_constant_implicits flags cst = let env = Global.env () in let sigma = Evd.from_env env in let cb = Environ.lookup_constant cst env in let ty = of_constr cb.const_type in - let impls = compute_semi_auto_implicits env sigma flags manual ty in + let impls = compute_semi_auto_implicits env sigma flags ty in impls (*s Inductives and constructors. Their implicit arguments are stored @@ -423,7 +441,7 @@ let compute_constant_implicits flags manual cst = $i$ are the implicit arguments of the inductive and $v$ the array of implicit arguments of the constructors. *) -let compute_mib_implicits flags manual kn = +let compute_mib_implicits flags kn = let env = Global.env () in let sigma = Evd.from_env env in let mib = Environ.lookup_mind kn env in @@ -439,34 +457,34 @@ let compute_mib_implicits flags manual kn = let imps_one_inductive i mip = let ind = (kn,i) in let ar, _ = Global.type_of_global_in_context env (IndRef ind) in - ((IndRef ind,compute_semi_auto_implicits env sigma flags manual (of_constr ar)), + ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), Array.mapi (fun j c -> - (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags manual c)) + (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) (Array.map of_constr mip.mind_nf_lc)) in Array.mapi imps_one_inductive mib.mind_packets -let compute_all_mib_implicits flags manual kn = - let imps = compute_mib_implicits flags manual kn in +let compute_all_mib_implicits flags kn = + let imps = compute_mib_implicits flags kn in List.flatten (Array.map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) (*s Variables. *) -let compute_var_implicits flags manual id = +let compute_var_implicits flags id = let env = Global.env () in let sigma = Evd.from_env env in - compute_semi_auto_implicits env sigma flags manual (NamedDecl.get_type (lookup_named id env)) + compute_semi_auto_implicits env sigma flags (NamedDecl.get_type (lookup_named id env)) (* Implicits of a global reference. *) -let compute_global_implicits flags manual = function - | VarRef id -> compute_var_implicits flags manual id - | ConstRef kn -> compute_constant_implicits flags manual kn +let compute_global_implicits flags = function + | VarRef id -> compute_var_implicits flags id + | ConstRef kn -> compute_constant_implicits flags kn | IndRef (kn,i) -> - let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps + let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps | ConstructRef ((kn,i),j) -> - let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1) + let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1) (* Merge a manual explicitation with an implicit_status list *) @@ -487,7 +505,7 @@ type implicit_discharge_request = | ImplLocal | ImplConstant of Constant.t * implicits_flags | ImplMutualInductive of MutInd.t * implicits_flags - | ImplInteractive of global_reference * implicits_flags * + | ImplInteractive of GlobRef.t * implicits_flags * implicit_interactive_request let implicits_table = Summary.ref Refmap.empty ~name:"implicits" @@ -520,7 +538,7 @@ let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) let subst_implicits (subst,(req,l)) = - (ImplLocal,List.smartmap (subst_implicits_decl subst) l) + (ImplLocal,List.Smart.map (subst_implicits_decl subst) l) let impls_of_context ctx = let map (decl, impl) = match impl with @@ -573,34 +591,34 @@ let rebuild_implicits (req,l) = | ImplLocal -> assert false | ImplConstant (con,flags) -> let oldimpls = snd (List.hd l) in - let newimpls = compute_constant_implicits flags [] con in + let newimpls = compute_constant_implicits flags con in req, [ConstRef con, List.map2 merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> - let newimpls = compute_all_mib_implicits flags [] kn in + let newimpls = compute_all_mib_implicits flags kn in let rec aux olds news = - match olds, news with - | (_, oldimpls) :: old, (gr, newimpls) :: tl -> - (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl - | [], [] -> [] - | _, _ -> assert false + match olds, news with + | (_, oldimpls) :: old, (gr, newimpls) :: tl -> + (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl + | [], [] -> [] + | _, _ -> assert false in req, aux l newimpls | ImplInteractive (ref,flags,o) -> (if isVarRef ref && is_in_section ref then ImplLocal else req), match o with | ImplAuto -> - let oldimpls = snd (List.hd l) in - let newimpls = compute_global_implicits flags [] ref in - [ref,List.map2 merge_impls oldimpls newimpls] + let oldimpls = snd (List.hd l) in + let newimpls = compute_global_implicits flags ref in + [ref,List.map2 merge_impls oldimpls newimpls] | ImplManual userimplsize -> - let oldimpls = snd (List.hd l) in - if flags.auto then - let newimpls = List.hd (compute_global_implicits flags [] ref) in - let p = List.length (snd newimpls) - userimplsize in - let newimpls = on_snd (List.firstn p) newimpls in - [ref,List.map (fun o -> merge_impls o newimpls) oldimpls] - else - [ref,oldimpls] + let oldimpls = snd (List.hd l) in + if flags.auto then + let newimpls = List.hd (compute_global_implicits flags ref) in + let p = List.length (snd newimpls) - userimplsize in + let newimpls = on_snd (List.firstn p) newimpls in + [ref,List.map (fun o -> merge_impls o newimpls) oldimpls] + else + [ref,oldimpls] let classify_implicits (req,_ as obj) = match req with | ImplLocal -> Dispose @@ -608,7 +626,7 @@ let classify_implicits (req,_ as obj) = match req with type implicits_obj = implicit_discharge_request * - (global_reference * implicits_list list) list + (GlobRef.t * implicits_list list) list let inImplicits : implicits_obj -> obj = declare_object {(default_object "IMPLICITS") with @@ -622,7 +640,7 @@ let inImplicits : implicits_obj -> obj = let is_local local ref = local || isVarRef ref && is_in_section ref let declare_implicits_gen req flags ref = - let imps = compute_global_implicits flags [] ref in + let imps = compute_global_implicits flags ref in add_anonymous_leaf (inImplicits (req,[ref,imps])) let declare_implicits local ref = @@ -643,7 +661,7 @@ let declare_mib_implicits kn = let flags = !implicit_args in let imps = Array.map_to_list (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) - (compute_mib_implicits flags [] kn) in + (compute_mib_implicits flags kn) in add_anonymous_leaf (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) @@ -653,8 +671,8 @@ type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool) type manual_implicits = manual_explicitation 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 env !implicit_args enriching autoimpls l + let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in + set_manual_implicits !implicit_args enriching autoimpls l let check_inclusion l = (* Check strict inclusion *) @@ -679,26 +697,26 @@ let declare_manual_implicits local ref ?enriching l = let env = Global.env () in let sigma = Evd.from_env env in let t, _ = Global.type_of_global_in_context env ref in + let t = of_constr t in let enriching = Option.default flags.auto enriching in - let isrigid,autoimpls = compute_auto_implicits env sigma flags enriching (of_constr t) in + let autoimpls = compute_auto_implicits env sigma flags enriching t in let l' = match l with | [] -> assert false | [l] -> - [DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l] + [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] | _ -> - check_rigidity isrigid; - let l = List.map (fun imps -> (imps,List.length 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 env flags enriching autoimpls imps)) l in + check_rigidity (is_rigid env sigma t); + let l = List.map (fun imps -> (imps,List.length 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 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'])) + in add_anonymous_leaf (inImplicits (req,[ref,l'])) let maybe_declare_manual_implicits local ref ?enriching l = match l with diff --git a/interp/impargs.mli b/interp/impargs.mli index 1eeb8e41ae..ea5aa90f68 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -10,7 +10,6 @@ open Names open EConstr -open Globnames open Environ (** {6 Implicit Arguments } *) @@ -103,7 +102,7 @@ val declare_var_implicits : variable -> unit val declare_constant_implicits : Constant.t -> unit val declare_mib_implicits : MutInd.t -> unit -val declare_implicits : bool -> global_reference -> unit +val declare_implicits : bool -> GlobRef.t -> unit (** [declare_manual_implicits local ref enriching l] Manual declaration of which arguments are expected implicit. @@ -111,15 +110,15 @@ val declare_implicits : bool -> global_reference -> unit implicits depending on the current state. Unsets implicits if [l] is empty. *) -val declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> +val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> manual_implicits list -> unit (** If the list is empty, do nothing, otherwise declare the implicits. *) -val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> +val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> manual_implicits -> unit -val implicits_of_global : global_reference -> implicits_list list +val implicits_of_global : GlobRef.t -> implicits_list list val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list @@ -130,7 +129,7 @@ val make_implicits_list : implicit_status list -> implicits_list list val drop_first_implicits : int -> implicits_list -> implicits_list -val projection_implicits : env -> projection -> implicit_status list -> +val projection_implicits : env -> Projection.t -> implicit_status list -> implicit_status list val select_impargs_size : int -> implicits_list list -> implicit_status list diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index a1a3be70f1..b48db9ac54 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -17,12 +17,14 @@ open Glob_term open Constrexpr open Libnames open Typeclasses -open Typeclasses_errors open Pp open Libobject open Nameops open Context.Rel.Declaration +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) +let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) + module RelDecl = Context.Rel.Declaration (*i*) @@ -58,7 +60,7 @@ let in_generalizable : bool * Misctypes.lident list option -> obj = classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj) } -let declare_generalizable local gen = +let declare_generalizable ~local gen = Lib.add_anonymous_leaf (in_generalizable (local, gen)) let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table @@ -238,13 +240,19 @@ let implicit_application env ?(allow_partial=true) f ty = 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 - Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd + 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 CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid in c, avoid +let warn_ignoring_implicit_status = + CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits" + (fun na -> + strbrk "Ignoring implicit status of product binder " ++ + 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 -> @@ -260,20 +268,18 @@ let implicits_of_glob_constr ?(with_products=true) l = let abs na bk b = add_impl i na bk (aux (succ i) b) in - match DAst.get c with - | GProd (na, bk, t, b) -> - if with_products then abs na bk b - else - let () = match bk with - | Implicit -> - Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ - Name.print na ++ strbrk " and following binders") - | _ -> () - in [] - | GLambda (na, bk, t, b) -> abs na bk b - | GLetIn (na, b, t, c) -> aux i b - | 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) - | _ -> [] + match DAst.get c with + | GProd (na, bk, t, b) -> + if with_products then abs na bk 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 b + | 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) + | _ -> [] in aux 1 l diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index b9815f34d5..e64c5c5427 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -12,9 +12,8 @@ open Names open Glob_term open Constrexpr open Libnames -open Globnames -val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit +val declare_generalizable : local:bool -> Misctypes.lident list option -> unit val ids_of_list : Id.t list -> Id.Set.t val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t @@ -39,10 +38,14 @@ 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 -> global_reference option * Context.Rel.Declaration.t -> + Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> global_reference option * Context.Rel.Declaration.t -> + (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> 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 * Context.Rel.t (* found, expected *) +val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Context.Rel.t -> 'a diff --git a/interp/interp.mllib b/interp/interp.mllib index bb22cf468d..3668455aeb 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,14 +1,16 @@ +Constrexpr +Genredexpr +Redops Tactypes Stdarg Genintern +Notation_term Notation_ops Notation Syntax_def Smartlocate Constrexpr_ops -Ppextend Dumpglob -Topconstr Reserve Impargs Implicit_quantifiers diff --git a/interp/modintern.ml b/interp/modintern.ml index dc93d8dc4d..fefd2ab6f5 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -63,7 +63,7 @@ let transl_with_decl env = function | CWith_Module ({CAst.v=fqid},qid) -> WithMod (fqid,lookup_module qid), Univ.ContextSet.empty | CWith_Definition ({CAst.v=fqid},udecl,c) -> - let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in + let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in let c, ectx = interp_constr env sigma c in begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with | Entries.Polymorphic_const_entry ctx -> diff --git a/interp/notation.ml b/interp/notation.ml index 47d6481350..05fcd0e7f5 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -20,7 +20,6 @@ open Constrexpr open Notation_term open Glob_term open Glob_ops -open Ppextend open Context.Named.Declaration (*i*) @@ -49,7 +48,6 @@ type notation_location = (DirPath.t * DirPath.t) * string type notation_data = { not_interp : interpretation; not_location : notation_location; - not_onlyprinting : bool; } type scope = { @@ -57,9 +55,6 @@ type scope = { delimiters: delimiters option } -(* Uninterpreted notation map: notation -> level * DirPath.t *) -let notation_level_map = ref String.Map.empty - (* Scopes table: scope_name -> symbol_interpretation *) let scope_map = ref String.Map.empty @@ -76,44 +71,6 @@ let default_scope = "" (* empty name, not available from outside *) let init_scope_map () = scope_map := String.Map.add default_scope empty_scope !scope_map -(**********************************************************************) -(* Operations on scopes *) - -let parenRelation_eq t1 t2 = match t1, t2 with -| L, L | E, E | Any, Any -> true -| Prec l1, Prec l2 -> Int.equal l1 l2 -| _ -> false - -open Extend - -let production_level_eq l1 l2 = true (* (l1 = l2) *) - -let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with -| NextLevel, NextLevel -> true -| NumLevel n1, NumLevel n2 -> Int.equal n1 n2 -| (NextLevel | NumLevel _), _ -> false *) - -let constr_entry_key_eq eq v1 v2 = match v1, v2 with -| ETName, ETName -> true -| ETReference, ETReference -> true -| ETBigint, ETBigint -> true -| ETBinder b1, ETBinder b2 -> b1 == b2 -| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2 -| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2 -| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 -| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' -| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false - -let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) = - let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in - let prod_eq (l1,pp1) (l2,pp2) = - if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2 - else production_level_eq l1 l2 in - Int.equal l1 l2 && List.equal tolerability_eq t1 t2 - && List.equal (constr_entry_key_eq prod_eq) u1 u2 - -let level_eq = level_eq_gen false - let declare_scope scope = try let _ = String.Map.find scope !scope_map in () with Not_found -> @@ -259,7 +216,7 @@ type interp_rule = according to the key of the pattern (adapted from Chet Murthy by HH) *) type key = - | RefKey of global_reference + | RefKey of GlobRef.t | Oth let key_compare k1 k2 = match k1, k2 with @@ -428,16 +385,6 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function (* Can we switch to [scope]? Yes if it has defined delimiters *) find_with_delimiters ntn_scope -(* Uninterpreted notation levels *) - -let declare_notation_level ntn level = - if String.Map.mem ntn !notation_level_map then - anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level."); - notation_level_map := String.Map.add ntn level !notation_level_map - -let level_of_notation ntn = - String.Map.find ntn !notation_level_map - (* The mapping between notations and their interpretation *) let warn_notation_overridden = @@ -449,20 +396,21 @@ let warn_notation_overridden = let declare_notation_interpretation ntn scopt pat df ~onlyprint = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in - let () = - if String.Map.mem ntn sc.notations then - let which_scope = match scopt with - | None -> mt () - | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in - warn_notation_overridden (ntn,which_scope) - in - let notdata = { - not_interp = pat; - not_location = df; - not_onlyprinting = onlyprint; - } in - let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in - let () = scope_map := String.Map.add scope sc !scope_map in + if not onlyprint then begin + let () = + if String.Map.mem ntn sc.notations then + let which_scope = match scopt with + | None -> mt () + | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in + warn_notation_overridden (ntn,which_scope) + in + let notdata = { + not_interp = pat; + not_location = df; + } in + let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in + scope_map := String.Map.add scope sc !scope_map + end; begin match scopt with | None -> scope_stack := SingleNotation ntn :: !scope_stack | Some _ -> () @@ -487,7 +435,6 @@ let rec find_interpretation ntn find = function let find_notation ntn sc = let n = String.Map.find ntn (find_scope sc).notations in - let () = if n.not_onlyprinting then raise Not_found in (n.not_interp, n.not_location) let notation_of_prim_token = function @@ -631,7 +578,6 @@ let exists_notation_in_scope scopt ntn onlyprint r = try let sc = String.Map.find scope !scope_map in let n = String.Map.find ntn sc.notations in - onlyprint = n.not_onlyprinting && interpretation_eq n.not_interp r with Not_found -> false @@ -741,7 +687,7 @@ let subst_arguments_scope (subst,(req,r,n,scl,cls)) = match subst_scope_class subst cl with | Some cl' as ocl' when cl' != cl -> ocl' | _ -> ocl in - let cls' = List.smartmap subst_cl cls in + let cls' = List.Smart.map subst_cl cls in (ArgsScopeNoDischarge,r',n,scl,cls') let discharge_arguments_scope (_,(req,r,n,l,_)) = @@ -778,7 +724,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = (req,r,0,l1@l,cls1) type arguments_scope_obj = - arguments_scope_discharge_request * global_reference * + arguments_scope_discharge_request * GlobRef.t * (* Used to communicate information from discharge to rebuild *) (* set to 0 otherwise *) int * scope_name option list * scope_class option list @@ -1051,7 +997,7 @@ let locate_notation prglob ntn scope = | [] -> str "Unknown notation" | _ -> str "Notation" ++ fnl () ++ - prlist (fun (ntn,l) -> + prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in prlist (fun (sc,r,(_,df)) -> @@ -1060,8 +1006,7 @@ let locate_notation prglob ntn scope = (if String.equal sc default_scope then mt () else (spc () ++ str ": " ++ str sc)) ++ (if Option.equal String.equal (Some sc) scope - then spc () ++ str "(default interpretation)" else mt ()) - ++ fnl ())) + then spc () ++ str "(default interpretation)" else mt ()))) l) ntns let collect_notation_in_scope scope sc known = @@ -1114,63 +1059,24 @@ let pr_visibility prglob = function | None -> pr_scope_stack prglob !scope_stack (**********************************************************************) -(* Mapping notations to concrete syntax *) - -type unparsing_rule = unparsing list * precedence -type extra_unparsing_rules = (string * string) list -(* Concrete syntax for symbolic-extension table *) -let notation_rules = - ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t) - -let declare_notation_rule ntn ~extra unpl gram = - notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules - -let find_notation_printing_rule ntn = - try pi1 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".") -let find_notation_extra_printing_rules ntn = - try pi2 (String.Map.find ntn !notation_rules) - with Not_found -> [] -let find_notation_parsing_rules ntn = - try pi3 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".") - -let get_defined_notations () = - String.Set.elements @@ String.Map.domain !notation_rules - -let add_notation_extra_printing_rule ntn k v = - try - notation_rules := - let p, pp, gr = String.Map.find ntn !notation_rules in - String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules - with Not_found -> - user_err ~hdr:"add_notation_extra_printing_rule" - (str "No such Notation.") - -(**********************************************************************) (* Synchronisation with reset *) let freeze _ = - (!scope_map, !notation_level_map, !scope_stack, !arguments_scope, - !delimiters_map, !notations_key_table, !notation_rules, - !scope_class_map) + (!scope_map, !scope_stack, !arguments_scope, + !delimiters_map, !notations_key_table, !scope_class_map) -let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = +let unfreeze (scm,scs,asc,dlm,fkm,clsc) = scope_map := scm; - notation_level_map := nlm; scope_stack := scs; delimiters_map := dlm; arguments_scope := asc; notations_key_table := fkm; - notation_rules := pprules; scope_class_map := clsc let init () = init_scope_map (); - notation_level_map := String.Map.empty; delimiters_map := String.Map.empty; notations_key_table := KeyMap.empty; - notation_rules := String.Map.empty; scope_class_map := initial_scope_class_map let _ = diff --git a/interp/notation.mli b/interp/notation.mli index 6803a7e517..b177b7f1e0 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -11,11 +11,9 @@ open Bigint open Names open Libnames -open Globnames open Constrexpr open Glob_term open Notation_term -open Ppextend (** Notations *) @@ -33,8 +31,6 @@ val declare_scope : scope_name -> unit val current_scopes : unit -> scopes -val level_eq : level -> level -> bool - (** Check where a scope is opened or not in a scope list, or in * the current opened scopes *) val scope_is_open_in_scopes : scope_name -> scopes -> bool @@ -91,7 +87,7 @@ val declare_string_interpreter : scope_name -> required_module -> val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes -> glob_constr * (notation_location * scope_name option) (* This function returns a glob_const representing a pattern *) -val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> unit) -> prim_token -> +val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) -> prim_token -> local_scopes -> glob_constr * (notation_location * scope_name option) (** Return the primitive token associated to a [term]/[cases_pattern]; @@ -136,15 +132,10 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list val availability_of_notation : scope_name option * notation -> local_scopes -> (scope_name option * delimiters option) option -(** {6 Declare and test the level of a (possibly uninterpreted) notation } *) - -val declare_notation_level : notation -> level -> unit -val level_of_notation : notation -> level (** raise [Not_found] if no level *) - (** {6 Miscellaneous} *) -val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> bool) -> - notation -> delimiters option -> global_reference +val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> + notation -> delimiters option -> GlobRef.t (** Checks for already existing notations *) val exists_notation_in_scope : scope_name option -> notation -> @@ -152,9 +143,9 @@ val exists_notation_in_scope : scope_name option -> notation -> (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : - bool (** true=local *) -> global_reference -> scope_name option list -> unit + bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit -val find_arguments_scope : global_reference -> scope_name option list +val find_arguments_scope : GlobRef.t -> scope_name option list type scope_class @@ -165,7 +156,7 @@ val subst_scope_class : Mod_subst.substitution -> scope_class -> scope_class option val declare_scope_class : scope_name -> scope_class -> unit -val declare_ref_arguments_scope : Evd.evar_map -> global_reference -> unit +val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option @@ -201,21 +192,6 @@ val locate_notation : (glob_constr -> Pp.t) -> notation -> val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t -(** {6 Printing rules for notations} *) - -(** Declare and look for the printing rule for symbolic notations *) -type unparsing_rule = unparsing list * precedence -type extra_unparsing_rules = (string * string) list -val declare_notation_rule : - notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit -val find_notation_printing_rule : notation -> unparsing_rule -val find_notation_extra_printing_rules : notation -> extra_unparsing_rules -val find_notation_parsing_rules : notation -> notation_grammar -val add_notation_extra_printing_rule : notation -> string -> string -> unit - -(** Returns notations with defined parsing/printing rules *) -val get_defined_notations : unit -> notation list - (** Rem: printing rules for primitive token are canonical *) val with_notation_protection : ('a -> 'b) -> 'a -> 'b diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index a0d69ce796..f208b23fb6 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -13,6 +13,7 @@ open CErrors open Util open Names open Nameops +open Constr open Globnames open Decl_kinds open Misctypes @@ -28,7 +29,7 @@ open Notation_term let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with -| NRef gr1, NRef gr2 -> eq_gr gr1 gr2 +| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2 | NVar id1, NVar id2 -> ( match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with | Some n,Some m -> Int.equal n m @@ -165,15 +166,15 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = | NApp (a,args) -> GApp (f e a, List.map (f e) args) | NList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in - let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in + let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in let inner = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in - let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in + let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in DAst.get (subst_glob_vars outerl it) | NBinderList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in - let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in + let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in let inner = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in - let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in + let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in DAst.get (subst_glob_vars outerl it) | NLambda (na,ty,c) -> let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) @@ -210,7 +211,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let e',na = protect g e na in GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2) | NRec (fk,idl,dll,tl,bl) -> - let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) -> + let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) -> let e,na = protect g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = Array.fold_left_map (to_id (protect g)) e idl in @@ -509,7 +510,9 @@ let notation_constr_of_glob_constr nenv a = let notation_constr_of_constr avoiding t = let t = EConstr.of_constr t in - let t = Detyping.detype Detyping.Now false avoiding (Global.env()) Evd.empty t in + let env = Global.env () in + let evd = Evd.from_env env in + let t = Detyping.detype Detyping.Now false avoiding env evd t in let nenv = { ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; @@ -521,7 +524,7 @@ let rec subst_pat subst pat = | PatVar _ -> pat | PatCstr (((kn,i),j),cpl,n) -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_pat subst) cpl in + and cpl' = List.Smart.map (subst_pat subst) cpl in if kn' == kn && cpl' == cpl then pat else DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n) @@ -536,7 +539,7 @@ let rec subst_notation_constr subst bound raw = | NApp (r,rl) -> let r' = subst_notation_constr subst bound r - and rl' = List.smartmap (subst_notation_constr subst bound) rl in + and rl' = List.Smart.map (subst_notation_constr subst bound) rl in if r' == r && rl' == rl then raw else NApp(r',rl') @@ -566,14 +569,14 @@ let rec subst_notation_constr subst bound raw = | NLetIn (n,r1,t,r2) -> let r1' = subst_notation_constr subst bound r1 in - let t' = Option.smartmap (subst_notation_constr subst bound) t in + let t' = Option.Smart.map (subst_notation_constr subst bound) t in let r2' = subst_notation_constr subst bound r2 in if r1' == r1 && t == t' && r2' == r2 then raw else NLetIn (n,r1',t',r2') | NCases (sty,rtntypopt,rl,branches) -> - let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt - and rl' = List.smartmap + let rtntypopt' = Option.Smart.map (subst_notation_constr subst bound) rtntypopt + and rl' = List.Smart.map (fun (a,(n,signopt) as x) -> let a' = subst_notation_constr subst bound a in let signopt' = Option.map (fun ((indkn,i),nal as z) -> @@ -581,9 +584,9 @@ let rec subst_notation_constr subst bound raw = if indkn == indkn' then z else ((indkn',i),nal)) signopt in if a' == a && signopt' == signopt then x else (a',(n,signopt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun (cpl,r as branch) -> - let cpl' = List.smartmap (subst_pat subst) cpl + let cpl' = List.Smart.map (subst_pat subst) cpl and r' = subst_notation_constr subst bound r in if cpl' == cpl && r' == r then branch else (cpl',r')) @@ -594,14 +597,14 @@ let rec subst_notation_constr subst bound raw = NCases (sty,rtntypopt',rl',branches') | NLetTuple (nal,(na,po),b,c) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po + let po' = Option.Smart.map (subst_notation_constr subst bound) po and b' = subst_notation_constr subst bound b and c' = subst_notation_constr subst bound c in if po' == po && b' == b && c' == c then raw else NLetTuple (nal,(na,po'),b',c') | NIf (c,(na,po),b1,b2) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po + let po' = Option.Smart.map (subst_notation_constr subst bound) po and b1' = subst_notation_constr subst bound b1 and b2' = subst_notation_constr subst bound b2 and c' = subst_notation_constr subst bound c in @@ -610,12 +613,12 @@ let rec subst_notation_constr subst bound raw = | NRec (fk,idl,dll,tl,bl) -> let dll' = - Array.smartmap (List.smartmap (fun (na,oc,b as x) -> - let oc' = Option.smartmap (subst_notation_constr subst bound) oc in + Array.Smart.map (List.Smart.map (fun (na,oc,b as x) -> + let oc' = Option.Smart.map (subst_notation_constr subst bound) oc in let b' = subst_notation_constr subst bound b in if oc' == oc && b' == b then x else (na,oc',b'))) dll in - let tl' = Array.smartmap (subst_notation_constr subst bound) tl in - let bl' = Array.smartmap (subst_notation_constr subst bound) bl in + let tl' = Array.Smart.map (subst_notation_constr subst bound) tl in + let bl' = Array.Smart.map (subst_notation_constr subst bound) bl in if dll' == dll && tl' == tl && bl' == bl then raw else NRec (fk,idl,dll',tl',bl') @@ -628,7 +631,7 @@ let rec subst_notation_constr subst bound raw = if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) | _ -> knd in - let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in + let nsolve = Option.Smart.map (Genintern.generic_substitute subst) solve in if nsolve == solve && nknd == knd then raw else NHole (nknd, naming, nsolve) @@ -684,7 +687,7 @@ let is_onlybinding_meta id metas = let is_onlybinding_pattern_like_meta isvar id metas = try match Id.List.assoc id metas with | _,NtnTypeBinder (NtnBinderParsedAsConstr - (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true + (AsIdentOrPattern | AsStrictPattern)) -> true | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar) | _ -> false with Not_found -> false @@ -1123,7 +1126,7 @@ let rec match_ inner u alp metas sigma a1 a2 = (* Matching compositionally *) | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma - | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma + | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma | GApp (f1,l1), NApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in let f1,l1,f2,l2 = @@ -1335,10 +1338,10 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = match DAst.get a1, a2 with | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) - | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> + | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 -> let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in sigma,(0,l) - | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) + | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in diff --git a/interp/notation_term.ml b/interp/notation_term.ml new file mode 100644 index 0000000000..52a6354a0c --- /dev/null +++ b/interp/notation_term.ml @@ -0,0 +1,98 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Misctypes +open Glob_term + +(** [notation_constr] *) + +(** [notation_constr] is the subtype of [glob_constr] allowed in syntactic + extensions (i.e. notations). + No location since intended to be substituted at any place of a text. + Complex expressions such as fixpoints and cofixpoints are excluded, + as well as non global expressions such as existential variables. *) + +type notation_constr = + (** Part common to [glob_constr] and [cases_pattern] *) + | NRef of GlobRef.t + | NVar of Id.t + | NApp of notation_constr * notation_constr list + | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option + | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool + (** Part only in [glob_constr] *) + | NLambda of Name.t * notation_constr * notation_constr + | NProd of Name.t * notation_constr * notation_constr + | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool + | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr + | NCases of Constr.case_style * notation_constr option * + (notation_constr * (Name.t * (inductive * Name.t list) option)) list * + (cases_pattern list * notation_constr) list + | NLetTuple of Name.t list * (Name.t * notation_constr option) * + notation_constr * notation_constr + | NIf of notation_constr * (Name.t * notation_constr option) * + notation_constr * notation_constr + | NRec of fix_kind * Id.t array * + (Name.t * notation_constr option * notation_constr) list array * + notation_constr array * notation_constr array + | NSort of glob_sort + | NCast of notation_constr * notation_constr cast_type + | NProj of Projection.t * notation_constr + +(** Note concerning NList: first constr is iterator, second is terminator; + first id is where each argument of the list has to be substituted + in iterator and snd id is alternative name just for printing; + boolean is associativity *) + +(** Types concerning notations *) + +type scope_name = string + +type tmp_scope_name = scope_name + +type subscopes = tmp_scope_name option * scope_name list + +(** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, + x carries the sequence of objects bound to the list x..y *) + +type constr_as_binder_kind = + | AsIdent + | AsIdentOrPattern + | AsStrictPattern + +type notation_binder_source = + (* This accepts only pattern *) + (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *) + | NtnParsedAsPattern of bool + (* This accepts only ident *) + | NtnParsedAsIdent + (* This accepts ident, or pattern, or both *) + | NtnBinderParsedAsConstr of constr_as_binder_kind + +type notation_var_instance_type = + | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList + +(** Type of variables when interpreting a constr_expr as a notation_constr: + in a recursive pattern x..y, both x and y carry the individual type + of each element of the list x..y *) +type notation_var_internalization_type = + | NtnInternTypeAny | NtnInternTypeOnlyBinder + +(** This characterizes to what a notation is interpreted to *) +type interpretation = + (Id.t * (subscopes * notation_var_instance_type)) list * + notation_constr + +type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list + +type notation_interp_env = { + ninterp_var_type : notation_var_internalization_type Id.Map.t; + ninterp_rec_vars : Id.t Id.Map.t; +} diff --git a/interp/ppextend.ml b/interp/ppextend.ml deleted file mode 100644 index c75d9e12f7..0000000000 --- a/interp/ppextend.ml +++ /dev/null @@ -1,43 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open Notation_term - -(*s Pretty-print. *) - -type ppbox = - | PpHB of int - | PpHOVB of int - | PpHVB of int - | PpVB of int - -type ppcut = - | PpBrk of int * int - | PpFnl - -let ppcmd_of_box = function - | PpHB n -> h n - | PpHOVB n -> hov n - | PpHVB n -> hv n - | PpVB n -> v n - -let ppcmd_of_cut = function - | PpFnl -> fnl () - | PpBrk(n1,n2) -> brk(n1,n2) - -type unparsing = - | UnpMetaVar of int * parenRelation - | UnpBinderMetaVar of int * parenRelation - | UnpListMetaVar of int * parenRelation * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list - | UnpTerminal of string - | UnpBox of ppbox * unparsing Loc.located list - | UnpCut of ppcut diff --git a/interp/redops.ml b/interp/redops.ml new file mode 100644 index 0000000000..b9a74136e4 --- /dev/null +++ b/interp/redops.ml @@ -0,0 +1,64 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Genredexpr + +let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *) + +let make_red_flag l = + let rec add_flag red = function + | [] -> red + | FBeta :: lf -> add_flag { red with rBeta = true } lf + | FMatch :: lf -> add_flag { red with rMatch = true } lf + | FFix :: lf -> add_flag { red with rFix = true } lf + | FCofix :: lf -> add_flag { red with rCofix = true } lf + | FZeta :: lf -> add_flag { red with rZeta = true } lf + | FConst l :: lf -> + if red.rDelta then + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); + add_flag { red with rConst = union_consts red.rConst l } lf + | FDeltaBut l :: lf -> + if red.rConst <> [] && not red.rDelta then + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); + add_flag + { red with rConst = union_consts red.rConst l; rDelta = true } + lf + in + add_flag + {rBeta = false; rMatch = false; rFix = false; rCofix = false; + rZeta = false; rDelta = false; rConst = []} + l + + +let all_flags = + {rBeta = true; rMatch = true; rFix = true; rCofix = true; + rZeta = true; rDelta = true; rConst = []} + +(** Mapping [red_expr_gen] *) + +let map_flags f flags = + { flags with rConst = List.map f flags.rConst } + +let map_occs f (occ,e) = (occ,f e) + +let map_red_expr_gen f g h = function + | Fold l -> Fold (List.map f l) + | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l) + | Simpl (flags,occs_o) -> + Simpl (map_flags g flags, Option.map (map_occs (Util.map_union g h)) occs_o) + | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l) + | Cbv flags -> Cbv (map_flags g flags) + | Lazy flags -> Lazy (map_flags g flags) + | CbvVm occs_o -> CbvVm (Option.map (map_occs (Util.map_union g h)) occs_o) + | CbvNative occs_o -> CbvNative (Option.map (map_occs (Util.map_union g h)) occs_o) + | Cbn flags -> Cbn (map_flags g flags) + | ExtraRedExpr _ | Red _ | Hnf as x -> x diff --git a/interp/ppextend.mli b/interp/redops.mli index c81058e725..7254f29b25 100644 --- a/interp/ppextend.mli +++ b/interp/redops.mli @@ -8,29 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Notation_term +open Genredexpr -(** {6 Pretty-print. } *) +val make_red_flag : 'a red_atom list -> 'a glob_red_flag -type ppbox = - | PpHB of int - | PpHOVB of int - | PpHVB of int - | PpVB of int +val all_flags : 'a glob_red_flag -type ppcut = - | PpBrk of int * int - | PpFnl +(** Mapping [red_expr_gen] *) -val ppcmd_of_box : ppbox -> Pp.t -> Pp.t - -val ppcmd_of_cut : ppcut -> Pp.t - -type unparsing = - | UnpMetaVar of int * parenRelation - | UnpBinderMetaVar of int * parenRelation - | UnpListMetaVar of int * parenRelation * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list - | UnpTerminal of string - | UnpBox of ppbox * unparsing Loc.located list - | UnpCut of ppcut +val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) -> + ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen diff --git a/interp/reserve.ml b/interp/reserve.ml index 36005121b1..071248f01f 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -22,7 +22,7 @@ open Notation_ops open Globnames type key = - | RefKey of global_reference + | RefKey of GlobRef.t | Oth (** TODO: share code from Notation *) @@ -112,7 +112,9 @@ let revert_reserved_type t = let t = EConstr.Unsafe.to_constr t in let reserved = KeyMap.find (constr_key t) !reserve_revtable in let t = EConstr.of_constr t in - let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in + let env = Global.env () in + let evd = Evd.from_env env in + let t = Detyping.detype Detyping.Now false Id.Set.empty env evd t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) let filter _ pat = diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 7ff7e899e2..45037b8b36 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -18,22 +18,22 @@ open Misctypes if not bound in the global env; raise a [UserError] if bound to a syntactic def that does not denote a reference *) -val locate_global_with_alias : ?head:bool -> qualid CAst.t -> global_reference +val locate_global_with_alias : ?head:bool -> qualid CAst.t -> GlobRef.t (** Extract a global_reference from a reference that can be an "alias" *) -val global_of_extended_global : extended_global_reference -> global_reference +val global_of_extended_global : extended_global_reference -> GlobRef.t (** Locate a reference taking into account possible "alias" notations. May raise [Nametab.GlobalizationError _] for an unknown reference, or a [UserError] if bound to a syntactic def that does not denote a reference. *) -val global_with_alias : ?head:bool -> reference -> global_reference +val global_with_alias : ?head:bool -> reference -> GlobRef.t (** The same for inductive types *) val global_inductive_with_alias : reference -> inductive (** Locate a reference taking into account notations and "aliases" *) -val smart_global : ?head:bool -> reference or_by_notation -> global_reference +val smart_global : ?head:bool -> reference or_by_notation -> GlobRef.t (** The same for inductive types *) val smart_global_inductive : reference or_by_notation -> inductive diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 53d1a522d3..dc9c370a1b 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -14,7 +14,6 @@ open Loc open Names open EConstr open Libnames -open Globnames open Genredexpr open Pattern open Constrexpr @@ -42,7 +41,7 @@ val wit_ident : Id.t uniform_genarg_type val wit_var : (lident, lident, Id.t) genarg_type -val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type +val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_quant_hyp : quantified_hypothesis uniform_genarg_type @@ -81,8 +80,8 @@ val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr, val wit_integer : int uniform_genarg_type val wit_preident : string uniform_genarg_type -val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type -val wit_global : (reference, global_reference located or_var, global_reference) genarg_type +val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 47faa5885c..a4f20fd739 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -96,13 +96,13 @@ let warn_compatibility_notation = CWarnings.(create ~name:"compatibility-notation" ~category:"deprecated" ~default:Enabled pr_compat_warning) -let verbose_compat kn def = function +let verbose_compat ?loc kn def = function | Some v when Flags.version_strictly_greater v -> - warn_compatibility_notation (kn, def, v) + warn_compatibility_notation ?loc (kn, def, v) | _ -> () -let search_syntactic_definition kn = +let search_syntactic_definition ?loc kn = let pat,v = KNmap.find kn !syntax_table in let def = out_pat pat in - verbose_compat kn def v; + verbose_compat ?loc kn def v; def diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 1933b8a9ae..c5b6655ff8 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -18,4 +18,4 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr val declare_syntactic_definition : bool -> Id.t -> Flags.compat_version option -> syndef_interpretation -> unit -val search_syntactic_definition : KerName.t -> syndef_interpretation +val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation diff --git a/interp/topconstr.ml b/interp/topconstr.ml deleted file mode 100644 index 7d2d75d9cb..0000000000 --- a/interp/topconstr.ml +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Constrexpr_ops - -let asymmetric_patterns = asymmetric_patterns -let error_invalid_pattern_notation = error_invalid_pattern_notation -let split_at_annot = split_at_annot -let ntn_loc = ntn_loc -let patntn_loc = patntn_loc -let map_constr_expr_with_binders = map_constr_expr_with_binders -let fold_constr_expr_with_binders = fold_constr_expr_with_binders -let ids_of_cases_indtype = ids_of_cases_indtype -let occur_var_constr_expr = occur_var_constr_expr -let free_vars_of_constr_expr = free_vars_of_constr_expr -let replace_vars_constr_expr = replace_vars_constr_expr diff --git a/interp/topconstr.mli b/interp/topconstr.mli deleted file mode 100644 index c86502015a..0000000000 --- a/interp/topconstr.mli +++ /dev/null @@ -1,53 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constrexpr - -(** Topconstr: This whole module is deprecated in favor of Constrexpr_ops *) -val asymmetric_patterns : bool ref -[@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"] - -(** Utilities on constr_expr *) -val split_at_annot : local_binder_expr list -> Misctypes.lident option -> local_binder_expr list * local_binder_expr list -[@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"] - -val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list -[@@ocaml.deprecated "use Constrexpr_ops.ntn_loc"] -val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list -[@@ocaml.deprecated "use Constrexpr_ops.patntn_loc"] - -(** For cases pattern parsing errors *) -val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a -[@@ocaml.deprecated "use Constrexpr_ops.error_invalid_pattern_notation"] - -(*************************************************************************) -val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr -[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] - -val free_vars_of_constr_expr : constr_expr -> Id.Set.t -[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] - -val occur_var_constr_expr : Id.t -> constr_expr -> bool -[@@ocaml.deprecated "use Constrexpr_ops.occur_var_constr_expr"] - -(** Specific function for interning "in indtype" syntax of "match" *) -val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t -[@@ocaml.deprecated "use Constrexpr_ops.ids_of_cases_indtype"] - -(** Used in typeclasses *) -val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> - ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b -[@@ocaml.deprecated "use Constrexpr_ops.fold_constr_expr_with_binders"] - -val map_constr_expr_with_binders : - (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> - 'a -> constr_expr -> constr_expr -[@@ocaml.deprecated "use Constrexpr_ops.map_constr_expr_with_binders"] |