diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
| commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
| tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /interp | |
| parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) | |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'interp')
40 files changed, 2033 insertions, 1093 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml new file mode 100644 index 00000000..77d612cf --- /dev/null +++ b/interp/constrexpr.ml @@ -0,0 +1,162 @@ +(************************************************************************) +(* * 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 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_entry = InConstrEntry | InCustomEntry of string +type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int +type notation_key = string +type notation = notation_entry_level * notation_key + +type 'a or_by_notation_r = + | AN of 'a + | ByNotation of (string * string option) + +type 'a or_by_notation = 'a or_by_notation_r CAst.t + +(* NB: the last string in [ByNotation] is actually a [Notation.delimiters], + but this formulation avoids a useless dependency. *) + +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 qualid + * cases_pattern_expr list option * cases_pattern_expr list + (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) + | CPatAtom of qualid 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 (qualid * 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 qualid * 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 * qualid * instance_expr option) * constr_expr list + | CApp of (proj_flag * constr_expr) * + (constr_expr * explicitation CAst.t option) list + | CRecord of (qualid * 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 * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option + | CPatVar of Pattern.patvar + | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list + | CSort of Glob_term.glob_sort + | CCast of constr_expr * constr_expr Glob_term.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 +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 + | 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 004c9356..23d0536d 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -10,12 +10,13 @@ open Pp open Util -open CAst open Names open Nameops open Libnames +open Namegen +open Glob_term open Constrexpr -open Misctypes +open Notation open Decl_kinds (***********************) @@ -72,22 +73,22 @@ let rec cases_pattern_expr_eq p1 p2 = | CPatAlias(a1,i1), CPatAlias(a2,i2) -> eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> - eq_reference c1 c2 && + qualid_eq c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && List.equal cases_pattern_expr_eq b1 b2 | CPatAtom(r1), CPatAtom(r2) -> - Option.equal eq_reference r1 r2 + Option.equal qualid_eq r1 r2 | CPatOr a1, CPatOr a2 -> List.equal cases_pattern_expr_eq a1 a2 | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) -> - String.equal n1 n2 && + notation_eq n1 n2 && cases_pattern_notation_substitution_eq s1 s2 && List.equal cases_pattern_expr_eq l1 l2 | CPatPrim i1, CPatPrim i2 -> prim_token_eq i1 i2 | CPatRecord l1, CPatRecord l2 -> let equal (r1, e1) (r2, e2) = - eq_reference r1 r2 && cases_pattern_expr_eq e1 e2 + qualid_eq r1 r2 && cases_pattern_expr_eq e1 e2 in List.equal equal l1 l2 | CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) -> @@ -107,7 +108,7 @@ let eq_universes u1 u2 = let rec constr_expr_eq e1 e2 = if CAst.(e1.v == e2.v) then true else match CAst.(e1.v, e2.v) with - | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2 + | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2 | CFix(id1,fl1), CFix(id2,fl2) -> eq_ast Id.equal id1 id2 && List.equal fix_expr_eq fl1 fl2 @@ -127,7 +128,7 @@ let rec constr_expr_eq e1 e2 = constr_expr_eq b1 b2 | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) -> Option.equal Int.equal proj1 proj2 && - eq_reference r1 r2 && + qualid_eq r1 r2 && List.equal constr_expr_eq al1 al2 | CApp((proj1,e1),al1), CApp((proj2,e2),al2) -> Option.equal Int.equal proj1 proj2 && @@ -135,7 +136,7 @@ let rec constr_expr_eq e1 e2 = List.equal args_eq al1 al2 | CRecord l1, CRecord l2 -> let field_eq (r1, e1) (r2, e2) = - eq_reference r1 r2 && constr_expr_eq e1 e2 + qualid_eq r1 r2 && constr_expr_eq e1 e2 in List.equal field_eq l1 l2 | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> @@ -161,11 +162,11 @@ let rec constr_expr_eq e1 e2 = | CEvar (id1, c1), CEvar (id2, c2) -> Id.equal id1 id2 && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> - Miscops.glob_sort_eq s1 s2 + Glob_ops.glob_sort_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> constr_expr_eq t1 t2 && cast_expr_eq c1 c2 | CNotation(n1, s1), CNotation(n2, s2) -> - String.equal n1 n2 && + notation_eq n1 n2 && constr_notation_substitution_eq s1 s2 | CPrim i1, CPrim i2 -> prim_token_eq i1 i2 @@ -179,7 +180,7 @@ let rec constr_expr_eq e1 e2 = | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _ | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _ | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _ - | CGeneralization _ | CDelimiters _), _ -> false + | CGeneralization _ | CDelimiters _ ), _ -> false and args_eq (a1,e1) (a2,e2) = Option.equal (eq_ast explicitation_eq) e1 e2 && @@ -277,7 +278,9 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with List.fold_left (cases_pattern_fold_names f) (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat - | CPatAtom (Some {v=Ident id}) when not (is_constructor id) -> f id a + | CPatAtom (Some qid) + when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) -> + f (qualid_basename qid) a | CPatPrim _ | CPatAtom _ -> a | CPatCast ({CAst.loc},_) -> CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names" @@ -358,7 +361,9 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function let free_vars_of_constr_expr c = let rec aux bdvars l = function - | { CAst.v = CRef ({v=Ident id},_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + let id = qualid_basename qid in + if Id.List.mem id bdvars then l else Id.Set.add id l | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c in aux [] Id.Set.empty c @@ -391,7 +396,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b) | CLetIn (na,a,t,b) -> CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b) - | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) + | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c) | CNotation (n,(l,ll,bl,bll)) -> (* This is an approximation because we don't know what binds what *) CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl, @@ -433,11 +438,13 @@ let map_constr_expr_with_binders g f e = CAst.map (function ) (* Used in constrintern *) -let rec replace_vars_constr_expr l = function - | { CAst.loc; v = CRef ({v=Ident id},us) } as x -> - (try CAst.make ?loc @@ CRef (make ?loc @@ Ident (Id.Map.find id l),us) with Not_found -> x) - | c -> map_constr_expr_with_binders Id.Map.remove - replace_vars_constr_expr l c +let rec replace_vars_constr_expr l r = + match r with + | { CAst.loc; v = CRef (qid,us) } as x when qualid_is_ident qid -> + let id = qualid_basename qid in + (try CAst.make ?loc @@ CRef (qualid_of_ident ?loc (Id.Map.find id l),us) + with Not_found -> x) + | cn -> map_constr_expr_with_binders Id.Map.remove replace_vars_constr_expr l cn (* Returns the ranges of locs of the notation that are not occupied by args *) (* and which are then occupied by proper symbols of the notation (or spaces) *) @@ -506,7 +513,7 @@ let split_at_annot bl na = (** Pseudo-constructors *) -let mkIdentC id = CAst.make @@ CRef (make @@ Ident id,None) +let mkIdentC id = CAst.make @@ CRef (qualid_of_ident id,None) let mkRefC r = CAst.make @@ CRef (r,None) let mkCastC (a,k) = CAst.make @@ CCast (a,k) let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b) @@ -525,21 +532,23 @@ let mkCProdN ?loc bll c = let mkCLambdaN ?loc bll c = CAst.make ?loc @@ CLambdaN (bll,c) -let coerce_reference_to_id = CAst.with_loc_val (fun ?loc -> function - | Ident id -> id - | Qualid _ -> - CErrors.user_err ?loc ~hdr:"coerce_reference_to_id" - (str "This expression should be a simple identifier.")) +let coerce_reference_to_id qid = + if qualid_is_ident qid then qualid_basename qid + else + CErrors.user_err ?loc:qid.CAst.loc ~hdr:"coerce_reference_to_id" + (str "This expression should be a simple identifier.") let coerce_to_id = function - | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc id + | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid -> + CAst.make ?loc @@ qualid_basename qid | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_id" (str "This expression should be a simple identifier.") let coerce_to_name = function - | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id - | { CAst.loc; v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous + | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid -> + CAst.make ?loc @@ Name (qualid_basename qid) + | { CAst.loc; v = CHole (None,IntroAnonymous,None) } -> CAst.make ?loc Anonymous | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") @@ -563,9 +572,10 @@ let mkAppPattern ?loc p lp = let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function | CRef (r,None) -> CPatAtom (Some r) - | CHole (None,Misctypes.IntroAnonymous,None) -> + | CHole (None,IntroAnonymous,None) -> CPatAtom None - | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' -> + | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (qid,None) }) + when qualid_is_ident qid && Id.equal id (qualid_basename qid) -> CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id)) | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args -> (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v @@ -595,7 +605,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 d038bd71..61e8aa1b 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -10,7 +10,6 @@ open Names open Libnames -open Misctypes open Constrexpr (** Constrexpr_ops: utilities on [constr_expr] *) @@ -42,9 +41,9 @@ val local_binders_loc : local_binder_expr list -> Loc.t option (** {6 Constructors}*) val mkIdentC : Id.t -> constr_expr -val mkRefC : reference -> constr_expr +val mkRefC : qualid -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr -val mkCastC : constr_expr * constr_expr cast_type -> constr_expr +val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr @@ -60,17 +59,9 @@ 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 +val coerce_reference_to_id : qualid -> Id.t (** FIXME: nothing to do here *) val coerce_to_id : constr_expr -> lident @@ -116,11 +107,18 @@ val occur_var_constr_expr : Id.t -> constr_expr -> bool val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list -val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list -val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list +val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> notation -> (int * int) list +val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -> (int * int) list (** For cases pattern parsing errors *) 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 af44921e..754fb3b9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -14,10 +14,10 @@ open CErrors open Util open Names open Nameops -open Constr open Termops open Libnames open Globnames +open Namegen open Impargs open CAst open Constrexpr @@ -29,7 +29,6 @@ open Pattern open Nametab open Notation open Detyping -open Misctypes open Decl_kinds module NamedDecl = Context.Named.Declaration @@ -102,8 +101,8 @@ let _show_inactive_notations () = IRuleSet.iter (function | NotationRule (scopt, ntn) -> - Feedback.msg_notice (str ntn ++ show_scope scopt) - | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn))) + Feedback.msg_notice (pr_notation ntn ++ show_scope scopt) + | SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)))) !inactive_notations_table let deactivate_notation nr = @@ -114,14 +113,14 @@ let deactivate_notation nr = | NotationRule (scopt, ntn) -> match availability_of_notation (scopt, ntn) (scopt, []) with | None -> user_err ~hdr:"Notation" - (str ntn ++ spc () ++ str "does not exist" + (pr_notation ntn ++ spc () ++ str "does not exist" ++ (match scopt with | None -> spc () ++ str "in the empty scope." | Some _ -> show_scope scopt ++ str ".")) | Some _ -> if IRuleSet.mem nr !inactive_notations_table then Feedback.msg_warning - (str "Notation" ++ spc () ++ str ntn ++ spc () + (str "Notation" ++ spc () ++ pr_notation ntn ++ spc () ++ str "is already inactive" ++ show_scope scopt ++ str ".") else inactive_notations_table := IRuleSet.add nr !inactive_notations_table @@ -132,12 +131,13 @@ let reactivate_notation nr = with Not_found -> match nr with | NotationRule (scopt, ntn) -> - Feedback.msg_warning (str "Notation" ++ spc () ++ str ntn ++ spc () + Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc () ++ str "is already active" ++ show_scope scopt ++ str ".") | SynDefRule kn -> + let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in Feedback.msg_warning - (str "Notation" ++ spc () ++ str (Names.KerName.to_string kn) + (str "Notation" ++ spc () ++ str s ++ spc () ++ str "is already active.") @@ -261,6 +261,14 @@ let insert_pat_alias ?loc p = function | Anonymous -> p | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na)) +let rec insert_coercion ?loc l c = match l with + | [] -> c + | ntn::l -> CAst.make ?loc @@ CNotation (ntn,([insert_coercion ?loc l c],[],[],[])) + +let rec insert_pat_coercion ?loc l c = match l with + | [] -> c + | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[]) + (**********************************************************************) (* conversion of references *) @@ -271,7 +279,7 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - make @@ Qualid (shortest_qualid_of_global vars r) + shortest_qualid_of_global ?loc vars r let my_extern_reference = ref default_extern_reference @@ -326,16 +334,16 @@ let is_zero s = in aux 0 let make_notation_gen loc ntn mknot mkprim destprim l bl = - match ntn,List.map destprim l with + match snd ntn,List.map destprim l with (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *) | "- _", [Some (Numeral (p,true))] when not (is_zero p) -> assert (bl=[]); - mknot (loc,ntn,([mknot (loc,"( _ )",l,[])]),[]) + mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[]) | _ -> match decompose_notation_key ntn, l with - | [Terminal "-"; Terminal x], [] when is_number x -> + | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] when is_number x -> mkprim (loc, Numeral (x,false)) - | [Terminal x], [] when is_number x -> + | (InConstrEntrySomeLevel,[Terminal x]), [] when is_number x -> mkprim (loc, Numeral (x,true)) | _ -> mknot (loc,ntn,l,bl) @@ -368,31 +376,39 @@ let pattern_printable_in_both_syntax (ind,_ as c) = (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args) ) impl_st -let lift f c = - let loc = c.CAst.loc in - CAst.make ?loc (f ?loc (DAst.get c)) - (* Better to use extern_glob_constr composed with injection/retraction ?? *) -let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = +let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; let (na,sc,p) = uninterp_prim_token_cases_pattern pat in + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> match availability_of_prim_token p sc scopes with | None -> raise No_match | Some key -> let loc = cases_pattern_loc pat in - insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na + insert_pat_coercion ?loc coercion + (insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na) with No_match -> try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_pattern scopes vars pat + extern_notation_pattern allscopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> - lift (fun ?loc -> function - | PatVar (Name id) -> CPatAtom (Some (make ?loc @@ Ident id)) - | PatVar (Anonymous) -> CPatAtom None + let loc = pat.CAst.loc in + match DAst.get pat with + | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) + | pat -> + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> + let allscopes = (InConstrEntrySomeLevel,scopes) in + let pat = match pat with + | PatVar (Name id) -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) + | PatVar (Anonymous) -> CAst.make ?loc (CPatAtom None) | PatCstr(cstrsp,args,na) -> - let args = List.map (extern_cases_pattern_in_scope scopes vars) args in + let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in let p = try if !Flags.raw_print then raise Exit; @@ -425,26 +441,32 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with | Some true_args -> CPatCstr (c, None, true_args) | None -> CPatCstr (c, Some full_args, []) - in (insert_pat_alias ?loc (CAst.make ?loc p) na).v - ) pat + in + insert_pat_alias ?loc (CAst.make ?loc p) na + in + insert_pat_coercion coercion pat + and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) - (tmp_scope, scopes as allscopes) vars = + (custom, (tmp_scope, scopes) as allscopes) vars = function | NotationRule (sc,ntn) -> begin - match availability_of_notation (sc,ntn) allscopes with + match availability_of_entry_coercion custom (fst ntn) with + | None -> raise No_match + | Some coercion -> + match availability_of_notation (sc,ntn) (tmp_scope,scopes) with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> let scopes' = Option.List.cons scopt scopes in let l = - List.map (fun (c,(scopt,scl)) -> - extern_cases_pattern_in_scope (scopt,scl@scopes') vars c) + List.map (fun (c,(subentry,(scopt,scl))) -> + extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars c) subst in let ll = - List.map (fun (c,(scopt,scl)) -> - let subscope = (scopt,scl@scopes') in + List.map (fun (c,(subentry,(scopt,scl))) -> + let subscope = (subentry,(scopt,scl@scopes')) in List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in @@ -454,14 +476,18 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) |Some true_args -> true_args |None -> raise No_match in - insert_pat_delimiters ?loc - (make_pat_notation ?loc ntn (l,ll) l2') key + insert_pat_coercion coercion + (insert_pat_delimiters ?loc + (make_pat_notation ?loc ntn (l,ll) l2') key) end | SynDefRule kn -> - let qid = make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn) in + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> + let qid = shortest_qualid_of_syndef ?loc vars kn in let l1 = - List.rev_map (fun (c,(scopt,scl)) -> - extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) + List.rev_map (fun (c,(subentry,(scopt,scl))) -> + extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) subst in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in let l2' = if !asymmetric_patterns then l2 @@ -471,8 +497,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) |None -> raise No_match in assert (List.is_empty substlist); - mkPat ?loc qid (List.rev_append l1 l2') -and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function + insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2')) +and extern_notation_pattern allscopes vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try @@ -485,7 +511,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None - | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (make ?loc @@ Ident id)) + | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id)) with No_match -> extern_notation_pattern allscopes vars t rules @@ -499,35 +525,27 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function with No_match -> extern_notation_ind_pattern allscopes vars ind args rules -let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = +let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and not explicit application. *) if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then let c = extern_reference vars (IndRef ind) in - let args = List.map (extern_cases_pattern_in_scope scopes vars) args in + let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), []) else try if !Flags.raw_print || !print_no_symbol then raise No_match; - let (sc,p) = uninterp_prim_token_ind_pattern ind args in - match availability_of_prim_token p sc scopes with - | None -> raise No_match - | Some key -> - insert_pat_delimiters (CAst.make @@ CPatPrim p) key - with No_match -> - try - if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_ind_pattern scopes vars ind args + extern_notation_ind_pattern allscopes vars ind args (uninterp_ind_pattern_notations ind) with No_match -> let c = extern_reference vars (IndRef ind) in - let args = List.map (extern_cases_pattern_in_scope scopes vars) args in + let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in match drop_implicits_in_patt (IndRef ind) 0 args with |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args) |None -> CAst.make @@ CPatCstr (c, Some args, []) let extern_cases_pattern vars p = - extern_cases_pattern_in_scope (None,[]) vars p + extern_cases_pattern_in_scope (InConstrEntrySomeLevel,(None,[])) vars p (**********************************************************************) (* Externalising applications *) @@ -641,12 +659,12 @@ let extern_app inctx impl (cf,f) us args = else explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args -let rec fill_arg_scopes args subscopes scopes = match args, subscopes with +let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) = match args, subscopes with | [], _ -> [] | a :: args, scopt :: subscopes -> - (a, (scopt, scopes)) :: fill_arg_scopes args subscopes scopes + (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all | a :: args, [] -> - (a, (None, scopes)) :: fill_arg_scopes args [] scopes + (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all let extern_args extern env args = let map (arg, argscopes) = lazy (extern argscopes env arg) in @@ -698,12 +716,15 @@ let rec flatten_application c = match DAst.get c with (* mapping glob_constr to numerals (in presence of coercions, choose the *) (* one with no delimiter if possible) *) -let extern_possible_prim_token scopes r = +let extern_possible_prim_token (custom,scopes) r = try let (sc,n) = uninterp_prim_token r in + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> match availability_of_prim_token n sc scopes with | None -> None - | Some key -> Some (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) + | Some key -> Some (insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)) with No_match -> None @@ -721,7 +742,7 @@ let extended_glob_local_binder_of_decl loc = function | (p,bk,None,t) -> GLocalAssum (p,bk,t) | (p,bk,Some x, t) -> match DAst.get t with - | GHole (_, Misctypes.IntroAnonymous, None) -> GLocalDef (p,bk,x,None) + | GHole (_, IntroAnonymous, None) -> GLocalDef (p,bk,x,None) | _ -> GLocalDef (p,bk,x,Some t) let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u) @@ -738,7 +759,13 @@ let extern_glob_sort = function let extern_universes = function | Some _ as l when !print_universes -> l | _ -> None - + +let extern_ref vars ref us = + extern_global (select_stronger_impargs (implicits_of_global ref)) + (extern_reference vars ref) (extern_universes us) + +let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) + let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try @@ -749,20 +776,35 @@ let rec extern inctx scopes vars r = let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation scopes vars r'' (uninterp_notations r'') - with No_match -> lift (fun ?loc -> function - | GRef (ref,us) -> - extern_global (select_stronger_impargs (implicits_of_global ref)) - (extern_reference vars ref) (extern_universes us) + with No_match -> + let loc = r'.CAst.loc in + match DAst.get r' with + | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) + + | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) + + | c -> - | GVar id -> CRef (make ?loc @@ Ident id,None) + match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> - | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None) + let scopes = (InConstrEntrySomeLevel, snd scopes) in + let c = match c with + + (* The remaining cases are only for the constr entry *) + + | GRef (ref,us) -> extern_ref vars ref us + + | GVar id -> extern_var ?loc id + + | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None) | GEvar (n,l) -> extern_evar n (List.map (on_snd (extern false scopes vars)) l) | GPatVar kind -> - if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else + if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else (match kind with | Evar_kinds.SecondOrderPatVar n -> CPatVar n | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) @@ -771,7 +813,7 @@ let rec extern inctx scopes vars r = (match DAst.get f with | GRef (ref,us) -> let subscopes = find_arguments_scope ref in - let args = fill_arg_scopes args subscopes (snd scopes) in + let args = fill_arg_scopes args subscopes scopes in begin try if !Flags.raw_print then raise Exit; @@ -918,18 +960,19 @@ let rec extern inctx scopes vars r = | GCast (c, c') -> CCast (sub_extern true scopes vars c, - Miscops.map_cast_type (extern_typ scopes vars) c') - ) r' + map_cast_type (extern_typ scopes vars) c') + + in insert_coercion coercion (CAst.make ?loc c) -and extern_typ (_,scopes) = - extern true (Notation.current_type_scope_name (),scopes) +and extern_typ (subentry,(_,scopes)) = + extern true (subentry,(Notation.current_type_scope_name (),scopes)) -and sub_extern inctx (_,scopes) = extern inctx (None,scopes) +and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(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)}] -> @@ -957,7 +1000,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)}] -> @@ -1017,7 +1060,7 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in make ?loc (pll,extern inctx scopes vars c) -and extern_notation (tmp_scope,scopes as allscopes) vars t = function +and extern_notation (custom,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> let loc = Glob_ops.loc_of_glob_constr t in @@ -1064,40 +1107,46 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function let e = match keyrule with | NotationRule (sc,ntn) -> - (match availability_of_notation (sc,ntn) allscopes with + (match availability_of_entry_coercion custom (fst ntn) with + | None -> raise No_match + | Some coercion -> + match availability_of_notation (sc,ntn) scopes with (* Uninterpretation is not allowed in current context *) | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> - let scopes' = Option.List.cons scopt scopes in + let scopes' = Option.List.cons scopt (snd scopes) in let l = - List.map (fun (c,(scopt,scl)) -> + List.map (fun (c,(subentry,(scopt,scl))) -> extern (* assuming no overloading: *) true - (scopt,scl@scopes') vars c) + (subentry,(scopt,scl@scopes')) vars c) terms in let ll = - List.map (fun (c,(scopt,scl)) -> - List.map (extern true (scopt,scl@scopes') vars) c) + List.map (fun (c,(subentry,(scopt,scl))) -> + List.map (extern true (subentry,(scopt,scl@scopes')) vars) c) termlists in let bl = - List.map (fun (bl,(scopt,scl)) -> - mkCPatOr (List.map (extern_cases_pattern_in_scope (scopt,scl@scopes') vars) bl)) + List.map (fun (bl,(subentry,(scopt,scl))) -> + mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)) binders in let bll = - List.map (fun (bl,(scopt,scl)) -> - pi3 (extern_local_binder (scopt,scl@scopes') vars bl)) + List.map (fun (bl,(subentry,(scopt,scl))) -> + pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) binderlists in - insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key) + insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key)) | SynDefRule kn -> + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> let l = - List.map (fun (c,(scopt,scl)) -> - extern true (scopt,scl@scopes) vars c, None) + List.map (fun (c,(subentry,(scopt,scl))) -> + extern true (subentry,(scopt,scl@snd scopes)) vars c, None) terms in - let a = CRef (make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn),None) in - CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in + let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in + insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in if List.is_empty args then e else - let args = fill_arg_scopes args argsscopes scopes in + let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in CAst.make ?loc @@ explicitize false argsimpls (None,e) args with @@ -1111,10 +1160,10 @@ and extern_recursion_order scopes vars = function let extern_glob_constr vars c = - extern false (None,[]) vars c + extern false (InConstrEntrySomeLevel,(None,[])) vars c let extern_glob_type vars c = - extern_typ (None,[]) vars c + extern_typ (InConstrEntrySomeLevel,(None,[])) vars c (******************************************************************) (* Main translation function from constr -> constr_expr *) @@ -1130,7 +1179,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t = let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in - extern false (scopt,[]) vars r + extern false (InConstrEntrySomeLevel,(scopt,[])) vars r let extern_constr_in_scope goal_concl_style scope env sigma t = extern_constr_gen false goal_concl_style (Some scope) env sigma t @@ -1151,14 +1200,14 @@ let extern_closed_glob ?lax goal_concl_style env sigma t = Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in - extern false (None,[]) vars r + extern false (InConstrEntrySomeLevel,(None,[])) vars r (******************************************************************) (* Main translation function from pattern -> constr_expr *) let any_any_branch = (* | _ => _ *) - CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) + CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,IntroAnonymous,None)) let compute_displayed_name_in_pattern sigma avoid na c = let open Namegen in @@ -1182,7 +1231,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.") with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar id - | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) + | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None) | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None), [glob_of_pat avoid env sigma c]) @@ -1207,7 +1256,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) -> @@ -1226,16 +1275,44 @@ 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 = - extern true (None,[]) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat) + extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat) let extern_rel_context where env sigma sign = let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in let vars = vars_of_env env in let a = List.map (extended_glob_local_binder_of_decl) a in - pi3 (extern_local_binder (None,[]) vars a) + pi3 (extern_local_binder (InConstrEntrySomeLevel,(None,[])) vars a) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 8ab70283..f09b316c 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 -> qualid 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 -> qualid) -> unit val get_extern_reference : - unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) + unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid) (** 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 83ace93c..d02f5941 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -15,6 +15,7 @@ open CAst open Names open Nameops open Namegen +open Constr open Libnames open Globnames open Impargs @@ -95,8 +96,8 @@ let is_global id = with Not_found -> false -let global_reference_of_reference ref = - locate_reference (qualid_of_reference ref).CAst.v +let global_reference_of_reference qid = + locate_reference qid let global_reference id = locate_reference (qualid_of_ident id) @@ -116,7 +117,7 @@ let global_reference_in_absolute_module dir id = type internalization_error = | VariableCapture of Id.t * Id.t | IllegalMetavariable - | NotAConstructor of reference + | NotAConstructor of qualid | UnboundFixName of bool * Id.t | NonLinearPattern of Id.t | BadPatternsNumber of int * int @@ -130,8 +131,8 @@ let explain_variable_capture id id' = let explain_illegal_metavariable = str "Metavariables allowed only in patterns" -let explain_not_a_constructor ref = - str "Unknown constructor: " ++ pr_reference ref +let explain_not_a_constructor qid = + str "Unknown constructor: " ++ pr_qualid qid let explain_unbound_fix_name is_cofix id = str "The name" ++ spc () ++ Id.print id ++ @@ -217,30 +218,36 @@ let expand_notation_string ntn n = (* This contracts the special case of "{ _ }" for sumbool, sumor notations *) (* Remark: expansion of squash at definition is done in metasyntax.ml *) let contract_curly_brackets ntn (l,ll,bl,bll) = + match ntn with + | InCustomEntryLevel _,_ -> ntn,(l,ll,bl,bll) + | InConstrEntrySomeLevel, ntn -> let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CNotation ("{ _ }",([a],[],[],[])) } :: l -> + | { CAst.v = CNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[],[],[])) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> a::contract_squash (n+1) l in let l = contract_squash 0 l in (* side effect; don't inline *) - !ntn',(l,ll,bl,bll) + (InConstrEntrySomeLevel,!ntn'),(l,ll,bl,bll) let contract_curly_brackets_pat ntn (l,ll) = + match ntn with + | InCustomEntryLevel _,_ -> ntn,(l,ll) + | InConstrEntrySomeLevel, ntn -> let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CPatNotation ("{ _ }",([a],[]),[]) } :: l -> + | { CAst.v = CPatNotation ((InConstrEntrySomeLevel,"{ _ }"),([a],[]),[]) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> a::contract_squash (n+1) l in let l = contract_squash 0 l in (* side effect; don't inline *) - !ntn',(l,ll) + (InConstrEntrySomeLevel,!ntn'),(l,ll) type intern_env = { ids: Names.Id.Set.t; @@ -393,7 +400,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars env fvs in let bl = List.map CAst.(map (fun id -> - (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) + (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) fvs in let na = match na with @@ -403,7 +410,8 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars let name = let id = match ty with - | { v = CApp ((_, { v = CRef ({v=Ident id},_) } ), _) } -> id + | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> + qualid_basename qid | _ -> default_non_dependent_ident in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name @@ -430,7 +438,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function | GLocalAssum (na,bk,t) -> (na,bk,None,t) | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t) | GLocalDef (na,bk,c,None) -> - let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in + let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,IntroAnonymous,None) in (na,bk,Some c,t) | GLocalPattern (_,_,_,_) -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") @@ -471,7 +479,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func let tyc = match ty with | Some ty -> ty - | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None) + | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None) in let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in let bk = Default Explicit in @@ -501,11 +509,11 @@ let intern_generalization intern env ntnvars loc bk ak c = if pi then (fun {loc=loc';v=id} acc -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ - GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc)) else (fun {loc=loc';v=id} acc -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ - GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) + GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc)) in List.fold_right (fun ({loc;v=id} as lid) (env, acc) -> let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in @@ -525,7 +533,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) (**********************************************************************) @@ -550,12 +558,13 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id = let is_var store pat = match DAst.get pat with - | PatVar na -> store na; true + | PatVar na -> ignore(store na); true | _ -> false let out_var pat = match pat.v with - | CPatAtom (Some ({v=Ident id})) -> Name id + | CPatAtom (Some qid) when qualid_is_ident qid -> + Name (qualid_basename qid) | CPatAtom None -> Anonymous | _ -> assert false @@ -563,7 +572,7 @@ let term_of_name = function | Name id -> DAst.make (GVar id) | Anonymous -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in - DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None)) + DAst.make (GHole (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st }, IntroAnonymous, None)) let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous @@ -605,7 +614,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam (renaming',env), None, Name id' type binder_action = -| AddLetIn of Misctypes.lname * constr_expr * constr_expr option +| AddLetIn of lname * constr_expr * constr_expr option | AddTermIter of (constr_expr * subscopes) Names.Id.Map.t | AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *) | AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *) @@ -621,18 +630,18 @@ let error_cannot_coerce_disjunctive_pattern_term ?loc () = let terms_of_binders bl = let rec term_of_pat pt = dmap_with_loc (fun ?loc -> function - | PatVar (Name id) -> CRef (make @@ Ident id, None) + | PatVar (Name id) -> CRef (qualid_of_ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in - let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in + let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in + let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in - CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in + CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with | bnd :: l -> let loc = bnd.loc in begin match DAst.get bnd with - | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (make ?loc @@ Ident id, None)) :: extract_variables l + | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l | GLocalDef (Name id,_,_,_) -> extract_variables l | GLocalDef (Anonymous,_,_,_) | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.") @@ -707,10 +716,12 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let arg = match arg with | None -> None | Some arg -> - let mk_env (c, (tmp_scope, subscopes)) = + let mk_env id (c, (tmp_scope, subscopes)) map = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in - let gc = intern nenv c in - (gc, Some c) + try + let gc = intern nenv c in + Id.Map.add id (gc, Some c) map + with GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -722,7 +733,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | [pat] -> (glob_constr_of_cases_pattern pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in - let terms = Id.Map.map mk_env terms in + let terms = Id.Map.fold mk_env terms Id.Map.empty in let binders = Id.Map.map mk_env' binders in let bindings = Id.Map.fold Id.Map.add terms binders in Some (Genintern.generic_substitute_notation bindings arg) @@ -805,7 +816,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = distinction *) let cases_pattern_of_name {loc;v=na} = - let atom = match na with Name id -> Some (make ?loc @@ Ident id) | Anonymous -> None in + let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in CAst.make ?loc (CPatAtom atom) let split_by_type ids subst = @@ -814,16 +825,16 @@ let split_by_type ids subst = | [] -> assert false | a::l -> l, Id.Map.add id (a,scl) s in let (terms,termlists,binders,binderlists),subst = - List.fold_left (fun ((terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) (id,(scl,typ)) -> + List.fold_left (fun ((terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) (id,((_,scl),typ)) -> match typ with | 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') @@ -842,10 +853,10 @@ let split_by_type ids subst = subst let split_by_type_pat ?loc ids subst = - let bind id scl l s = + let bind id (_,scopes) l s = match l with | [] -> assert false - | a::l -> l, Id.Map.add id (a,scl) s in + | a::l -> l, Id.Map.add id (a,scopes) s in let (terms,termlists),subst = List.fold_left (fun ((terms,termlists),(terms',termlists')) (id,(scl,typ)) -> match typ with @@ -861,7 +872,7 @@ let split_by_type_pat ?loc ids subst = subst let make_subst ids l = - let fold accu (id, scl) a = Id.Map.add id (a, scl) accu in + let fold accu (id, scopes) a = Id.Map.add id (a, scopes) accu in List.fold_left2 fold Id.Map.empty ids l let intern_notation intern env ntnvars loc ntn fullargs = @@ -902,7 +913,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = try let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in let expl_impls = List.map - (fun id -> CAst.make ?loc @@ CRef (make ?loc @@ Ident id,None), Some (make ?loc @@ ExplByName id)) expl_impls in + (fun id -> CAst.make ?loc @@ CRef (qualid_of_ident ?loc id,None), Some (make ?loc @@ ExplByName id)) expl_impls in let tys = string_of_ty ty in Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys; gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls @@ -969,28 +980,27 @@ let dump_extended_global loc = function | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref | SynDef sp -> Dumpglob.add_glob_kn ?loc sp -let intern_extended_global_of_qualid {loc;v=qid} = - let r = Nametab.locate_extended qid in dump_extended_global loc r; r +let intern_extended_global_of_qualid qid = + let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r -let intern_reference ref = - let qid = qualid_of_reference ref in +let intern_reference qid = let r = try intern_extended_global_of_qualid qid with Not_found -> error_global_not_found qid 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.qualid * 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 ?(no_secvar=false) qid intern env ntnvars us args = @@ -1013,7 +1023,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in let loc = c.loc in let err () = - user_err ?loc (str "Notation " ++ pr_qualid qid.v + user_err ?loc (str "Notation " ++ pr_qualid qid ++ str " cannot have a universe instance," ++ str " its expanded head does not start with a reference") in @@ -1027,37 +1037,35 @@ let intern_qualid ?(no_secvar=false) 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) + user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) | Some _, _ -> err () in c, projapp, args2 -let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = -function - | {loc; v=Qualid qid} -> - let qid = make ?loc qid in - let r,projapp,args2 = - try intern_qualid qid intern env ntnvars us args - with Not_found -> error_global_not_found qid - in - let x, imp, scopes, l = find_appl_head_data r in - (x,imp,scopes,l), args2 - | {loc; v=Ident id} -> - try intern_var env lvar namedctx loc id us, args +let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qid = + let loc = qid.CAst.loc in + if qualid_is_ident qid then + try intern_var env lvar namedctx loc (qualid_basename qid) us, args with Not_found -> - let qid = make ?loc @@ qualid_of_ident id in try let r, projapp, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 with Not_found -> - (* Extra allowance for non globalizing functions *) - if !interning_grammar || env.unb then - (gvar (loc,id) us, [], [], []), args + (* Extra allowance for non globalizing functions *) + if !interning_grammar || env.unb then + (gvar (loc,qualid_basename qid) us, [], [], []), args else error_global_not_found qid + else + let r,projapp,args2 = + try intern_qualid qid intern env ntnvars us args + with Not_found -> error_global_not_found qid + in + let x, imp, scopes, l = find_appl_head_data r in + (x,imp,scopes,l), args2 let interp_reference vars r = let (r,_,_,_),_ = @@ -1072,11 +1080,11 @@ 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 + | RCPatAlias of 'a raw_cases_pattern_expr * lname + | 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 + | RCPatAtom of (lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option | RCPatOr of 'a raw_cases_pattern_expr list and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t @@ -1261,18 +1269,18 @@ let find_constructor loc add_params ref = List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)]) | None -> [] -let find_pattern_variable = function - | {v=Ident id} -> id - | {loc;v=Qualid _} as x -> raise (InternalizationError(loc,NotAConstructor x)) +let find_pattern_variable qid = + if qualid_is_ident qid then qualid_basename qid + else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid)) let check_duplicate loc fields = - let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in + let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in let dups = List.duplicates eq fields in match dups with | [] -> () | (r, _) :: _ -> user_err ?loc (str "This record defines several times the field " ++ - pr_reference r ++ str ".") + pr_qualid r ++ str ".") (** [sort_fields ~complete loc fields completer] expects a list [fields] of field assignments [f = e1; g = e2; ...], where [f, g] @@ -1297,14 +1305,14 @@ let sort_fields ~complete loc fields completer = (gr, Recordops.find_projection gr) with Not_found -> user_err ?loc ~hdr:"intern" - (pr_reference first_field_ref ++ str": Not a projection") + (pr_qualid first_field_ref ++ str": Not a projection") in (* the number of parameters *) let nparams = record.Recordops.s_EXPECTEDPARAM in (* the reference constructor of the record *) let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in - try make ?loc @@ Qualid (shortest_qualid_of_global Id.Set.empty global_record_id) + try shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in @@ -1312,14 +1320,14 @@ let sort_fields ~complete loc fields completer = first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) = - (* elimitate the first field from the projections, + (* eliminate the first field from the projections, but keep its index *) let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc = match projs with | [] -> (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 -> @@ -1355,9 +1363,9 @@ let sort_fields ~complete loc fields completer = let field_glob_ref = try global_reference_of_reference field_ref with Not_found -> user_err ?loc ~hdr:"intern" - (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in + (str "The field \"" ++ pr_qualid 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 @@ -1368,7 +1376,8 @@ let sort_fields ~complete loc fields completer = (* the order does not matter as we sort them next, List.rev_* is just for efficiency *) let remaining_fields = - let complete_field (idx, _field_ref) = (idx, completer idx) in + let complete_field (idx, field_ref) = (idx, + completer idx field_ref record.Recordops.s_CONST) in List.rev_map complete_field remaining_projs in List.rev_append remaining_fields acc in @@ -1384,7 +1393,7 @@ let sort_fields ~complete loc fields completer = (** {6 Manage multiple aliases} *) type alias = { - alias_ids : Misctypes.lident list; + alias_ids : lident list; alias_map : Id.t Id.Map.t; } @@ -1482,10 +1491,9 @@ let drop_notations_pattern looked_for genv = end | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x in - let rec drop_syndef top scopes re pats = - let qid = qualid_of_reference re in + let rec drop_syndef top scopes qid pats = try - match locate_extended qid.v with + match locate_extended qid with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with @@ -1523,7 +1531,7 @@ let drop_notations_pattern looked_for genv = | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id) | CPatRecord l -> let sorted_fields = - sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in + sort_fields ~complete:false loc l (fun _idx fieldname constructor -> CAst.make ?loc @@ CPatAtom None) in begin match sorted_fields with | None -> DAst.make ?loc @@ RCPatAtom None | Some (n, head, pl) -> @@ -1541,10 +1549,10 @@ let drop_notations_pattern looked_for genv = | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (r, Some expl_pl, pl) -> - let g = try locate (qualid_of_reference r).v + | CPatCstr (qid, Some expl_pl, pl) -> + let g = try locate qid with Not_found -> - raise (InternalizationError (loc,NotAConstructor r)) in + raise (InternalizationError (loc,NotAConstructor qid)) in if expl_pl == [] then (* Convention: (@r) deactivates all further implicit arguments and scopes *) DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, []) @@ -1553,11 +1561,11 @@ let drop_notations_pattern looked_for genv = (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) - | CPatNotation ("- _",([a],[]),[]) when is_non_zero_pat a -> + | CPatNotation ((InConstrEntrySomeLevel,"- _"),([a],[]),[]) when is_non_zero_pat a -> let p = match a.CAst.v with CPatPrim (Numeral (p, _)) -> p | _ -> assert false in let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in rcp_of_glob scopes pat - | CPatNotation ("( _ )",([a],[]),[]) -> + | CPatNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) -> in_pat top scopes a | CPatNotation (ntn,fullargs,extrargs) -> let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in @@ -1724,15 +1732,15 @@ let get_implicit_name n imps = let set_hole_implicit i b c = let loc = c.CAst.loc in match DAst.get c with - | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None) | GApp (r, _) -> let loc = r.CAst.loc in begin match DAst.get r with | GRef (r, _) -> - Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) + Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") end - | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) + | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),IntroAnonymous,None) | _ -> anomaly (Pp.str "Only refs have implicits.") let exists_implicit_name id = @@ -1870,10 +1878,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = DAst.make ?loc @@ GLetIn (na.CAst.v, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) - | CNotation ("- _", ([a],[],[],[])) when is_non_zero a -> + | CNotation ((InConstrEntrySomeLevel,"- _"), ([a],[],[],[])) when is_non_zero a -> let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in intern env (CAst.make ?loc @@ CPrim (Numeral (p,false))) - | CNotation ("( _ )",([a],[],[],[])) -> intern env a + | CNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a | CNotation (ntn,args) -> intern_notation intern env ntnvars loc ntn args | CGeneralization (b,a,c) -> @@ -1889,9 +1897,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern_applied_reference intern env (Environ.named_context globalenv) lvar us args ref in - (* Rem: GApp(_,f,[]) stands for @f *) - DAst.make ?loc @@ - GApp (f, intern_args env args_scopes (List.map fst args)) + (* Rem: GApp(_,f,[]) stands for @f *) + if args = [] then DAst.make ?loc @@ GApp (f,[]) else + smart_gapp f loc (intern_args env args_scopes (List.map fst args)) | CApp ((isproj,f), args) -> let f,args = match f.CAst.v with @@ -1917,14 +1925,22 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in let fields = sort_fields ~complete:true loc fs - (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)), - Misctypes.IntroAnonymous, None)) + (fun _idx fieldname constructorname -> + let open Evar_kinds in + let fieldinfo : Evar_kinds.record_field = + {fieldname=fieldname; recordname=inductive_of_constructor constructorname} + in + CAst.make ?loc @@ CHole (Some + (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with + Evar_kinds.qm_obligation=st; + Evar_kinds.qm_record_field=Some fieldinfo + }) , IntroAnonymous, None)) in begin match fields with | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.") | Some (n, constrname, args) -> - let pars = List.make n (CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in + let pars = List.make n (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) in let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in intern env app end @@ -1964,13 +1980,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let main_sub_eqn = CAst.make @@ ([],thepats, (* "|p1,..,pn" *) Option.cata (intern_type env') - (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) + (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None)) rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in let catch_all_sub_eqn = 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)) + DAst.make @@ GHole(Evar_kinds.ImpossibleCase,IntroAnonymous,None))] (* "=> _" *) in + 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 @@ @@ -2000,8 +2016,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | None -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in (match naming with - | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id - | _ -> Evar_kinds.QuestionMark (st,Anonymous)) + | IntroIdentifier id -> Evar_kinds.NamedHole id + | _ -> Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st; }) | Some k -> k in let solve = match solve with @@ -2045,8 +2061,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = GSort s | CCast (c1, c2) -> DAst.make ?loc @@ - GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2) - ) + GCast (intern env c1, map_cast_type (intern_type env) c2) + ) and intern_type env = intern (set_type_scope env) and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list = diff --git a/interp/constrintern.mli b/interp/constrintern.mli index f5e32dc4..dd0944cc 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -11,9 +11,7 @@ open Names open Evd open Environ -open Misctypes open Libnames -open Globnames open Glob_term open Pattern open EConstr @@ -143,10 +141,10 @@ 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 : qualid -> GlobRef.t (** Expands abbreviations (syndef); raise an error if not existing *) -val interp_reference : ltac_sign -> reference -> glob_constr +val interp_reference : ltac_sign -> qualid -> glob_constr (** Interpret binders *) @@ -175,11 +173,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 c55a6c69..a82e6b35 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -150,8 +150,8 @@ let register_side_effect (c, role) = ignore(add_leaf id o); update_tables c; match role with - | Safe_typing.Subproof -> () - | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|] + | Subproof -> () + | Schema (ind, kind) -> !declare_scheme kind [|ind,c|] let declare_constant_common id cst = let o = inConstant cst in @@ -382,19 +382,44 @@ let inInductive : inductive_obj -> obj = discharge_function = discharge_inductive; rebuild_function = infer_inductive_subtyping } -let declare_projections mind = - let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in - match spec.mind_record with - | Some (Some (_, kns, pjs)) -> - Array.iteri (fun i kn -> - let id = Label.to_id (Constant.label kn) in - let entry = {proj_entry_ind = mind; proj_entry_arg = i} in - let kn' = declare_constant id (ProjectionEntry entry, - IsDefinition StructureComponent) - in - assert(Constant.equal kn kn')) kns; true,true - | Some None -> true,false - | None -> false,false +let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = + let id = Label.to_id label in + let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in + Recordops.declare_primitive_projection p; + (* ^ needs to happen before declaring the constant, otherwise + Heads gets confused. *) + let univs = match univs with + | Monomorphic_ind_entry _ -> + (** Global constraints already defined through the inductive *) + Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_ind_entry ctx -> + Polymorphic_const_entry ctx + | Cumulative_ind_entry ctx -> + Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx) + in + let term, types = match univs with + | Monomorphic_const_entry _ -> term, types + | Polymorphic_const_entry ctx -> + let u = Univ.UContext.instance ctx in + Vars.subst_instance_constr u term, Vars.subst_instance_constr u types + in + let entry = definition_entry ~types ~univs term in + ignore(declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent)) + +let declare_projections univs mind = + let env = Global.env () in + let mib = Environ.lookup_mind mind env in + match mib.mind_record with + | PrimRecord info -> + let iter_ind i (_, labs, _) = + let ind = (mind, i) in + let projs = Inductiveops.compute_projections env ind in + Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs + in + let () = Array.iteri iter_ind info in + true + | FakeRecord -> false + | NotRecord -> false (* for initial declaration *) let declare_mind mie = @@ -403,7 +428,7 @@ let declare_mind mie = | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in let mind = Global.mind_of_delta_kn kn in - let isrecord,isprim = declare_projections mind in + let isprim = declare_projections mie.mind_entry_universes mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; oname, isprim @@ -446,24 +471,20 @@ let assumption_message id = discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") -(** Global universe names, in a different summary *) - -type universe_context_decl = polymorphic * Univ.ContextSet.t - -let cache_universe_context (p, ctx) = - Global.push_context_set p ctx; - if p then Lib.add_section_context ctx +(** Monomorphic universes need to survive sections. *) -let input_universe_context : universe_context_decl -> Libobject.obj = +let input_universe_context : Univ.ContextSet.t -> Libobject.obj = declare_object - { (default_object "Global universe context state") with - cache_function = (fun (na, pi) -> cache_universe_context pi); - load_function = (fun _ (_, pi) -> cache_universe_context pi); - discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); - classify_function = (fun a -> Keep a) } + { (default_object "Monomorphic section universes") with + cache_function = (fun (na, uctx) -> Global.push_context_set false uctx); + discharge_function = (fun (_, x) -> Some x); + classify_function = (fun a -> Dispose) } let declare_universe_context poly ctx = - Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) + if poly then + (Global.push_context_set true ctx; Lib.add_section_context ctx) + else + Lib.add_anonymous_leaf (input_universe_context ctx) (** Global universes are not substitutive objects but global objects bound at the *library* or *module* level. The polymorphic flag is @@ -487,7 +508,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 +559,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 +585,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 @@ -572,30 +593,11 @@ let do_universe poly l = ignore(Lib.add_leaf id (input_universe (src, lev)))) l -type constraint_decl = polymorphic * Univ.Constraint.t - -let cache_constraints (na, (p, c)) = - let ctx = - Univ.ContextSet.add_constraints c - Univ.ContextSet.empty (* No declared universes here, just constraints *) - in cache_universe_context (p,ctx) - -let discharge_constraints (_, (p, c as a)) = - if p then None else Some a - -let input_constraints : constraint_decl -> Libobject.obj = - let open Libobject in - declare_object - { (default_object "Global universe constraints") with - cache_function = cache_constraints; - load_function = (fun _ -> cache_constraints); - discharge_function = discharge_constraints; - classify_function = (fun a -> Keep a) } - let do_constraint poly l = + let open Univ in 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 () = @@ -614,7 +616,8 @@ let do_constraint poly l = let constraints = List.fold_left (fun acc (l, d, r) -> let p, lu = u_of_id l and p', ru = u_of_id r in check_poly p p'; - Univ.Constraint.add (lu, d, ru) acc) - Univ.Constraint.empty l + Constraint.add (lu, d, ru) acc) + Constraint.empty l in - Lib.add_anonymous_leaf (input_constraints (poly, constraints)) + let uctx = ContextSet.add_constraints constraints ContextSet.empty in + declare_universe_context poly uctx diff --git a/interp/declare.mli b/interp/declare.mli index 084d746e..02e73cd6 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_universe : polymorphic -> lident list -> unit +val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> unit diff --git a/interp/discharge.ml b/interp/discharge.ml index e16a955d..0e44a8b4 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -111,9 +111,10 @@ let process_inductive info modlist mib = let section_decls' = Context.Named.map discharge section_decls in let (params',inds') = abstract_inductive section_decls' nparamdecls inds in let record = match mib.mind_record with - | Some (Some (id, _, _)) -> Some (Some id) - | Some None -> Some None - | None -> None + | PrimRecord info -> + Some (Some (Array.map pi1 info)) + | FakeRecord -> Some None + | NotRecord -> None in { mind_entry_record = record; mind_entry_finite = mib.mind_finite; diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index bc6a1ef3..ccad6b19 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -113,7 +113,7 @@ let type_of_global_ref gr = "var" ^ type_of_logical_kind (Decls.variable_kind v) | Globnames.IndRef ind -> let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in - if mib.Declarations.mind_record <> None then + if mib.Declarations.mind_record <> Declarations.NotRecord then begin match mib.Declarations.mind_finite with | Finite -> "indrec" | BiFinite -> "rec" @@ -167,7 +167,7 @@ let dump_modref ?loc mp ty = let dump_libref ?loc dp ty = dump_ref ?loc (Names.DirPath.to_string dp) "<>" "<>" ty -let cook_notation df sc = +let cook_notation (from,df) sc = (* We encode notations so that they are space-free and still human-readable *) (* - all spaces are replaced by _ *) (* - all _ denoting a non-terminal symbol are replaced by x *) @@ -203,7 +203,9 @@ let cook_notation df sc = if !i <= l then (set ntn !j '_'; incr j; incr i) done; let df = Bytes.sub_string ntn 0 !j in - match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df + let df_sc = match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df in + let from_df_sc = match from with Constrexpr.InCustomEntryLevel (from,_) -> ":" ^ from ^ df_sc | Constrexpr.InConstrEntrySomeLevel -> ":" ^ df_sc in + from_df_sc let dump_notation_location posl df (((path,secpath),_),sc) = if dump () then @@ -254,7 +256,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 43c10000..931d05a9 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -24,10 +24,10 @@ 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 +val dump_definition : Names.lident -> bool -> string -> unit val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit val dump_reference : ?loc:Loc.t -> string -> string -> 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 : Names.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/genintern.ml b/interp/genintern.ml index 161201c4..d9a0db04 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -26,9 +26,15 @@ let empty_glob_sign env = { extra = Store.empty; } +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option +type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern + type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb type 'glb subst_fun = substitution -> 'glb -> 'glb -type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb +type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb module InternObj = struct diff --git a/interp/genintern.mli b/interp/genintern.mli index d818713f..f4f064bc 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -22,6 +22,12 @@ type glob_sign = { val empty_glob_sign : Environ.env -> glob_sign +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option +type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern + (** {5 Internalization functions} *) type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb @@ -42,7 +48,7 @@ val generic_substitute : glob_generic_argument subst_fun (** {5 Notation functions} *) -type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb +type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml new file mode 100644 index 00000000..607f2258 --- /dev/null +++ b/interp/genredexpr.ml @@ -0,0 +1,65 @@ +(************************************************************************) +(* * 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 Names.lident * 'a + | ConstrTypeOf of 'a + +open Libnames +open Constrexpr + +type r_trm = constr_expr +type r_pat = constr_pattern_expr +type r_cst = qualid 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 9ad62c0d..e542b818 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 *) @@ -671,34 +689,34 @@ let check_rigidity isrigid = user_err (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") let projection_implicits env p impls = - let pb = Environ.lookup_projection p env in - CList.skipn_at_least pb.Declarations.proj_npars impls + let npars = Projection.npars p in + CList.skipn_at_least npars impls let declare_manual_implicits local ref ?enriching l = let flags = !implicit_args in 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 103a4f9e..ea5aa90f 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 diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 58df9abc..4f3037b1 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 * Constr.rel_context (* found, expected *) +let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) + module RelDecl = Context.Rel.Declaration (*i*) @@ -51,14 +53,14 @@ let cache_generalizable_type (_,(local,cmd)) = let load_generalizable_type _ (_,(local,cmd)) = generalizable_table := add_generalizable cmd !generalizable_table -let in_generalizable : bool * Misctypes.lident list option -> obj = +let in_generalizable : bool * lident list option -> obj = declare_object {(default_object "GENERALIZED-IDENT") with load_function = load_generalizable_type; cache_function = cache_generalizable_type; 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 @@ -94,9 +96,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = else l in let rec aux bdvars l c = match CAst.(c.v) with - | CRef ({CAst.v=Ident id},_) -> found c.CAst.loc id bdvars l - | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef ({CAst.v=Ident id},_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) -> - Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c + | CRef (qid,_) when qualid_is_ident qid -> + found c.CAst.loc (qualid_basename qid) bdvars l + | CNotation ((InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when + qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) -> + Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c @@ -194,7 +198,7 @@ let combine_params avoid fn applied needed = let combine_params_freevar = fun avoid (_, decl) -> let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (CAst.make @@ CRef (CAst.make @@ Ident id',None), Id.Set.add id' avoid) + (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) let destClassApp cl = let open CAst in @@ -216,9 +220,8 @@ let destClassAppExpl cl = let implicit_application env ?(allow_partial=true) f ty = let is_class = try - let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in - let qid = qualid_of_reference r in - let gr = Nametab.locate qid.CAst.v in + let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in + let gr = Nametab.locate qid in if Typeclasses.is_class gr then Some (clapp, gr) else None with Not_found -> None in @@ -238,7 +241,7 @@ 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 diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index b9815f34..437fef17 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -12,13 +12,12 @@ 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 -> 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 -val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t +val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t +val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t (** Fragile, should be used only for construction a set of identifiers to avoid *) @@ -32,17 +31,21 @@ val free_vars_of_binders : order with the location of their first occurrence *) val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t -> - glob_constr -> Misctypes.lident list + glob_constr -> lident list 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 * Constr.rel_declaration -> 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 * Constr.rel_declaration -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t + +(* Should be likely located elsewhere *) +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) +val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a diff --git a/interp/interp.mllib b/interp/interp.mllib index bb22cf46..3668455a 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 dc93d8dc..c27cc9cc 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -12,7 +12,7 @@ open Declarations open Libnames open Constrexpr open Constrintern -open Misctypes +open Declaremods type module_internalization_error = | NotAModuleNorModtype of string @@ -23,7 +23,7 @@ exception ModuleInternalizationError of module_internalization_error let error_not_a_module_loc kind loc qid = let s = string_of_qualid qid in - let e = match kind with + let e = let open Declaremods in match kind with | Module -> Modops.ModuleTypingError (Modops.NotAModule s) | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s) | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s) @@ -45,7 +45,9 @@ let error_application_to_module_type loc = or both are searched. The returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) -let lookup_module_or_modtype kind {CAst.loc;v=qid} = +let lookup_module_or_modtype kind qid = + let open Declaremods in + let loc = qid.CAst.loc in try if kind == ModType then raise Not_found; let mp = Nametab.locate_module qid in @@ -63,7 +65,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 -> @@ -83,7 +85,7 @@ let loc_of_module l = l.CAst.loc let rec interp_module_ast env kind m cst = match m with | {CAst.loc;v=CMident qid} -> - let (mp,kind) = lookup_module_or_modtype kind CAst.(make ?loc qid) in + let (mp,kind) = lookup_module_or_modtype kind qid in (MEident mp, kind, cst) | {CAst.loc;v=CMapply (me1,me2)} -> let me1',kind1, cst = interp_module_ast env kind me1 cst in diff --git a/interp/modintern.mli b/interp/modintern.mli index ef37aead..529c438c 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -11,7 +11,6 @@ open Environ open Entries open Constrexpr -open Misctypes (** Module internalization errors *) @@ -30,4 +29,4 @@ exception ModuleInternalizationError of module_internalization_error isn't ModAny. *) val interp_module_ast : - env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t + env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t diff --git a/interp/notation.ml b/interp/notation.ml index bb58f00c..e2751865 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*) @@ -40,6 +39,30 @@ open Context.Named.Declaration expression, set this scope to be the current scope *) +let notation_entry_eq s1 s2 = match (s1,s2) with +| InConstrEntry, InConstrEntry -> true +| InCustomEntry s1, InCustomEntry s2 -> String.equal s1 s2 +| (InConstrEntry | InCustomEntry _), _ -> false + +let notation_entry_level_eq s1 s2 = match (s1,s2) with +| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> true +| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2 +| (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false + +let notation_eq (from1,ntn1) (from2,ntn2) = + notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2 + +let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s + +module NotationOrd = + struct + type t = notation + let compare = Pervasives.compare + end + +module NotationSet = Set.Make(NotationOrd) +module NotationMap = CMap.Make(NotationOrd) + (**********************************************************************) (* Scope of symbols *) @@ -52,13 +75,10 @@ type notation_data = { } type scope = { - notations: notation_data String.Map.t; + notations: notation_data NotationMap.t; 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 @@ -66,7 +86,7 @@ let scope_map = ref String.Map.empty let delimiters_map = ref String.Map.empty let empty_scope = { - notations = String.Map.empty; + notations = NotationMap.empty; delimiters = None } @@ -78,41 +98,6 @@ let init_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 -> @@ -143,12 +128,12 @@ let normalize_scope sc = (**********************************************************************) (* The global stack of scopes *) -type scope_elem = Scope of scope_name | SingleNotation of string +type scope_elem = Scope of scope_name | SingleNotation of notation type scopes = scope_elem list let scope_eq s1 s2 = match s1, s2 with -| Scope s1, Scope s2 -| SingleNotation s1, SingleNotation s2 -> String.equal s1 s2 +| Scope s1, Scope s2 -> String.equal s1 s2 +| SingleNotation s1, SingleNotation s2 -> notation_eq s1 s2 | Scope _, SingleNotation _ | SingleNotation _, Scope _ -> false @@ -200,8 +185,6 @@ let push_scope sc scopes = Scope sc :: scopes let push_scopes = List.fold_right push_scope -type local_scopes = tmp_scope_name option * scope_name list - let make_current_scopes (tmp_scope,scopes) = Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack) @@ -258,7 +241,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 @@ -283,16 +266,14 @@ let keymap_find key map = (* Scopes table : interpretation -> scope_name *) let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) -let prim_token_key_table = ref (KeyMap.empty : (string * (any_glob_constr -> prim_token option) * bool) KeyMap.t) - let glob_prim_constr_key c = match DAst.get c with - | GRef (ref, _) -> RefKey (canonical_gr ref) + | GRef (ref, _) -> Some (canonical_gr ref) | GApp (c, _) -> begin match DAst.get c with - | GRef (ref, _) -> RefKey (canonical_gr ref) - | _ -> Oth + | GRef (ref, _) -> Some (canonical_gr ref) + | _ -> None end - | _ -> Oth + | _ -> None let glob_constr_keys c = match DAst.get c with | GApp (c, _) -> @@ -320,77 +301,521 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) (* Interpreting numbers (not in summary because functional objects) *) type required_module = full_path * string list +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign -type 'a prim_token_interpreter = - ?loc:Loc.t -> 'a -> glob_constr +type prim_token_uid = string -type cases_pattern_status = bool (* true = use prim token in patterns *) +type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr +type 'a prim_token_uninterpreter = any_glob_constr -> 'a option -type 'a prim_token_uninterpreter = - glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status +type 'a prim_token_interpretation = + 'a prim_token_interpreter * 'a prim_token_uninterpreter -type internal_prim_token_interpreter = - ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr) +module InnerPrimToken = struct -let prim_token_interpreter_tab = - (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) + type interpreter = + | RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr) + | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr) + | StringInterp of (?loc:Loc.t -> string -> glob_constr) -let add_prim_token_interpreter sc interp = - try - let cont = Hashtbl.find prim_token_interpreter_tab sc in - Hashtbl.replace prim_token_interpreter_tab sc (interp cont) - with Not_found -> - let cont = (fun ?loc _p -> raise Not_found) in - Hashtbl.add prim_token_interpreter_tab sc (interp cont) + let interp_eq f f' = match f,f' with + | RawNumInterp f, RawNumInterp f' -> f == f' + | BigNumInterp f, BigNumInterp f' -> f == f' + | StringInterp f, StringInterp f' -> f == f' + | _ -> false -let declare_prim_token_interpreter sc interp (patl,uninterp,b) = - declare_scope sc; - add_prim_token_interpreter sc interp; - List.iter (fun pat -> - prim_token_key_table := KeyMap.add - (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table) - patl + let ofNumeral n s = + if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) + + let do_interp ?loc interp primtok = + match primtok, interp with + | Numeral (n,s), RawNumInterp interp -> interp ?loc (n,s) + | Numeral (n,s), BigNumInterp interp -> interp ?loc (ofNumeral n s) + | String s, StringInterp interp -> interp ?loc s + | _ -> raise Not_found + + type uninterpreter = + | RawNumUninterp of (any_glob_constr -> rawnum option) + | BigNumUninterp of (any_glob_constr -> Bigint.bigint option) + | StringUninterp of (any_glob_constr -> string option) + + let uninterp_eq f f' = match f,f' with + | RawNumUninterp f, RawNumUninterp f' -> f == f' + | BigNumUninterp f, BigNumUninterp f' -> f == f' + | StringUninterp f, StringUninterp f' -> f == f' + | _ -> false + + let mkNumeral n = + if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true) + else Numeral (Bigint.to_string (Bigint.neg n), false) -let mkNumeral n = - if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true) - else Numeral (Bigint.to_string (Bigint.neg n), false) + let mkString = function + | None -> None + | Some s -> if Unicode.is_utf8 s then Some (String s) else None -let ofNumeral n s = + let do_uninterp uninterp g = match uninterp with + | RawNumUninterp u -> Option.map (fun (n,s) -> Numeral (n,s)) (u g) + | BigNumUninterp u -> Option.map mkNumeral (u g) + | StringUninterp u -> mkString (u g) + +end + +(* The following two tables of (un)interpreters will *not* be + synchronized. But their indexes will be checked to be unique. + These tables contain primitive token interpreters which are + registered in plugins, such as string and ascii syntax. It is + essential that only plugins add to these tables, and that + vernacular commands do not. See + https://github.com/coq/coq/issues/8401 for details of what goes + wrong when vernacular commands add to these tables. *) +let prim_token_interpreters = + (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.interpreter) Hashtbl.t) + +let prim_token_uninterpreters = + (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t) + +(*******************************************************) +(* Numeral notation interpretation *) +type numeral_notation_error = + | UnexpectedTerm of Constr.t + | UnexpectedNonOptionTerm of Constr.t + +exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error + +type numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number + +type int_ty = + { uint : Names.inductive; + int : Names.inductive } + +type z_pos_ty = + { z_ty : Names.inductive; + pos_ty : Names.inductive } + +type target_kind = + | Int of int_ty (* Coq.Init.Decimal.int + uint *) + | UInt of Names.inductive (* Coq.Init.Decimal.uint *) + | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) + +type option_kind = Option | Direct +type conversion_kind = target_kind * option_kind + +type numeral_notation_obj = + { to_kind : conversion_kind; + to_ty : GlobRef.t; + of_kind : conversion_kind; + of_ty : GlobRef.t; + num_ty : Libnames.qualid; (* for warnings / error messages *) + warning : numnot_option } + +module Numeral = struct +(** * Numeral notation *) + +(** Reduction + + The constr [c] below isn't necessarily well-typed, since we + built it via an [mkApp] of a conversion function on a term + that starts with the right constructor but might be partially + applied. + + At least [c] is known to be evar-free, since it comes from + our own ad-hoc [constr_of_glob] or from conversions such + as [coqint_of_rawnum]. +*) + +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let sigma,t = Typing.type_of env sigma c in + let c' = Vnorm.cbv_vm env sigma c t in + EConstr.Unsafe.to_constr c' + +(* For testing with "compute" instead of "vm_compute" : +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let c' = Tacred.compute env sigma c in + EConstr.Unsafe.to_constr c' +*) + +let eval_constr_app env sigma c1 c2 = + eval_constr env sigma (mkApp (c1,[| c2 |])) + +exception NotANumber + +let warn_large_num = + CWarnings.create ~name:"large-number" ~category:"numbers" + (fun ty -> + strbrk "Stack overflow or segmentation fault happens when " ++ + strbrk "working with large numbers in " ++ pr_qualid ty ++ + strbrk " (threshold may vary depending" ++ + strbrk " on your system limits and on the command executed).") + +let warn_abstract_large_num = + CWarnings.create ~name:"abstract-large-number" ~category:"numbers" + (fun (ty,f) -> + strbrk "To avoid stack overflow, large numbers in " ++ + pr_qualid ty ++ strbrk " are interpreted as applications of " ++ + Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".") + +(** Comparing two raw numbers (base 10, big-endian, non-negative). + A bit nasty, but not critical: only used to decide when a + number is considered as large (see warnings above). *) + +exception Comp of int + +let rec rawnum_compare s s' = + let l = String.length s and l' = String.length s' in + if l < l' then - rawnum_compare s' s + else + let d = l-l' in + try + for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done; + for i = d to l-1 do + let c = Pervasives.compare s.[i] s'.[i-d] in + if c != 0 then raise (Comp c) + done; + 0 + with Comp c -> c + +(***********************************************************************) + +(** ** Conversion between Coq [Decimal.int] and internal raw string *) + +(** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *) + +let digit_of_char c = + assert ('0' <= c && c <= '9'); + Char.code c - Char.code '0' + 2 + +let char_of_digit n = + assert (2<=n && n<=11); + Char.chr (n-2 + Char.code '0') + +let coquint_of_rawnum uint str = + let nil = mkConstruct (uint,1) in + let rec do_chars s i acc = + if i < 0 then acc + else + let dg = mkConstruct (uint, digit_of_char s.[i]) in + do_chars s (i-1) (mkApp(dg,[|acc|])) + in + do_chars str (String.length str - 1) nil + +let coqint_of_rawnum inds (str,sign) = + let uint = coquint_of_rawnum inds.uint str in + mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|]) + +let rawnum_of_coquint c = + let rec of_uint_loop c buf = + match Constr.kind c with + | Construct ((_,1), _) (* Nil *) -> () + | App (c, [|a|]) -> + (match Constr.kind c with + | Construct ((_,n), _) (* D0 to D9 *) -> + let () = Buffer.add_char buf (char_of_digit n) in + of_uint_loop a buf + | _ -> raise NotANumber) + | _ -> raise NotANumber + in + let buf = Buffer.create 64 in + let () = of_uint_loop c buf in + if Int.equal (Buffer.length buf) 0 then + (* To avoid ambiguities between Nil and (D0 Nil), we choose + to not display Nil alone as "0" *) + raise NotANumber + else Buffer.contents buf + +let rawnum_of_coqint c = + match Constr.kind c with + | App (c,[|c'|]) -> + (match Constr.kind c with + | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true) + | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false) + | _ -> raise NotANumber) + | _ -> raise NotANumber + + +(***********************************************************************) + +(** ** Conversion between Coq [Z] and internal bigint *) + +(** First, [positive] from/to bigint *) + +let rec pos_of_bigint posty n = + match Bigint.div2_with_rest n with + | (q, false) -> + let c = mkConstruct (posty, 2) in (* xO *) + mkApp (c, [| pos_of_bigint posty q |]) + | (q, true) when not (Bigint.equal q Bigint.zero) -> + let c = mkConstruct (posty, 1) in (* xI *) + mkApp (c, [| pos_of_bigint posty q |]) + | (q, true) -> + mkConstruct (posty, 3) (* xH *) + +let rec bigint_of_pos c = match Constr.kind c with + | Construct ((_, 3), _) -> (* xH *) Bigint.one + | App (c, [| d |]) -> + begin match Constr.kind c with + | Construct ((_, n), _) -> + begin match n with + | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d)) + | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d) + | n -> assert false (* no other constructor of type positive *) + end + | x -> raise NotANumber + end + | x -> raise NotANumber + +(** Now, [Z] from/to bigint *) + +let z_of_bigint { z_ty; pos_ty } n = + if Bigint.equal n Bigint.zero then + mkConstruct (z_ty, 1) (* Z0 *) + else + let (s, n) = + if Bigint.is_pos_or_zero n then (2, n) (* Zpos *) + else (3, Bigint.neg n) (* Zneg *) + in + let c = mkConstruct (z_ty, s) in + mkApp (c, [| pos_of_bigint pos_ty n |]) + +let bigint_of_z z = match Constr.kind z with + | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero + | App (c, [| d |]) -> + begin match Constr.kind c with + | Construct ((_, n), _) -> + begin match n with + | 2 -> (* Zpos *) bigint_of_pos d + | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d) + | n -> assert false (* no other constructor of type Z *) + end + | _ -> raise NotANumber + end + | _ -> raise NotANumber + +(** The uninterp function below work at the level of [glob_constr] + which is too low for us here. So here's a crude conversion back + to [constr] for the subset that concerns us. *) + +let rec constr_of_glob env sigma g = match DAst.get g with + | Glob_term.GRef (ConstructRef c, _) -> + let sigma,c = Evd.fresh_constructor_instance env sigma c in + sigma,mkConstructU c + | Glob_term.GApp (gc, gcl) -> + let sigma,c = constr_of_glob env sigma gc in + let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in + sigma,mkApp (c, Array.of_list cl) + | _ -> + raise NotANumber + +let rec glob_of_constr ?loc env sigma c = match Constr.kind c with + | App (c, ca) -> + let c = glob_of_constr ?loc env sigma c in + let cel = List.map (glob_of_constr ?loc env sigma) (Array.to_list ca) in + DAst.make ?loc (Glob_term.GApp (c, cel)) + | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None)) + | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) + | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) + | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) + | _ -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedTerm c)) + +let no_such_number ?loc ty = + CErrors.user_err ?loc + (str "Cannot interpret this number as a value of type " ++ + pr_qualid ty) + +let interp_option ty ?loc env sigma c = + match Constr.kind c with + | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c + | App (_None, [| _ |]) -> no_such_number ?loc ty + | x -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedNonOptionTerm c)) + +let uninterp_option c = + match Constr.kind c with + | App (_Some, [| _; x |]) -> x + | _ -> raise NotANumber + +let big2raw n = + if Bigint.is_pos_or_zero n then (Bigint.to_string n, true) + else (Bigint.to_string (Bigint.neg n), false) + +let raw2big (n,s) = if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) -let mkString = function -| None -> None -| Some s -> if Unicode.is_utf8 s then Some (String s) else None +let interp o ?loc n = + begin match o.warning with + | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 -> + warn_large_num o.num_ty + | _ -> () + end; + let c = match fst o.to_kind with + | Int int_ty -> coqint_of_rawnum int_ty n + | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n) + | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty + | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n) + in + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in + let to_ty = EConstr.Unsafe.to_constr to_ty in + match o.warning, snd o.to_kind with + | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 -> + warn_abstract_large_num (o.num_ty,o.to_ty); + glob_of_constr ?loc env sigma (mkApp (to_ty,[|c|])) + | _ -> + let res = eval_constr_app env sigma to_ty c in + match snd o.to_kind with + | Direct -> glob_of_constr ?loc env sigma res + | Option -> interp_option o.num_ty ?loc env sigma res + +let uninterp o (Glob_term.AnyGlobConstr n) = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in + let of_ty = EConstr.Unsafe.to_constr of_ty in + try + let sigma,n = constr_of_glob env sigma n in + let c = eval_constr_app env sigma of_ty n in + let c = if snd o.of_kind == Direct then c else uninterp_option c in + match fst o.of_kind with + | Int _ -> Some (rawnum_of_coqint c) + | UInt _ -> Some (rawnum_of_coquint c, true) + | Z _ -> Some (big2raw (bigint_of_z c)) + with + | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) + | NotANumber -> None (* all other functions except big2raw *) +end + +(* A [prim_token_infos], which is synchronized with the document + state, either contains a unique id pointing to an unsynchronized + prim token function, or a numeral notation object describing how to + interpret and uninterpret. We provide [prim_token_infos] because + we expect plugins to provide their own interpretation functions, + rather than going through numeral notations, which are available as + a vernacular. *) + +type prim_token_interp_info = + Uid of prim_token_uid + | NumeralNotation of numeral_notation_obj + +type prim_token_infos = { + pt_local : bool; (** Is this interpretation local? *) + pt_scope : scope_name; (** Concerned scope *) + pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *) + pt_required : required_module; (** Module that should be loaded first *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} -let delay dir int ?loc x = (dir, (fun () -> int ?loc x)) +(* Table from scope_name to backtrack-able informations about interpreters + (in particular interpreter unique id). *) +let prim_token_interp_infos = + ref (String.Map.empty : (required_module * prim_token_interp_info) String.Map.t) + +(* Table from global_reference to backtrack-able informations about + prim_token uninterpretation (in particular uninterpreter unique id). *) +let prim_token_uninterp_infos = + ref (Refmap.empty : (scope_name * prim_token_interp_info * bool) Refmap.t) + +let hashtbl_check_and_set allow_overwrite uid f h eq = + match Hashtbl.find h uid with + | exception Not_found -> Hashtbl.add h uid f + | _ when allow_overwrite -> Hashtbl.add h uid f + | g when eq f g -> () + | _ -> + user_err ~hdr:"prim_token_interpreter" + (str "Unique identifier " ++ str uid ++ + str " already used to register a numeral or string (un)interpreter.") + +let register_gen_interpretation allow_overwrite uid (interp, uninterp) = + hashtbl_check_and_set + allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq; + hashtbl_check_and_set + allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq + +let register_rawnumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp) + +let register_bignumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp) + +let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp) + +let cache_prim_token_interpretation (_,infos) = + let ptii = infos.pt_interp_info in + let sc = infos.pt_scope in + declare_scope sc; + prim_token_interp_infos := + String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos; + List.iter (fun r -> prim_token_uninterp_infos := + Refmap.add r (sc,ptii,infos.pt_in_match) + !prim_token_uninterp_infos) + infos.pt_refs + +let subst_prim_token_interpretation (subs,infos) = + { infos with + pt_refs = List.map (subst_global_reference subs) infos.pt_refs } + +let classify_prim_token_interpretation infos = + if infos.pt_local then Dispose else Substitute infos + +let inPrimTokenInterp : prim_token_infos -> obj = + declare_object {(default_object "PRIM-TOKEN-INTERP") with + open_function = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o); + cache_function = cache_prim_token_interpretation; + subst_function = subst_prim_token_interpretation; + classify_function = classify_prim_token_interpretation} + +let enable_prim_token_interpretation infos = + Lib.add_anonymous_leaf (inPrimTokenInterp infos) + +(** Compatibility. + Avoid the next two functions, they will now store unnecessary + objects in the library segment. Instead, combine + [register_*_interpretation] and [enable_prim_token_interpretation] + (the latter inside a [Mltop.declare_cache_obj]). +*) -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign +let fresh_string_of = + let count = ref 0 in + fun root -> count := !count+1; (string_of_int !count)^"_"^root + +let declare_numeral_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = + let uid = fresh_string_of sc in + register_bignumeral_interpretation uid (interp,uninterp); + enable_prim_token_interpretation + { pt_local = local; + pt_scope = sc; + pt_interp_info = Uid uid; + pt_required = dir; + pt_refs = List.map_filter glob_prim_constr_key patl; + pt_in_match = b } +let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = + let uid = fresh_string_of sc in + register_string_interpretation uid (interp,uninterp); + enable_prim_token_interpretation + { pt_local = local; + pt_scope = sc; + pt_interp_info = Uid uid; + pt_required = dir; + pt_refs = List.map_filter glob_prim_constr_key patl; + pt_in_match = b } -let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) = - declare_prim_token_interpreter sc - (fun cont ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s) - | p -> cont ?loc p) - (patl, (fun r -> match uninterp r with - | None -> None - | Some (n,s) -> Some (Numeral (n,s))), inpat) - -let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = - let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in - declare_prim_token_interpreter sc - (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s) - | p -> cont ?loc p) - (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat) - -let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = - declare_prim_token_interpreter sc - (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p) - (patl, (fun r -> mkString (uninterp r)), inpat) let check_required_module ?loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () with Not_found -> - user_err ?loc ~hdr:"prim_token_interpreter" - (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") + match d with + | [] -> user_err ?loc ~hdr:"prim_token_interpreter" + (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++ str " could not be found in the current environment.") + | _ -> user_err ?loc ~hdr:"prim_token_interpreter" + (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) @@ -418,7 +843,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function end | SingleNotation ntn' :: scopes -> begin match ntn_scope, ntn with - | None, Some ntn when String.equal ntn ntn' -> + | None, Some ntn when notation_eq ntn ntn' -> Some (None, None) | _ -> find_without_delimiters find (ntn_scope,ntn) scopes @@ -427,24 +852,12 @@ 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 ?(onlyprint=false) 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,onlyprint) !notation_level_map - -let level_of_notation ?(onlyprint=false) ntn = - let (level,onlyprint') = String.Map.find ntn !notation_level_map in - if onlyprint' && not onlyprint then raise Not_found; - level - (* The mapping between notations and their interpretation *) let warn_notation_overridden = CWarnings.create ~name:"notation-overridden" ~category:"parsing" (fun (ntn,which_scope) -> - str "Notation" ++ spc () ++ str ntn ++ spc () + str "Notation" ++ spc () ++ pr_notation ntn ++ spc () ++ strbrk "was already used" ++ which_scope ++ str ".") let declare_notation_interpretation ntn scopt pat df ~onlyprint = @@ -452,7 +865,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = let sc = find_scope scope in if not onlyprint then begin let () = - if String.Map.mem ntn sc.notations then + if NotationMap.mem ntn sc.notations then let which_scope = match scopt with | None -> mt () | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in @@ -462,7 +875,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = not_interp = pat; not_location = df; } in - let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in + let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in scope_map := String.Map.add scope sc !scope_map end; begin match scopt with @@ -479,7 +892,7 @@ let rec find_interpretation ntn find = function | Scope scope :: scopes -> (try let (pat,df) = find scope in pat,(df,Some scope) with Not_found -> find_interpretation ntn find scopes) - | SingleNotation ntn'::scopes when String.equal ntn' ntn -> + | SingleNotation ntn'::scopes when notation_eq ntn' ntn -> (try let (pat,df) = find default_scope in pat,(df,None) with Not_found -> (* e.g. because single notation only for constr, not cases_pattern *) @@ -488,12 +901,12 @@ let rec find_interpretation ntn find = function find_interpretation ntn find scopes let find_notation ntn sc = - let n = String.Map.find ntn (find_scope sc).notations in + let n = NotationMap.find ntn (find_scope sc).notations in (n.not_interp, n.not_location) let notation_of_prim_token = function - | Numeral (n,true) -> n - | Numeral (n,false) -> "- "^n + | Numeral (n,true) -> InConstrEntrySomeLevel, n + | Numeral (n,false) -> InConstrEntrySomeLevel, "- "^n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = @@ -505,21 +918,25 @@ let find_prim_token check_allowed ?loc p sc = pat, df with Not_found -> (* Try for a primitive numerical notation *) - let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc ?loc p in + let (spdir,info) = String.Map.find sc !prim_token_interp_infos in check_required_module ?loc sc spdir; - let pat = interp () in + let interp = match info with + | Uid uid -> Hashtbl.find prim_token_interpreters uid + | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o) + in + let pat = InnerPrimToken.do_interp ?loc interp p in check_allowed pat; pat, ((dirpath (fst spdir),DirPath.empty),"") let interp_prim_token_gen ?loc g p local_scopes = let scopes = make_current_scopes local_scopes in - let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in + let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes with Not_found -> user_err ?loc ~hdr:"interp_prim_token" ((match p with | Numeral _ -> - str "No interpretation for numeral " ++ str (notation_of_prim_token p) + str "No interpretation for numeral " ++ pr_notation (notation_of_prim_token p) | String s -> str "No interpretation for string " ++ qs s) ++ str ".") let interp_prim_token ?loc = @@ -544,7 +961,7 @@ let interp_notation ?loc ntn local_scopes = try find_interpretation ntn (find_notation ntn) scopes with Not_found -> user_err ?loc - (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") + (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".") let uninterp_notations c = List.map_append (fun key -> keymap_find key !notations_key_table) @@ -558,47 +975,161 @@ let uninterp_ind_pattern_notations ind = let availability_of_notation (ntn_scope,ntn) scopes = let f scope = - String.Map.mem ntn (String.Map.find scope !scope_map).notations in + NotationMap.mem ntn (String.Map.find scope !scope_map).notations in find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes) -let uninterp_prim_token c = +(* We support coercions from a custom entry at some level to an entry + at some level (possibly the same), and from and to the constr entry. E.g.: + + Notation "[ expr ]" := expr (expr custom group at level 1). + Notation "( x )" := x (in custom group at level 0, x at level 1). + Notation "{ x }" := x (in custom group at level 0, x constr). + + Supporting any level is maybe overkill in that coercions are + commonly from the lowest level of the source entry to the highest + level of the target entry. *) + +type entry_coercion = notation list + +module EntryCoercionOrd = + struct + type t = notation_entry * notation_entry + let compare = Pervasives.compare + end + +module EntryCoercionMap = Map.Make(EntryCoercionOrd) + +let entry_coercion_map = ref EntryCoercionMap.empty + +let level_ord lev lev' = + match lev, lev' with + | None, _ -> true + | _, None -> true + | Some n, Some n' -> n <= n' + +let rec search nfrom nto = function + | [] -> raise Not_found + | ((pfrom,pto),coe)::l -> + if level_ord pfrom nfrom && level_ord nto pto then coe else search nfrom nto l + +let decompose_custom_entry = function + | InConstrEntrySomeLevel -> InConstrEntry, None + | InCustomEntryLevel (s,n) -> InCustomEntry s, Some n + +let availability_of_entry_coercion entry entry' = + let entry, lev = decompose_custom_entry entry in + let entry', lev' = decompose_custom_entry entry' in + if notation_entry_eq entry entry' && level_ord lev' lev then Some [] + else + try Some (search lev lev' (EntryCoercionMap.find (entry,entry') !entry_coercion_map)) + with Not_found -> None + +let better_path ((lev1,lev2),path) ((lev1',lev2'),path') = + (* better = shorter and lower source and higher target *) + level_ord lev1 lev1' && level_ord lev2' lev2 && List.length path <= List.length path' + +let shorter_path (_,path) (_,path') = + List.length path <= List.length path' + +let rec insert_coercion_path path = function + | [] -> [path] + | path'::paths as allpaths -> + (* If better or equal we keep the more recent one *) + if better_path path path' then path::paths + else if better_path path' path then allpaths + else if shorter_path path path' then path::allpaths + else path'::insert_coercion_path path paths + +let declare_entry_coercion (entry,_ as ntn) entry' = + let entry, lev = decompose_custom_entry entry in + let entry', lev' = decompose_custom_entry entry' in + (* Transitive closure *) + let toaddleft = + EntryCoercionMap.fold (fun (entry'',entry''') paths l -> + List.fold_right (fun ((lev'',lev'''),path) l -> + if notation_entry_eq entry entry''' && level_ord lev lev''' && + not (notation_entry_eq entry' entry'') + then ((entry'',entry'),((lev'',lev'),path@[ntn]))::l else l) paths l) + !entry_coercion_map [] in + let toaddright = + EntryCoercionMap.fold (fun (entry'',entry''') paths l -> + List.fold_right (fun ((lev'',lev'''),path) l -> + if entry' = entry'' && level_ord lev' lev'' && entry <> entry''' + then ((entry,entry'''),((lev,lev'''),path@[ntn]))::l else l) paths l) + !entry_coercion_map [] in + entry_coercion_map := + List.fold_right (fun (pair,path) -> + let olds = try EntryCoercionMap.find pair !entry_coercion_map with Not_found -> [] in + EntryCoercionMap.add pair (insert_coercion_path path olds)) + (((entry,entry'),((lev,lev'),[ntn]))::toaddright@toaddleft) + !entry_coercion_map + +let entry_has_global_map = ref String.Map.empty + +let declare_custom_entry_has_global s n = try - let (sc,numpr,_) = - KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in - match numpr (AnyGlobConstr c) with - | None -> raise Notation_ops.No_match - | Some n -> (sc,n) - with Not_found -> raise Notation_ops.No_match - -let uninterp_prim_token_ind_pattern ind args = - let ref = IndRef ind in + let p = String.Map.find s !entry_has_global_map in + user_err (str "Custom entry " ++ str s ++ + str " has already a rule for global references at level " ++ int p ++ str ".") + with Not_found -> + entry_has_global_map := String.Map.add s n !entry_has_global_map + +let entry_has_global = function + | InConstrEntrySomeLevel -> true + | InCustomEntryLevel (s,n) -> + try String.Map.find s !entry_has_global_map <= n with Not_found -> false + +let entry_has_ident_map = ref String.Map.empty + +let declare_custom_entry_has_ident s n = try - let k = RefKey (canonical_gr ref) in - let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in - if not b then raise Notation_ops.No_match; - let args' = List.map - (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in - let ref = DAst.make @@ GRef (ref,None) in - match numpr (AnyGlobConstr (DAst.make @@ GApp (ref,args'))) with - | None -> raise Notation_ops.No_match - | Some n -> (sc,n) - with Not_found -> raise Notation_ops.No_match + let p = String.Map.find s !entry_has_ident_map in + user_err (str "Custom entry " ++ str s ++ + str " has already a rule for global references at level " ++ int p ++ str ".") + with Not_found -> + entry_has_ident_map := String.Map.add s n !entry_has_ident_map + +let entry_has_ident = function + | InConstrEntrySomeLevel -> true + | InCustomEntryLevel (s,n) -> + try String.Map.find s !entry_has_ident_map <= n with Not_found -> false + +let uninterp_prim_token c = + match glob_prim_constr_key c with + | None -> raise Notation_ops.No_match + | Some r -> + try + let (sc,info,_) = Refmap.find r !prim_token_uninterp_infos in + let uninterp = match info with + | Uid uid -> Hashtbl.find prim_token_uninterpreters uid + | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o) + in + match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with + | None -> raise Notation_ops.No_match + | Some n -> (sc,n) + with Not_found -> raise Notation_ops.No_match let uninterp_prim_token_cases_pattern c = - try - let k = cases_pattern_key c in - let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in - if not b then raise Notation_ops.No_match; - let na,c = glob_constr_of_closed_cases_pattern c in - match numpr (AnyGlobConstr c) with - | None -> raise Notation_ops.No_match - | Some n -> (na,sc,n) - with Not_found -> raise Notation_ops.No_match + match glob_constr_of_closed_cases_pattern c with + | exception Not_found -> raise Notation_ops.No_match + | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n) let availability_of_prim_token n printer_scope local_scopes = let f scope = - try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true - with Not_found -> false in + try + let uid = snd (String.Map.find scope !prim_token_interp_infos) in + let open InnerPrimToken in + match n, uid with + | Numeral _, NumeralNotation _ -> true + | _, NumeralNotation _ -> false + | _, Uid uid -> + let interp = Hashtbl.find prim_token_interpreters uid in + match n, interp with + | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true + | String _, StringInterp _ -> true + | _ -> false + with Not_found -> false + in let scopes = make_current_scopes local_scopes in Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) @@ -619,7 +1150,8 @@ let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeBinderList, NtnTypeBinderList -> true | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false -let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) = +let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) = + notation_entry_level_eq entry1 entry2 && pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && ntpe_eq tp1 tp2 @@ -631,7 +1163,7 @@ let exists_notation_in_scope scopt ntn onlyprint r = let scope = match scopt with Some s -> s | None -> default_scope in try let sc = String.Map.find scope !scope_map in - let n = String.Map.find ntn sc.notations in + let n = NotationMap.find ntn sc.notations in interpretation_eq n.not_interp r with Not_found -> false @@ -741,7 +1273,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 +1310,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 @@ -847,10 +1379,10 @@ let rec string_of_symbol = function let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"] | Break _ -> [] -let make_notation_key symbols = - String.concat " " (List.flatten (List.map string_of_symbol symbols)) +let make_notation_key from symbols = + (from,String.concat " " (List.flatten (List.map string_of_symbol symbols))) -let decompose_notation_key s = +let decompose_notation_key (from,s) = let len = String.length s in let rec decomp_ntn dirs n = if n>=len then List.rev dirs else @@ -865,7 +1397,7 @@ let decompose_notation_key s = | s -> Terminal (String.drop_simple_quotes s) in decomp_ntn (tok::dirs) (pos+1) in - decomp_ntn [] 0 + from, decomp_ntn [] 0 (************) (* Printing *) @@ -894,14 +1426,14 @@ let pr_notation_info prglob ntn c = let pr_named_scope prglob scope sc = (if String.equal scope default_scope then - match String.Map.cardinal sc.notations with + match NotationMap.cardinal sc.notations with | 0 -> str "No lonely notation" | n -> str "Lonely notation" ++ (if Int.equal n 1 then mt() else str"s") else str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters) ++ fnl () ++ pr_scope_classes scope - ++ String.Map.fold + ++ NotationMap.fold (fun ntn { not_interp = (_, r); not_location = (_, df) } strm -> pr_notation_info prglob df r ++ fnl () ++ strm) sc.notations (mt ()) @@ -916,11 +1448,11 @@ let pr_scopes prglob = let rec find_default ntn = function | [] -> None | Scope scope :: scopes -> - if String.Map.mem ntn (find_scope scope).notations then + if NotationMap.mem ntn (find_scope scope).notations then Some scope else find_default ntn scopes | SingleNotation ntn' :: scopes -> - if String.equal ntn ntn' then Some default_scope + if notation_eq ntn ntn' then Some default_scope else find_default ntn scopes let factorize_entries = function @@ -929,7 +1461,7 @@ let factorize_entries = function let (ntn,l_of_ntn,rest) = List.fold_left (fun (a',l,rest) (a,c) -> - if String.equal a a' then (a',c::l,rest) else (a,[c],(a',l)::rest)) + if notation_eq a a' then (a',c::l,rest) else (a,[c],(a',l)::rest)) (ntn,[c],[]) l in (ntn,l_of_ntn)::rest @@ -984,15 +1516,15 @@ let possible_notations ntn = (* Only "_ U _" format *) [ntn] else - let ntn' = make_notation_key (raw_analyze_notation_tokens toks) in + let _,ntn' = make_notation_key None (raw_analyze_notation_tokens toks) in if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn'] let browse_notation strict ntn map = let ntns = possible_notations ntn in - let find ntn' ntn = + let find (from,ntn' as fullntn') ntn = if String.contains ntn ' ' then String.equal ntn ntn' else - let toks = decompose_notation_key ntn' in + let _,toks = decompose_notation_key fullntn' in let get_terminals = function Terminal ntn -> Some ntn | _ -> None in let trms = List.map_filter get_terminals toks in if strict then String.List.equal [ntn] trms @@ -1001,10 +1533,10 @@ let browse_notation strict ntn map = let l = String.Map.fold (fun scope_name sc -> - String.Map.fold (fun ntn { not_interp = (_, r); not_location = df } l -> + NotationMap.fold (fun ntn { not_interp = (_, r); not_location = df } l -> if List.exists (find ntn) ntns then (ntn,(scope_name,r,df))::l else l) sc.notations) map [] in - List.sort (fun x y -> String.compare (fst x) (fst y)) l + List.sort (fun x y -> String.compare (snd (fst x)) (snd (fst y))) l let global_reference_of_notation test (ntn,(sc,c,_)) = match c with @@ -1065,9 +1597,9 @@ let locate_notation prglob ntn scope = let collect_notation_in_scope scope sc known = assert (not (String.equal scope default_scope)); - String.Map.fold + NotationMap.fold (fun ntn { not_interp = (_, r); not_location = (_, df) } (l,known as acc) -> - if String.List.mem ntn known then acc else ((df,r)::l,ntn::known)) + if List.mem_f notation_eq ntn known then acc else ((df,r)::l,ntn::known)) sc.notations ([],known) let collect_notations stack = @@ -1080,10 +1612,10 @@ let collect_notations stack = collect_notation_in_scope scope (find_scope scope) knownntn in ((scope,l)::all,knownntn) | SingleNotation ntn -> - if String.List.mem ntn knownntn then (all,knownntn) + if List.mem_f notation_eq ntn knownntn then (all,knownntn) else let { not_interp = (_, r); not_location = (_, df) } = - String.Map.find ntn (find_scope default_scope).notations in + NotationMap.find ntn (find_scope default_scope).notations in let all' = match all with | (s,lonelyntn)::rest when String.equal s default_scope -> (s,(df,r)::lonelyntn)::rest @@ -1113,64 +1645,35 @@ 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, + !prim_token_interp_infos, !prim_token_uninterp_infos, + !entry_coercion_map, !entry_has_global_map, + !entry_has_ident_map) -let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = +let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = 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 + scope_class_map := clsc; + prim_token_interp_infos := ptii; + prim_token_uninterp_infos := ptui; + entry_coercion_map := coe; + entry_has_global_map := globs; + entry_has_ident_map := ids 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 + scope_class_map := initial_scope_class_map; + prim_token_interp_infos := String.Map.empty; + prim_token_uninterp_infos := Refmap.empty let _ = Summary.declare_summary "symbols" diff --git a/interp/notation.mli b/interp/notation.mli index 18671feb..eb080f57 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -8,17 +8,29 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Bigint open Names open Libnames -open Globnames open Constrexpr open Glob_term open Notation_term -open Ppextend (** Notations *) +val pr_notation : notation -> Pp.t +(** Printing *) + +val notation_entry_eq : notation_entry -> notation_entry -> bool +(** Equality on [notation_entry]. *) + +val notation_entry_level_eq : notation_entry_level -> notation_entry_level -> bool +(** Equality on [notation_entry_level]. *) + +val notation_eq : notation -> notation -> bool +(** Equality on [notation]. *) + +module NotationSet : Set.S with type elt = notation +module NotationMap : CMap.ExtS with type key = notation and module Set := NotationSet + (** {6 Scopes } *) (** A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters *) @@ -27,14 +39,10 @@ type delimiters = string type scope type scopes (** = [scope_name list] *) -type local_scopes = tmp_scope_name option * scope_name list - 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 @@ -66,33 +74,112 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name type notation_location = (DirPath.t * DirPath.t) * string type required_module = full_path * string list -type cases_pattern_status = bool (** true = use prim token in patterns *) +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign -type 'a prim_token_interpreter = - ?loc:Loc.t -> 'a -> glob_constr +(** The unique id string below will be used to refer to a particular + registered interpreter/uninterpreter of numeral or string notation. + Using the same uid for different (un)interpreters will fail. + If at most one interpretation of prim token is used per scope, + then the scope name could be used as unique id. *) -type 'a prim_token_uninterpreter = - glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status +type prim_token_uid = string -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign +type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr +type 'a prim_token_uninterpreter = any_glob_constr -> 'a option + +type 'a prim_token_interpretation = + 'a prim_token_interpreter * 'a prim_token_uninterpreter + +val register_rawnumeral_interpretation : + ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit + +val register_bignumeral_interpretation : + ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + +val register_string_interpretation : + ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit + +(** * Numeral notation *) -val declare_rawnumeral_interpreter : scope_name -> required_module -> - rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit +type numeral_notation_error = + | UnexpectedTerm of Constr.t + | UnexpectedNonOptionTerm of Constr.t -val declare_numeral_interpreter : scope_name -> required_module -> - bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit +exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error -val declare_string_interpreter : scope_name -> required_module -> - string prim_token_interpreter -> string prim_token_uninterpreter -> unit +type numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number + +type int_ty = + { uint : Names.inductive; + int : Names.inductive } + +type z_pos_ty = + { z_ty : Names.inductive; + pos_ty : Names.inductive } + +type target_kind = + | Int of int_ty (* Coq.Init.Decimal.int + uint *) + | UInt of Names.inductive (* Coq.Init.Decimal.uint *) + | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) + +type option_kind = Option | Direct +type conversion_kind = target_kind * option_kind + +type numeral_notation_obj = + { to_kind : conversion_kind; + to_ty : GlobRef.t; + of_kind : conversion_kind; + of_ty : GlobRef.t; + num_ty : Libnames.qualid; (* for warnings / error messages *) + warning : numnot_option } + +type prim_token_interp_info = + Uid of prim_token_uid + | NumeralNotation of numeral_notation_obj + +type prim_token_infos = { + pt_local : bool; (** Is this interpretation local? *) + pt_scope : scope_name; (** Concerned scope *) + pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *) + pt_required : required_module; (** Module that should be loaded first *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} + +(** Note: most of the time, the [pt_refs] field above will contain + inductive constructors (e.g. O and S for nat). But it could also be + injection functions such as IZR for reals. *) + +(** Activate a prim token interpretation whose unique id and functions + have already been registered. *) + +val enable_prim_token_interpretation : prim_token_infos -> unit + +(** Compatibility. + Avoid the next two functions, they will now store unnecessary + objects in the library segment. Instead, combine + [register_*_interpretation] and [enable_prim_token_interpretation] + (the latter inside a [Mltop.declare_cache_obj]). +*) + +val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module -> + Bigint.bigint prim_token_interpreter -> + glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit +val declare_string_interpreter : ?local:bool -> scope_name -> required_module -> + string prim_token_interpreter -> + glob_constr list * string prim_token_uninterpreter * bool -> unit (** Return the [term]/[cases_pattern] bound to a primitive token in a given scope context*) -val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes -> +val interp_prim_token : ?loc:Loc.t -> prim_token -> subscopes -> 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 -> - local_scopes -> glob_constr * (notation_location * scope_name option) +val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) -> prim_token -> + subscopes -> glob_constr * (notation_location * scope_name option) (** Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) @@ -101,11 +188,9 @@ val uninterp_prim_token : 'a glob_constr_g -> scope_name * prim_token val uninterp_prim_token_cases_pattern : 'a cases_pattern_g -> Name.t * scope_name * prim_token -val uninterp_prim_token_ind_pattern : - inductive -> cases_pattern list -> scope_name * prim_token val availability_of_prim_token : - prim_token -> scope_name -> local_scopes -> delimiters option option + prim_token -> scope_name -> subscopes -> delimiters option option (** {6 Declare and interpret back and forth a notation } *) @@ -120,7 +205,7 @@ val declare_notation_interpretation : notation -> scope_name option -> val declare_uninterpretation : interp_rule -> interpretation -> unit (** Return the interpretation bound to a notation *) -val interp_notation : ?loc:Loc.t -> notation -> local_scopes -> +val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) type notation_rule = interp_rule * interpretation * int option @@ -133,18 +218,13 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first argument is itself not None if a delimiters is needed *) -val availability_of_notation : scope_name option * notation -> local_scopes -> +val availability_of_notation : scope_name option * notation -> subscopes -> (scope_name option * delimiters option) option -(** {6 Declare and test the level of a (possibly uninterpreted) notation } *) - -val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit -val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *) - (** {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_key -> delimiters option -> GlobRef.t (** Checks for already existing notations *) val exists_notation_in_scope : scope_name option -> notation -> @@ -152,9 +232,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 +245,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 @@ -186,8 +266,8 @@ type symbol = val symbol_eq : symbol -> symbol -> bool (** Make/decompose a notation of the form "_ U _" *) -val make_notation_key : symbol list -> notation -val decompose_notation_key : notation -> symbol list +val make_notation_key : notation_entry_level -> symbol list -> notation +val decompose_notation_key : notation -> notation_entry_level * symbol list (** Decompose a notation of the form "a 'U' b" *) val decompose_raw_notation : string -> symbol list @@ -196,25 +276,20 @@ val decompose_raw_notation : string -> symbol list val pr_scope_class : scope_class -> Pp.t val pr_scope : (glob_constr -> Pp.t) -> scope_name -> Pp.t val pr_scopes : (glob_constr -> Pp.t) -> Pp.t -val locate_notation : (glob_constr -> Pp.t) -> notation -> +val locate_notation : (glob_constr -> Pp.t) -> notation_key -> scope_name option -> Pp.t val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t -(** {6 Printing rules for notations} *) +type entry_coercion = notation list +val declare_entry_coercion : notation -> notation_entry_level -> unit +val availability_of_entry_coercion : notation_entry_level -> notation_entry_level -> entry_coercion option -(** 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 +val declare_custom_entry_has_global : string -> int -> unit +val declare_custom_entry_has_ident : string -> int -> unit -(** Returns notations with defined parsing/printing rules *) -val get_defined_notations : unit -> notation list +val entry_has_global : notation_entry_level -> bool +val entry_has_ident : notation_entry_level -> bool (** Rem: printing rules for primitive token are canonical *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 55e532dc..7a525f84 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -13,9 +13,10 @@ open CErrors open Util open Names open Nameops +open Constr open Globnames open Decl_kinds -open Misctypes +open Namegen open Glob_term open Glob_ops open Mod_subst @@ -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 @@ -85,12 +86,12 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Array.equal (eq_notation_constr vars) us1 us2 && Array.equal (eq_notation_constr vars) rs1 rs2 | NSort s1, NSort s2 -> - Miscops.glob_sort_eq s1 s2 + glob_sort_eq s1 s2 | NCast (t1, c1), NCast (t2, c2) -> (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _), _ -> false + | NRec _ | NSort _ | NCast _ ), _ -> false (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) @@ -152,10 +153,12 @@ let protect g e na = if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern."); e',na -let apply_cases_pattern ?loc ((ids,disjpat),id) c = - let tm = DAst.make ?loc (GVar id) in +let apply_cases_pattern_term ?loc (ids,disjpat) tm c = let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in - DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqns) + DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns) + +let apply_cases_pattern ?loc (ids_disjpat,id) c = + apply_cases_pattern_term ?loc ids_disjpat (DAst.make ?loc (GVar id)) c let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let lt x = DAst.make ?loc x in lt @@ match nc with @@ -181,7 +184,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let e',disjpat,na = g e na in (match disjpat with | None -> GLetIn (na,f e b,Option.map (f e) t,f e' c) - | Some disjpat -> DAst.get (apply_cases_pattern ?loc disjpat (f e' c))) + | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c))) | NCases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with @@ -213,7 +216,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = (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 GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k) + | NCast (c,k) -> GCast (f e c,map_cast_type (f e) k) | NSort x -> GSort x | NHole (x, naming, arg) -> GHole (x, naming, arg) | NRef x -> GRef (x,None) @@ -430,7 +433,7 @@ let notation_constr_and_vars_of_glob_constr recvars a = user_err Pp.(str "Binders marked as implicit not allowed in notations."); add_name found na; (na,Option.map aux oc,aux b))) dll in NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) - | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k) + | GCast (c,k) -> NCast (aux c,map_cast_type aux k) | GSort s -> NSort s | GHole (w,naming,arg) -> if arg != None then has_ltac := true; @@ -505,7 +508,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; @@ -517,7 +522,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) @@ -532,7 +537,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') @@ -562,14 +567,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) -> @@ -577,9 +582,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')) @@ -590,14 +595,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 @@ -606,12 +611,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') @@ -624,13 +629,13 @@ 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) | NCast (r1,k) -> let r1' = subst_notation_constr subst bound r1 in - let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in + let k' = smartmap_cast_type (subst_notation_constr subst bound) k in if r1' == r1 && k' == k then raw else NCast(r1',k') let subst_interpretation subst (metas,pat) = @@ -651,11 +656,11 @@ let abstract_return_type_context pi mklam tml rtno = let abstract_return_type_context_glob_constr tml rtn = abstract_return_type_context (fun {CAst.v=(_,nal)} -> nal) (fun na c -> DAst.make @@ - GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn + GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,IntroAnonymous,None),c)) tml rtn let abstract_return_type_context_notation_constr tml rtn = abstract_return_type_context snd - (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) tml rtn + (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn let is_term_meta id metas = try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false @@ -672,7 +677,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 @@ -887,7 +892,9 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) | GVar id' -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), sigma - | _ -> anomaly (str "A term which can be a binder has to be a variable.") + | t -> + (* The term is a non-variable pattern *) + raise No_match with Not_found -> (* The matching against a term allowing to find the instance has not been found yet *) (* If it will be a different name, we shall unfortunately fail *) @@ -995,9 +1002,9 @@ let remove_sigma x (terms,termlists,binders,binderlists) = let remove_bindinglist_sigma x (terms,termlists,binders,binderlists) = (terms,termlists,binders,Id.List.remove_assoc x binderlists) -let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas +let add_ldots_var metas = (ldots_var,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas -let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas +let add_meta_bindinglist x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeBinderList))::metas (* This tells if letins in the middle of binders should be included in the sequence of binders *) @@ -1042,7 +1049,7 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert = let alp,sigma = bind_bindinglist_env alp sigma x bl in match_fun alp metas sigma rest termin -let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas +let add_meta_term x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *) let match_termlist match_fun alp metas sigma rest x y iter termin revert = let rec aux sigma acc rest = @@ -1111,7 +1118,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 = @@ -1179,7 +1186,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | GCast(t1, c1), NCast(t2, c2) -> match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2 | GSort (GType _), NSort (GType _) when not u -> sigma - | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma + | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, NHole _ -> sigma @@ -1193,7 +1200,7 @@ let rec match_ inner u alp metas sigma a1 a2 = let avoid = Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in let id' = Namegen.next_ident_away id avoid in - let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in + let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma | NVar id2 -> bind_term_env alp sigma id2 t1 @@ -1207,7 +1214,7 @@ let rec match_ inner u alp metas sigma a1 a2 = | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ - | GCast _), _ -> raise No_match + | GCast _ ), _ -> raise No_match and match_in u = match_ true u @@ -1223,7 +1230,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = let store, get = set_temporary_memory () in match na1, DAst.get b1, na2 with (* Matching individual binders as part of a recursive pattern *) - | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id + | Name p, GCases (Constr.LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id when is_gvar p e && is_bindinglist_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> (match get () with | [{CAst.v=(ids,disj_of_patl,b1)}] -> diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index f038b5be..58fa221b 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -53,18 +53,18 @@ val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_const exception No_match val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> - ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list * - ('a cases_pattern_disjunction_g * subscopes) list * - ('a extended_glob_local_binder_g list * subscopes) list + ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list * + ('a cases_pattern_disjunction_g * extended_subscopes) list * + ('a extended_glob_local_binder_g list * extended_subscopes) list val match_notation_constr_cases_pattern : 'a cases_pattern_g -> interpretation -> - (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) * + (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) * (int * 'a cases_pattern_g list) val match_notation_constr_ind_pattern : inductive -> 'a cases_pattern_g list -> interpretation -> - (('a cases_pattern_g * subscopes) list * ('a cases_pattern_g list * subscopes) list) * + (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) * (int * 'a cases_pattern_g list) (** {5 Matching a notation pattern against a [glob_constr]} *) diff --git a/interp/notation_term.ml b/interp/notation_term.ml new file mode 100644 index 00000000..5fb0ca1b --- /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 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 * Namegen.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 + +(** 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 extended_subscopes = Constrexpr.notation_entry_level * subscopes + +(** 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 * (extended_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 c75d9e12..00000000 --- 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 00000000..b9a74136 --- /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 c81058e7..7254f29b 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 36005121..071248f0 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/reserve.mli b/interp/reserve.mli index daee5863..a10858e7 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -11,5 +11,5 @@ open Names open Notation_term -val declare_reserved_type : Misctypes.lident list -> notation_constr -> unit +val declare_reserved_type : lident list -> notation_constr -> unit val find_reserved_type : Id.t -> notation_constr diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 1f4a93a6..91491bdf 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -18,7 +18,6 @@ open Pp open CErrors open Libnames open Globnames -open Misctypes open Syntax_def open Notation_term @@ -42,36 +41,34 @@ let global_of_extended_global = function | [],NApp (NRef ref,[]) -> ref | _ -> raise Not_found -let locate_global_with_alias ?(head=false) {CAst.loc; v=qid} = +let locate_global_with_alias ?(head=false) qid = let ref = Nametab.locate_extended qid in try if head then global_of_extended_global_head ref else global_of_extended_global ref with Not_found -> - user_err ?loc (pr_qualid qid ++ + user_err ?loc:qid.CAst.loc (pr_qualid qid ++ str " is bound to a notation that does not denote a reference.") -let global_inductive_with_alias ({CAst.loc} as lr) = - let qid = qualid_of_reference lr in +let global_inductive_with_alias qid = try match locate_global_with_alias qid with | IndRef ind -> ind | ref -> - user_err ?loc ~hdr:"global_inductive" - (pr_reference lr ++ spc () ++ str "is not an inductive type.") + user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" + (pr_qualid qid ++ spc () ++ str "is not an inductive type.") with Not_found -> Nametab.error_global_not_found qid -let global_with_alias ?head r = - let qid = qualid_of_reference r in +let global_with_alias ?head qid = try locate_global_with_alias ?head qid with Not_found -> Nametab.error_global_not_found qid -let smart_global ?head = CAst.with_loc_val (fun ?loc -> function +let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function | AN r -> global_with_alias ?head r | ByNotation (ntn,sc) -> Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc) -let smart_global_inductive = CAst.with_loc_val (fun ?loc -> function +let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function | AN r -> global_inductive_with_alias r | ByNotation (ntn,sc) -> diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 7ff7e899..e41ef789 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -11,29 +11,28 @@ open Names open Libnames open Globnames -open Misctypes (** [locate_global_with_alias] locates global reference possibly following a notation if this notation has a role of aliasing; raise [Not_found] 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 -> 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 -> qualid -> GlobRef.t (** The same for inductive types *) -val global_inductive_with_alias : reference -> inductive +val global_inductive_with_alias : qualid -> 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 -> qualid Constrexpr.or_by_notation -> GlobRef.t (** The same for inductive types *) -val smart_global_inductive : reference or_by_notation -> inductive +val smart_global_inductive : qualid Constrexpr.or_by_notation -> inductive diff --git a/interp/stdarg.ml b/interp/stdarg.ml index e5ed58be..7b01b6dc 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -11,6 +11,8 @@ open Genarg open Geninterp +type 'a and_short_name = 'a * Names.lident option + let make0 ?dyn name = let wit = Genarg.make0 name in let () = register_val0 wit dyn in @@ -34,9 +36,6 @@ let wit_pre_ident : string uniform_genarg_type = let wit_int_or_var = make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var" -let wit_intro_pattern = - make0 "intropattern" - let wit_ident = make0 "ident" @@ -45,8 +44,6 @@ let wit_var = let wit_ref = make0 "ref" -let wit_quant_hyp = make0 "quant_hyp" - let wit_sort_family = make0 "sort_family" let wit_constr = @@ -56,12 +53,6 @@ let wit_uconstr = make0 "uconstr" let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" -let wit_constr_with_bindings = make0 "constr_with_bindings" - -let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" - -let wit_bindings = make0 "bindings" - let wit_red_expr = make0 "redexpr" let wit_clause_dft_concl = @@ -74,6 +65,4 @@ let wit_preident = wit_pre_ident let wit_reference = wit_ref let wit_global = wit_ref let wit_clause = wit_clause_dft_concl -let wit_quantified_hypothesis = wit_quant_hyp -let wit_intropattern = wit_intro_pattern let wit_redexpr = wit_red_expr diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 53d1a522..5e5e43ed 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -14,13 +14,14 @@ open Loc open Names open EConstr open Libnames -open Globnames open Genredexpr open Pattern open Constrexpr -open Misctypes -open Tactypes open Genarg +open Genintern +open Locus + +type 'a and_short_name = 'a * lident option val wit_unit : unit uniform_genarg_type @@ -36,15 +37,11 @@ val wit_pre_ident : string uniform_genarg_type val wit_int_or_var : (int or_var, int or_var, int) genarg_type -val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type - 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_quant_hyp : quantified_hypothesis uniform_genarg_type +val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_sort_family : (Sorts.family, unit, unit) genarg_type @@ -55,23 +52,8 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_ val wit_open_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_constr_with_bindings : - (constr_expr with_bindings, - glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type - -val wit_open_constr_with_bindings : - (constr_expr with_bindings, - glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type - -val wit_bindings : - (constr_expr bindings, - glob_constr_and_expr bindings, - constr bindings delayed_open) genarg_type - val wit_red_expr : - ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type @@ -81,12 +63,10 @@ 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 : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_global : (qualid, 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 val wit_redexpr : - ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index a4f20fd7..e3d490a1 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -77,8 +77,8 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr (* Coercions to the general format of notation that also supports variables bound to list of expressions *) -let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,(sc,NtnTypeConstr))) ids,ac) -let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac) +let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac) +let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () diff --git a/interp/tactypes.ml b/interp/tactypes.ml deleted file mode 100644 index 83e42be8..00000000 --- a/interp/tactypes.ml +++ /dev/null @@ -1,34 +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) *) -(************************************************************************) - -(** Tactic-related types that are not totally Ltac specific and still used in - lower API. It's not clear whether this is a temporary API or if this is - meant to stay. *) - -open Names -open Constrexpr -open Pattern -open Misctypes - -(** In globalize tactics, we need to keep the initial [constr_expr] to recompute - in the environment by the effective calls to Intro, Inversion, etc - The [constr_expr] field is [None] in TacDef though *) -type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option -type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern - -type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr = EConstr.constr delayed_open -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t -type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list -type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = intro_pattern_naming_expr CAst.t diff --git a/interp/topconstr.ml b/interp/topconstr.ml deleted file mode 100644 index 7d2d75d9..00000000 --- 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 c8650201..00000000 --- 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"] |