diff options
Diffstat (limited to 'interp')
42 files changed, 2407 insertions, 1409 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml new file mode 100644 index 0000000000..77d612cfd9 --- /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 4ee13c961f..3a4969a3ee 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 @@ -176,12 +177,10 @@ let rec constr_expr_eq e1 e2 = | CDelimiters(s1,e1), CDelimiters(s2,e2) -> String.equal s1 s2 && constr_expr_eq e1 e2 - | CProj(p1,c1), CProj(p2,c2) -> - eq_reference p1 p2 && constr_expr_eq c1 c2 | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _ | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _ | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _ - | CGeneralization _ | CDelimiters _ | CProj _), _ -> false + | CGeneralization _ | CDelimiters _ ), _ -> false and args_eq (a1,e1) (a2,e2) = Option.equal (eq_ast explicitation_eq) e1 e2 && @@ -279,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" @@ -356,13 +357,13 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (_,_) -> Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc - | CProj (_,c) -> - f n acc c ) 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 @@ -395,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, @@ -434,16 +435,16 @@ let map_constr_expr_with_binders g f e = CAst.map (function let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in let d' = f e'' d in (id,bl',t',d')) dl) - | CProj (p,c) -> - CProj (p, f e c) ) (* 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) *) @@ -512,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,27 +526,37 @@ let mkAppC (f,l) = | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l) | _ -> CAst.make @@ CApp ((None, f), l) +let mkProdCN ?loc bll c = + if bll = [] then c else + CAst.make ?loc @@ CProdN (bll,c) + +let mkLambdaCN ?loc bll c = + if bll = [] then c else + CAst.make ?loc @@ CLambdaN (bll,c) + let mkCProdN ?loc bll c = CAst.make ?loc @@ CProdN (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.") @@ -569,9 +580,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 @@ -592,16 +604,34 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr" (str "This expression should be coercible to a pattern.")) c -let asymmetric_patterns = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "no parameters in constructors"; - Goptions.optkey = ["Asymmetric";"Patterns"]; - Goptions.optread = (fun () -> !asymmetric_patterns); - Goptions.optwrite = (fun a -> asymmetric_patterns:=a); -} - -(************************************************************************) -(* Deprecated *) -let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c -let prod_constr_expr c bl = mkCProdN ?loc:(local_binders_loc bl) bl c +(** Local universe and constraint declarations. *) + +let interp_univ_constraints env evd cstrs = + let interp (evd,cstrs) (u, d, u') = + let ul = Pretyping.interp_known_glob_level evd u in + let u'l = Pretyping.interp_known_glob_level evd u' in + let cstr = (ul,d,u'l) in + let cstrs' = Univ.Constraint.add cstr cstrs in + try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in + evd, cstrs' + with Univ.UniverseInconsistency e -> + CErrors.user_err ~hdr:"interp_constraint" + (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e) + in + List.fold_left interp (evd,Univ.Constraint.empty) cstrs + +let interp_univ_decl env decl = + let open UState in + let pl : lident list = decl.univdecl_instance in + let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in + let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in + let decl = { univdecl_instance = pl; + univdecl_extensible_instance = decl.univdecl_extensible_instance; + univdecl_constraints = cstrs; + univdecl_extensible_constraints = decl.univdecl_extensible_constraints } + in evd, decl + +let interp_univ_decl_opt env l = + match l with + | None -> Evd.from_env env, UState.default_univ_decl + | Some decl -> interp_univ_decl env decl diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index d038bd71ab..7f14eb4583 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] *) @@ -39,38 +38,44 @@ val constr_loc : constr_expr -> Loc.t option val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t option val local_binders_loc : local_binder_expr list -> Loc.t option -(** {6 Constructors}*) +(** {6 Constructors} *) + +(** {7 Term constructors} *) + +(** Basic form of the corresponding constructors *) val mkIdentC : Id.t -> constr_expr -val mkRefC : reference -> constr_expr -val mkAppC : constr_expr * constr_expr list -> constr_expr -val mkCastC : constr_expr * constr_expr cast_type -> constr_expr +val mkRefC : qualid -> 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 -val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr -(** Same as [abstract_constr_expr], with location *) +val mkAppC : constr_expr * constr_expr list -> constr_expr +(** Basic form of application, collapsing nested applications *) + +(** Optimized constructors: does not add a constructor for an empty binder list *) + +val mkLambdaCN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr +val mkProdCN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr +(** Aliases for the corresponding constructors; generally [mkLambdaCN] and + [mkProdCN] should be preferred *) + +val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr -(** Same as [prod_constr_expr], with location *) +(** {7 Pattern constructors} *) + +(** Interpretation of a list of patterns as a disjunctive pattern (optimized) *) 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 +121,15 @@ 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 48ddd94961..25f2526f74 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -17,6 +17,7 @@ open Nameops open Termops open Libnames open Globnames +open Namegen open Impargs open CAst open Constrexpr @@ -25,10 +26,8 @@ open Notation_ops open Glob_term open Glob_ops open Pattern -open Nametab open Notation open Detyping -open Misctypes open Decl_kinds module NamedDecl = Context.Named.Declaration @@ -101,8 +100,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 = @@ -113,14 +112,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 @@ -131,12 +130,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.") @@ -193,17 +193,12 @@ let without_specific_symbols l = (* Control printing of records *) (* Set Record Printing flag *) -let record_print = ref true - -let _ = - let open Goptions in - declare_bool_option - { optdepr = false; - optname = "record printing"; - optkey = ["Printing";"Records"]; - optread = (fun () -> !record_print); - optwrite = (fun b -> record_print := b) } - +let get_record_print = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"record printing" + ~key:["Printing";"Records"] + ~value:true let is_record indsp = try @@ -212,7 +207,7 @@ let is_record indsp = with Not_found -> false let encode_record r = - let indsp = global_inductive r in + let indsp = Nametab.global_inductive r in if not (is_record indsp) then user_err ?loc:r.CAst.loc ~hdr:"encode_record" (str "This type is not a structure type."); @@ -260,6 +255,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 *) @@ -270,7 +273,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) + Nametab.shortest_qualid_of_global ?loc vars r let my_extern_reference = ref default_extern_reference @@ -325,16 +328,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) @@ -367,31 +370,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; @@ -415,7 +426,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = with Not_found | No_match | Exit -> let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in - if !asymmetric_patterns then + if Constrintern.get_asymmetric_patterns () then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) @@ -424,66 +435,77 @@ 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 - let l2' = if !asymmetric_patterns || not (List.is_empty ll) then l2 + let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2 else match drop_implicits_in_patt gr nb_to_drop l2 with |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 = Nametab.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 + let l2' = if Constrintern.get_asymmetric_patterns () then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_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 if is_inactive_rule keyrule then raise No_match; let loc = t.loc in match DAst.get t with - | PatCstr (cstr,_,na) -> + | PatCstr (cstr,args,na) -> + let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in let p = apply_notation_to_pattern ?loc (ConstructRef cstr) (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na | 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 @@ -497,35 +519,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 *) @@ -589,11 +603,17 @@ let explicitize inctx impl (cf,f) args = let expl () = match ip with | Some i -> - if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then - raise Expl + (* Careful: It is possible to have declared implicits ending + before the principal argument *) + let is_impl = + try is_status_implicit (List.nth impl (i-1)) + with Failure _ -> false + in + if is_impl + then raise Expl else let (args1,args2) = List.chop i args in - let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in + let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in let args1 = exprec 1 (args1,impl1) in let args2 = exprec (i+1) (args2,impl2) in let ip = Some (List.length args1) in @@ -633,12 +653,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 @@ -690,18 +710,21 @@ 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 = - try - let (sc,n) = uninterp_prim_token r in - 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) - with No_match -> - None - -let extern_optimal_prim_token scopes r r' = - let c = extern_possible_prim_token scopes r in - let c' = if r==r' then None else extern_possible_prim_token scopes r' in +let extern_possible_prim_token (custom,scopes) r = + 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 -> raise No_match + | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) + +let extern_possible extern r = + try Some (extern r) with No_match -> None + +let extern_optimal extern r r' = + let c = extern_possible extern r in + let c' = if r==r' then None else extern_possible extern r' in match c,c' with | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n | _ -> raise No_match @@ -713,7 +736,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) @@ -730,31 +753,54 @@ 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 if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal_prim_token scopes r r' + extern_optimal (extern_possible_prim_token scopes) r r' with No_match -> try 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) + extern_optimal + (fun r -> extern_notation scopes vars r (uninterp_notations r)) + r r'' + 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) - | GVar id -> CRef (make ?loc @@ Ident id,None) + | c -> - | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None) + match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> + + 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,[])) @@ -763,7 +809,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; @@ -773,7 +819,7 @@ let rec extern inctx scopes vars r = () else if PrintingConstructor.active (fst cstrsp) then raise Exit - else if not !record_print then + else if not (get_record_print ()) then raise Exit; let projs = struc.Recordops.s_PROJ in let locals = struc.Recordops.s_PROJKIND in @@ -910,21 +956,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') - | GProj (p, c) -> - let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in - CProj (pr, sub_extern inctx 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)}] -> @@ -952,7 +996,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)}] -> @@ -1012,7 +1056,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 @@ -1059,40 +1103,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 (Nametab.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 @@ -1106,10 +1156,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 *) @@ -1125,7 +1175,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 @@ -1146,14 +1196,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 @@ -1177,7 +1227,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]) @@ -1202,7 +1252,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) -> @@ -1221,7 +1271,7 @@ 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) + 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 @@ -1255,10 +1305,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | 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 8ab70283c8..f09b316cd6 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 f2cd07c94e..6313f2d7ba 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 @@ -27,7 +28,6 @@ open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops -open Nametab open Notation open Inductiveops open Decl_kinds @@ -95,8 +95,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,10 +116,13 @@ 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 + | NotAProjection of qualid + | NotAProjectionOf of qualid * qualid + | ProjectionsOfDifferentRecords of qualid * qualid exception InternalizationError of internalization_error Loc.located @@ -130,8 +133,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 ++ @@ -145,6 +148,16 @@ let explain_bad_patterns_number n1 n2 = str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ str " but found " ++ int n2 +let explain_field_not_a_projection field_id = + pr_qualid field_id ++ str ": Not a projection" + +let explain_field_not_a_projection_of field_id inductive_id = + pr_qualid field_id ++ str ": Not a projection of inductive " ++ pr_qualid inductive_id + +let explain_projections_of_diff_records inductive1_id inductive2_id = + str "This record contains fields of both " ++ pr_qualid inductive1_id ++ + str " and " ++ pr_qualid inductive2_id + let explain_internalization_error e = let pp = match e with | VariableCapture (id,id') -> explain_variable_capture id id' @@ -153,6 +166,11 @@ let explain_internalization_error e = | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id | NonLinearPattern id -> explain_non_linear_pattern id | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 + | NotAProjection field_id -> explain_field_not_a_projection field_id + | NotAProjectionOf (field_id, inductive_id) -> + explain_field_not_a_projection_of field_id inductive_id + | ProjectionsOfDifferentRecords (inductive1_id, inductive2_id) -> + explain_projections_of_diff_records inductive1_id inductive2_id in pp ++ str "." let error_bad_inductive_type ?loc = @@ -217,30 +235,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 +417,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 +427,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,10 +455,10 @@ 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.") + Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") ) let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd") @@ -471,7 +496,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 +526,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 +550,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 +575,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 +589,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 +631,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 +647,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 (Nametab.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 +733,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, None) map + with Nametab.GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -722,7 +750,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 +833,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 +842,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 +870,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 +889,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 +930,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,36 +997,38 @@ 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 + with Not_found -> Nametab.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 qid intern env ntnvars us args = +let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in match intern_extended_global_of_qualid qid with + | TrueGlobal (VarRef _) when no_secvar -> + (* Rule out section vars since these should have been found by intern_var *) + raise Not_found | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> - let (ids,c) = Syntax_def.search_syntactic_definition sp in + let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments ?loc; let args1,args2 = List.chop nids args in @@ -1010,7 +1040,7 @@ let intern_qualid 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 @@ -1024,44 +1054,35 @@ let intern_qualid qid intern env ntnvars us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end - | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) - user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v) + user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) | Some _, _ -> err () in c, projapp, args2 -(* Rule out section vars since these should have been found by intern_var *) -let intern_non_secvar_qualid qid intern env ntnvars us args = - let c, _, _ as r = intern_qualid qid intern env ntnvars us args in - match DAst.get c with - | GRef (VarRef _, _) -> raise Not_found - | _ -> r - -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_non_secvar_qualid qid intern env ntnvars us args in + 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 - else error_global_not_found qid + (* Extra allowance for non globalizing functions *) + if !interning_grammar || env.unb then + (gvar (loc,qualid_basename qid) us, [], [], []), args + else Nametab.error_global_not_found qid + else + let r,projapp,args2 = + try intern_qualid qid intern env ntnvars us args + with Not_found -> Nametab.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,_,_,_),_ = @@ -1076,11 +1097,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 @@ -1140,9 +1161,18 @@ let check_number_of_pattern loc n l = if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = - if List.exists (fun ids' -> not (List.eq_set (fun {loc;v=id} {v=id'} -> Id.equal id id') ids ids')) idsl then - user_err ?loc (str - "The components of this disjunctive pattern must bind the same variables.") + let eq_id {v=id} {v=id'} = Id.equal id id' in + (* Collect remaining patterns which do not have the same variables as the first pattern *) + let idsl = List.filter (fun ids' -> not (List.eq_set eq_id ids ids')) idsl in + match idsl with + | ids'::_ -> + (* Look for an [id] which is either in [ids] and not in [ids'] or in [ids'] and not in [ids] *) + let ids'' = List.subtract eq_id ids ids' in + let ids'' = if ids'' = [] then List.subtract eq_id ids' ids else ids'' in + user_err ?loc + (strbrk "The components of this disjunctive pattern must bind the same variables (" ++ + Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).") + | [] -> () (** Use only when params were NOT asked to the user. @return if letin are included *) @@ -1256,18 +1286,22 @@ 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 ".") + +let inductive_of_record loc record = + let inductive = IndRef (inductive_of_constructor record.Recordops.s_CONST) in + Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive (** [sort_fields ~complete loc fields completer] expects a list [fields] of field assignments [f = e1; g = e2; ...], where [f, g] @@ -1291,15 +1325,14 @@ let sort_fields ~complete loc fields completer = let gr = global_reference_of_reference first_field_ref in (gr, Recordops.find_projection gr) with Not_found -> - user_err ?loc ~hdr:"intern" - (pr_reference first_field_ref ++ str": Not a projection") + raise (InternalizationError(loc, NotAProjection first_field_ref)) 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 Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in @@ -1307,14 +1340,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 -> @@ -1350,20 +1383,27 @@ 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 this_field_record = try Recordops.find_projection field_glob_ref + with Not_found -> + let inductive_ref = inductive_of_record loc record in + raise (InternalizationError(loc, NotAProjectionOf (field_ref, inductive_ref))) + 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 - (str "This record contains fields of different records.") + let ind1 = inductive_of_record loc record in + let ind2 = inductive_of_record loc this_field_record in + raise (InternalizationError(loc, ProjectionsOfDifferentRecords (ind1, ind2))) in index_fields fields remaining_projs ((field_index, field_value) :: acc) | [] -> (* 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 @@ -1379,7 +1419,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; } @@ -1448,6 +1488,12 @@ let is_non_zero_pat c = match c with | { CAst.v = CPatPrim (Numeral (p, true)) } -> not (is_zero p) | _ -> false +let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"no parameters in constructors" + ~key:["Asymmetric";"Patterns"] + ~value:false + let drop_notations_pattern looked_for genv = (* At toplevel, Constructors and Inductives are accepted, in recursive calls only constructor are allowed *) @@ -1477,10 +1523,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 Nametab.locate_extended qid with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with @@ -1518,12 +1563,12 @@ 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) -> let pl = - if !asymmetric_patterns then pl else + if get_asymmetric_patterns () then pl else let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in List.rev_append pars pl in match drop_syndef top scopes head pl with @@ -1536,10 +1581,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 Nametab.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, []) @@ -1548,11 +1593,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 @@ -1645,7 +1690,7 @@ let rec intern_pat genv ntnvars aliases pat = let aliases' = merge_aliases aliases id in intern_pat genv ntnvars aliases' p | RCPatCstr (head, expl_pl, pl) -> - if !asymmetric_patterns then + if get_asymmetric_patterns () then let len = if List.is_empty expl_pl then Some (List.length pl) else None in let c,idslpl1 = find_constructor loc len head in let with_letin = @@ -1719,15 +1764,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 = @@ -1850,12 +1895,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = Array.map (fun (bl,_,_) -> bl) idl, Array.map (fun (_,ty,_) -> ty) idl, Array.map (fun (_,_,bd) -> bd) idl) + | CProdN ([],c2) -> anomaly (Pp.str "The AST is malformed, found prod without binders.") | CProdN (bl,c2) -> let (env',bl) = List.fold_left intern_local_binder (env,[]) bl in expand_binders ?loc mkGProd bl (intern_type env' c2) - | CLambdaN ([],c2) -> - (* Such a term is built sometimes: it should not change scope *) - intern env c2 + | CLambdaN ([],c2) -> anomaly (Pp.str "The AST is malformed, found lambda without binders.") | CLambdaN (bl,c2) -> let (env',bl) = List.fold_left intern_local_binder (reset_tmp_scope env,[]) bl in expand_binders ?loc mkGLambda bl (intern env' c2) @@ -1865,10 +1909,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) -> @@ -1884,9 +1928,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 @@ -1912,14 +1956,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 @@ -1959,13 +2011,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 @@ @@ -1995,8 +2047,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 @@ -2005,15 +2057,22 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let (ltacvars, ntnvars) = lvar in (* Preventively declare notation variables in ltac as non-bindings *) Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars; - let ntnvars = Id.Map.domain ntnvars in let extra = ltacvars.ltac_extra in + (* We inform ltac that the interning vars and the notation vars are bound *) + (* but we could instead rely on the "intern_sign" *) let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in - let lvars = Id.Set.union lvars ntnvars in + let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in let ltacvars = Id.Set.union lvars env.ids in + (* Propagating enough information for mutual interning with tac-in-term *) + let intern_sign = { + Genintern.intern_ids = env.ids; + Genintern.notation_variable_status = ntnvars + } in let ist = { Genintern.genv = globalenv; ltacvars; extra; + intern_sign; } in let (_, glb) = Genintern.generic_intern ist gen in Some glb @@ -2040,13 +2099,7 @@ 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) - | CProj (pr, c) -> - match intern_reference pr with - | ConstRef p -> - DAst.make ?loc @@ GProj (Projection.make p false, intern env c) - | _ -> - raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *) + GCast (intern env c1, map_cast_type (intern_type env) c2) ) and intern_type env = intern (set_type_scope env) @@ -2304,16 +2357,23 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) ~pattern_mode:true ~ltacvars env sigma c in pattern_of_glob_constr c +let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) + { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = + let tmp_scope = scope_of_type_kind sigma kind in + let impls = empty_internalization_env in + internalize env {ids; unb = false; tmp_scope; scopes = []; impls} + pattern_mode (ltacvars, vl) c + let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = + let ids = extract_ids env in (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in - let c = internalize (Global.env()) {ids = extract_ids env; unb = false; - tmp_scope = None; scopes = []; impls = impls} + let c = internalize env {ids; unb = false; tmp_scope = None; scopes = []; impls} false (empty_ltac_sign, vl) a in + (* Splits variables into those that are binding, bound, or both *) (* Translate and check that [c] has all its free variables bound in [vars] *) let a, reversible = notation_constr_of_glob_constr nenv c in - (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in let unused = match reversible with NonInjective ids -> ids | _ -> [] in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index f5e32dc4cd..035e4bc644 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. *) @@ -187,8 +185,18 @@ val interp_notation_constr : env -> ?impls:internalization_env -> notation_interp_env -> constr_expr -> (bool * subscopes) Id.Map.t * notation_constr * reversibility_status +(** Idem but to glob_constr (weaker check of binders) *) + +val intern_core : typing_constraint -> + env -> evar_map -> ?pattern_mode:bool -> ?ltacvars:ltac_sign -> + Genintern.intern_variable_status -> constr_expr -> + glob_constr + (** Globalization options *) val parsing_explicit : bool ref (** Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b + +(** Placeholder for global option, should be moved to a parameter *) +val get_asymmetric_patterns : unit -> bool diff --git a/interp/declare.ml b/interp/declare.ml index c55a6c69ba..1e972d3e35 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -39,7 +39,6 @@ type constant_obj = { cst_decl : global_declaration option; (** [None] when the declaration is a side-effect and has already been defined in the global environment. *) - cst_hyps : Dischargedhypsmap.discharged_hyps; cst_kind : logical_kind; cst_locl : bool; } @@ -61,14 +60,7 @@ let open_constant i ((sp,kn), obj) = if obj.cst_locl then () else let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con); - match (Global.lookup_constant con).const_body with - | (Def _ | Undef _) -> () - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with - | Some f when Future.is_val f -> - Global.push_context_set false (Future.force f) - | _ -> () + Nametab.push (Nametab.Exactly i) sp (ConstRef con) let exists_name id = variable_exists id || Global.exists_objlabel (Label.of_id id) @@ -79,7 +71,6 @@ let check_exists sp = let cache_constant ((sp,kn), obj) = let id = basename sp in - let _,dir,_ = KerName.repr kn in let kn' = match obj.cst_decl with | None -> @@ -88,34 +79,26 @@ let cache_constant ((sp,kn), obj) = else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".") | Some decl -> let () = check_exists sp in - Global.add_constant dir id decl + Global.add_constant ~in_section:(Lib.sections_are_opened ()) id decl in assert (Constant.equal kn' (Constant.make1 kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); let cst = Global.lookup_constant kn' in add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (Constant.make1 kn) obj.cst_kind -let discharged_hyps kn sechyps = - let (_,dir,_) = KerName.repr kn in - let args = Array.to_list (instance_from_variable_context sechyps) in - List.rev_map (Libnames.make_path dir) args - let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in let from = Global.lookup_constant con in let modlist = replacement_context () in let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in - let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in let abstract = (named_of_variable_context hyps, subst, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in - Some { obj with cst_hyps = new_hyps; cst_decl = Some new_decl; } + Some { obj with cst_decl = Some new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant cst = { cst_decl = None; - cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; } @@ -142,16 +125,15 @@ let update_tables c = let register_side_effect (c, role) = let o = inConstant { cst_decl = None; - cst_hyps = [] ; cst_kind = IsProof Theorem; cst_locl = false; } in - let id = Label.to_id (pi3 (Constant.repr3 c)) in + let id = Label.to_id (Constant.label c) in 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 @@ -194,7 +176,6 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let () = List.iter register_side_effect export in let cst = { cst_decl = Some decl; - cst_hyps = [] ; cst_kind = kind; cst_locl = local; } in @@ -238,7 +219,7 @@ let cache_variable ((sp,_),o) = let (body, uctx), () = Future.force de.const_entry_body in let poly, univs = match de.const_entry_universes with | Monomorphic_const_entry uctx -> false, uctx - | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx + | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in let univs = Univ.ContextSet.union uctx univs in (** We must declare the universe constraints before type-checking the @@ -255,7 +236,6 @@ let cache_variable ((sp,_),o) = poly, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl poly ctx; - Dischargedhypsmap.set_discharged_hyps sp []; add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with @@ -311,34 +291,30 @@ let inductive_names sp kn mie = ([], 0) mie.mind_entry_inds in names -let load_inductive i ((sp,kn),(_,mie)) = +let load_inductive i ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names -let open_inductive i ((sp,kn),(_,mie)) = +let open_inductive i ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names -let cache_inductive ((sp,kn),(dhyps,mie)) = +let cache_inductive ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter check_exists (List.map fst names); let id = basename sp in - let _,dir,_ = KerName.repr kn in - let kn' = Global.add_mind dir id mie in + let kn' = Global.add_mind id mie in assert (MutInd.equal kn' (MutInd.make1 kn)); let mind = Global.lookup_mind kn' in add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; - Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names -let discharge_inductive ((sp,kn),(dhyps,mie)) = +let discharge_inductive ((sp,kn),mie) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in let info = section_segment_of_mutual_inductive mind in - let sechyps = info.Lib.abstr_ctx in - Some (discharged_hyps kn sechyps, - Discharge.process_inductive info repl mie) + Some (Discharge.process_inductive info repl mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; @@ -349,30 +325,28 @@ let dummy_one_inductive_entry mie = { } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry (_,m) = ([],{ +let dummy_inductive_entry m = { mind_entry_params = []; mind_entry_record = None; mind_entry_finite = Declarations.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; mind_entry_private = None; -}) +} (* reinfer subtyping constraints for inductive after section is dischared. *) -let infer_inductive_subtyping (pth, mind_ent) = +let infer_inductive_subtyping mind_ent = match mind_ent.mind_entry_universes with | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> - (pth, mind_ent) - | Cumulative_ind_entry cumi -> + mind_ent + | Cumulative_ind_entry (_, cumi) -> begin let env = Global.env () in (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) - (pth, InferCumulativity.infer_inductive env mind_ent) + InferCumulativity.infer_inductive env mind_ent end -type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry - -let inInductive : inductive_obj -> obj = +let inInductive : mutual_inductive_entry -> obj = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; @@ -382,28 +356,52 @@ 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 univs = match univs with + | Monomorphic_ind_entry _ -> + (** Global constraints already defined through the inductive *) + Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_ind_entry (nas, ctx) -> + Polymorphic_const_entry (nas, ctx) + | Cumulative_ind_entry (nas, ctx) -> + Polymorphic_const_entry (nas, 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 + let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in + let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in + Recordops.declare_primitive_projection p cst + + +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 = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in - let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) 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 +444,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 @@ -475,85 +469,69 @@ type universe_source = | QualifiedUniv of Id.t (* global universe introduced by some global value *) | UnqualifiedUniv (* other global universe *) -type universe_decl = universe_source * Nametab.universe_id - -let add_universe src (dp, i) = - let level = Univ.Level.make dp i in - let optpoly = match src with - | BoundUniv -> Some true - | UnqualifiedUniv -> Some false - | QualifiedUniv _ -> None - in - 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; - if poly then Lib.add_section_context ctx) - optpoly +type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list let check_exists sp = - let depth = sections_depth () in - let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in if Nametab.exists_universe sp then alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists") else () -let qualify_univ src (sp,i as orig) = +let qualify_univ i dp src id = match src with - | BoundUniv | UnqualifiedUniv -> orig + | BoundUniv | UnqualifiedUniv -> + i, Libnames.make_path dp id | QualifiedUniv l -> - let sp0, id = Libnames.repr_path sp in - let sp0 = DirPath.repr sp0 in - Libnames.make_path (DirPath.make (l::sp0)) id, i+1 - -let cache_universe ((sp, _), (src, id)) = - let sp, i = qualify_univ src (sp,1) in - let () = check_exists sp in - let () = Nametab.push_universe (Nametab.Until i) sp id in - add_universe src id - -let load_universe i ((sp, _), (src, id)) = - let sp, i = qualify_univ src (sp,i) in - let () = Nametab.push_universe (Nametab.Until i) sp id in - add_universe src id - -let open_universe i ((sp, _), (src, id)) = - let sp, i = qualify_univ src (sp,i) in - let () = Nametab.push_universe (Nametab.Exactly i) sp id in - () - -let discharge_universe = function + let dp = DirPath.repr dp in + Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id + +let do_univ_name ~check i dp src (id,univ) = + let i, sp = qualify_univ i dp src id in + if check then check_exists sp; + Nametab.push_universe i sp univ + +let cache_univ_names ((sp, _), (src, univs)) = + let depth = sections_depth () in + let dp = pop_dirpath_n depth (dirpath sp) in + List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs + +let load_univ_names i ((sp, _), (src, univs)) = + List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs + +let open_univ_names i ((sp, _), (src, univs)) = + List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs + +let discharge_univ_names = function | _, (BoundUniv, _) -> None | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x -let input_universe : universe_decl -> Libobject.obj = +let input_univ_names : universe_name_decl -> Libobject.obj = declare_object { (default_object "Global universe name state") with - cache_function = cache_universe; - load_function = load_universe; - open_function = open_universe; - discharge_function = discharge_universe; + cache_function = cache_univ_names; + load_function = load_univ_names; + open_function = open_univ_names; + discharge_function = discharge_univ_names; subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a); classify_function = (fun a -> Substitute a) } let declare_univ_binders gr pl = if Global.is_polymorphic gr then - Universes.register_universe_binders gr pl + () else let l = match gr with | ConstRef c -> Label.to_id @@ Constant.label c | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> id + | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") | ConstructRef _ -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on an constructor reference") in - Id.Map.iter (fun id lvl -> - match Univ.Level.name lvl with - | None -> () - | Some na -> - ignore (Lib.add_leaf id (input_universe (QualifiedUniv l, na)))) - pl + let univs = Id.Map.fold (fun id univ univs -> + match Univ.Level.name univ with + | None -> assert false (* having Prop/Set/Var as binders is nonsense *) + | Some univ -> (id,univ)::univs) pl [] + in + Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) let do_universe poly l = let in_section = Lib.sections_are_opened () in @@ -564,38 +542,21 @@ 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 ctx = List.fold_left (fun ctx (_,(dp,i)) -> Univ.LSet.add (Univ.Level.make dp i) ctx) + Univ.LSet.empty l, Univ.Constraint.empty + in + let () = declare_universe_context poly ctx in let src = if poly then BoundUniv else UnqualifiedUniv in - List.iter (fun (id,lev) -> - 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) } + Lib.add_anonymous_leaf (input_univ_names (src, l)) 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 + Lib.is_polymorphic_univ level, level in let in_section = Lib.sections_are_opened () in let () = @@ -614,7 +575,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 084d746e68..468e056909 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Libnames open Constr open Entries open Decl_kinds @@ -29,7 +28,7 @@ type section_variable_entry = type variable_declaration = DirPath.t * section_variable_entry * logical_kind -val declare_variable : variable -> variable_declaration -> object_name +val declare_variable : variable -> variable_declaration -> Libobject.object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) @@ -69,7 +68,7 @@ val set_declare_scheme : (** [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block and a boolean indicating if it is a primitive record. *) -val declare_mind : mutual_inductive_entry -> object_name * bool +val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool (** Declaration messages *) @@ -83,10 +82,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 e16a955d96..eeda5a6867 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names -open CErrors open Util open Term open Constr @@ -17,17 +15,10 @@ open Vars open Declarations open Cooking open Entries -open Context.Rel.Declaration (********************************) (* Discharging mutual inductive *) -let detype_param = - function - | LocalAssum (Name id, p) -> id, LocalAssumEntry p - | LocalDef (Name id, p,_) -> id, LocalDefEntry p - | _ -> anomaly (Pp.str "Unnamed inductive local variable.") - (* Replace Var(y1)..Var(yq):C1..Cq |- Ij:Bj @@ -57,7 +48,7 @@ let abstract_inductive decls nparamdecls inds = (* To be sure to be the same as before, should probably be moved to process_inductive *) let params' = let (_,arity,_,_,_) = List.hd inds' in let (params,_) = decompose_prod_n_assum nparamdecls' arity in - List.map detype_param params + params in let ind'' = List.map @@ -88,13 +79,15 @@ let process_inductive info modlist mib = | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx | Polymorphic_ind auctx -> let subst, auctx = Lib.discharge_abstract_universe_context info auctx in + let nas = Univ.AUContext.names auctx in let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_ind_entry auctx + subst, Polymorphic_ind_entry (nas, auctx) | Cumulative_ind cumi -> let auctx = Univ.ACumulativityInfo.univ_context cumi in let subst, auctx = Lib.discharge_abstract_universe_context info auctx in + let nas = Univ.AUContext.names auctx in let auctx = Univ.AUContext.repr auctx in - subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx) + subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx) in let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in let inds = @@ -111,9 +104,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 bc6a1ef3aa..f5be0ddbae 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 @@ -232,7 +234,7 @@ let add_glob ?loc ref = add_glob_gen ?loc sp lib_dp ty let mp_of_kn kn = - let mp,sec,l = Names.KerName.repr kn in + let mp,l = Names.KerName.repr kn in Names.MPdot (mp,l) let add_glob_kn ?loc kn = @@ -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 43c100008c..931d05a975 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/dune b/interp/dune new file mode 100644 index 0000000000..e9ef7ba99a --- /dev/null +++ b/interp/dune @@ -0,0 +1,6 @@ +(library + (name interp) + (synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]") + (public_name coq.interp) + (wrapped false) + (libraries pretyping)) diff --git a/interp/genintern.ml b/interp/genintern.ml index 161201c448..1b736b7977 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -14,21 +14,42 @@ open Genarg module Store = Store.Make () +type intern_variable_status = { + intern_ids : Id.Set.t; + notation_variable_status : + (bool ref * Notation_term.subscopes option ref * + Notation_term.notation_var_internalization_type) + Id.Map.t +} + type glob_sign = { ltacvars : Id.Set.t; genv : Environ.env; extra : Store.t; + intern_sign : intern_variable_status; +} + +let empty_intern_sign = { + intern_ids = Id.Set.empty; + notation_variable_status = Id.Map.empty; } let empty_glob_sign env = { ltacvars = Id.Set.empty; genv = env; extra = Store.empty; + intern_sign = empty_intern_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 + 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 d818713fcf..4100f39029 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -14,14 +14,29 @@ open Genarg module Store : Store.S +type intern_variable_status = { + intern_ids : Id.Set.t; + notation_variable_status : + (bool ref * Notation_term.subscopes option ref * + Notation_term.notation_var_internalization_type) + Id.Map.t +} + type glob_sign = { ltacvars : Id.Set.t; genv : Environ.env; extra : Store.t; + intern_sign : intern_variable_status; } 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 +57,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 0000000000..607f2258fd --- /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 9ad62c0de3..d024a9e808 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -19,7 +19,6 @@ open Decl_kinds open Lib open Libobject open EConstr -open Termops open Reductionops open Constrexpr open Namegen @@ -139,7 +138,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 +162,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 = @@ -200,20 +199,22 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc acc.(i) <- update pos rig acc.(i) | App (f,_) when rig && is_flexible_reference env sigma bound depth f -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Proj (p,c) when rig -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Case _ when rig -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Evar _ -> () | _ -> - iter_constr_with_full_binders sigma push_lift (frec rig) ed c + iter_with_full_binders sigma push_lift (frec rig) ed c in 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 +227,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 +348,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 +374,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 +440,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 @@ -432,41 +449,41 @@ let compute_mib_implicits flags manual kn = (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> (** No need to care about constraints here *) - let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in + let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) mib.mind_packets) in let env_ar = Environ.push_rel_context ar env in 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)), + let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in + ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), Array.mapi (fun j c -> - (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,14 +504,14 @@ 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" +let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits" let implicits_of_global ref = try - let l = Refmap.find ref !implicits_table in + let l = GlobRef.Map.find ref !implicits_table in try let rename_l = Arguments_renaming.arguments_names ref in let rec rename implicits names = match implicits, names with @@ -509,7 +526,7 @@ let implicits_of_global ref = with Not_found -> [DefaultImpArgs,[]] let cache_implicits_decl (ref,imps) = - implicits_table := Refmap.add ref imps !implicits_table + implicits_table := GlobRef.Map.add ref imps !implicits_table let load_implicits _ (_,(_,l)) = List.iter cache_implicits_decl l @@ -520,7 +537,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 @@ -543,29 +560,27 @@ let discharge_implicits (_,(req,l)) = | ImplInteractive (ref,flags,exp) -> (try let vars = variable_section_segment_of_reference ref in - let ref' = if isVarRef ref then ref else pop_global_reference ref in let extra_impls = impls_of_context vars in - let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in - Some (ImplInteractive (ref',flags,exp),l') + let l' = [ref, List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in + Some (ImplInteractive (ref,flags,exp),l') with Not_found -> (* ref not defined in this section *) Some (req,l)) | ImplConstant (con,flags) -> (try - let con' = pop_con con in let vars = variable_section_segment_of_reference (ConstRef con) in let extra_impls = impls_of_context vars in let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in - let l' = [ConstRef con',newimpls] in - Some (ImplConstant (con',flags),l') + let l' = [ConstRef con,newimpls] in + Some (ImplConstant (con,flags),l') with Not_found -> (* con not defined in this section *) Some (req,l)) | ImplMutualInductive (kn,flags) -> (try let l' = List.map (fun (gr, l) -> let vars = variable_section_segment_of_reference gr in let extra_impls = impls_of_context vars in - ((if isVarRef gr then gr else pop_global_reference gr), + (gr, List.map (add_section_impls vars extra_impls) l)) l in - Some (ImplMutualInductive (pop_kn kn,flags),l') + Some (ImplMutualInductive (kn,flags),l') with Not_found -> (* ref not defined in this section *) Some (req,l)) let rebuild_implicits (req,l) = @@ -573,34 +588,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 +623,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 +637,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 +658,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 +668,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 +686,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, _ = Typeops.type_of_global_in_context env ref in + let t = of_constr t in let enriching = Option.default flags.auto enriching in - let isrigid,autoimpls = compute_auto_implicits env sigma flags enriching (of_constr t) in + let autoimpls = compute_auto_implicits env sigma flags enriching t in let l' = match l with | [] -> assert false | [l] -> - [DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l] + [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] | _ -> - check_rigidity isrigid; - let l = List.map (fun imps -> (imps,List.length imps)) l in - let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in - check_inclusion l; - let nargs = List.length autoimpls in - List.map (fun (imps,n) -> - (LessArgsThan (nargs-n), - set_manual_implicits env flags enriching autoimpls imps)) l in + check_rigidity (is_rigid env sigma t); + let l = List.map (fun imps -> (imps,List.length imps)) l in + let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in + check_inclusion l; + let nargs = List.length autoimpls in + List.map (fun (imps,n) -> + (LessArgsThan (nargs-n), + set_manual_implicits flags enriching autoimpls imps)) l in let req = if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) - in - add_anonymous_leaf (inImplicits (req,[ref,l'])) + in add_anonymous_leaf (inImplicits (req,[ref,l'])) let maybe_declare_manual_implicits local ref ?enriching l = match l with diff --git a/interp/impargs.mli b/interp/impargs.mli index 1eeb8e41ae..ea5aa90f68 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -10,7 +10,6 @@ open Names open EConstr -open Globnames open Environ (** {6 Implicit Arguments } *) @@ -103,7 +102,7 @@ val declare_var_implicits : variable -> unit val declare_constant_implicits : Constant.t -> unit val declare_mib_implicits : MutInd.t -> unit -val declare_implicits : bool -> global_reference -> unit +val declare_implicits : bool -> GlobRef.t -> unit (** [declare_manual_implicits local ref enriching l] Manual declaration of which arguments are expected implicit. @@ -111,15 +110,15 @@ val declare_implicits : bool -> global_reference -> unit implicits depending on the current state. Unsets implicits if [l] is empty. *) -val declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> +val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> manual_implicits list -> unit (** If the list is empty, do nothing, otherwise declare the implicits. *) -val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool -> +val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> manual_implicits -> unit -val implicits_of_global : global_reference -> implicits_list list +val implicits_of_global : GlobRef.t -> implicits_list list val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list @@ -130,7 +129,7 @@ val make_implicits_list : implicit_status list -> implicits_list list val drop_first_implicits : int -> implicits_list -> implicits_list -val projection_implicits : env -> projection -> implicit_status list -> +val projection_implicits : env -> Projection.t -> implicit_status list -> implicit_status list val select_impargs_size : int -> implicits_list list -> implicit_status list diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index a1a3be70f1..4f3037b1fc 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,13 +241,19 @@ let implicit_application env ?(allow_partial=true) f ty = let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in if not (Int.equal needlen applen) then - Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd + mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd end; let pars = List.rev (List.combine ci rd) in let args, avoid = combine_params avoid f par pars in CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid in c, avoid +let warn_ignoring_implicit_status = + CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits" + (fun na -> + strbrk "Ignoring implicit status of product binder " ++ + Name.print na ++ strbrk " and following binders") + let implicits_of_glob_constr ?(with_products=true) l = let add_impl i na bk l = match bk with | Implicit -> @@ -260,20 +269,18 @@ let implicits_of_glob_constr ?(with_products=true) l = let abs na bk b = add_impl i na bk (aux (succ i) b) in - match DAst.get c with - | GProd (na, bk, t, b) -> - if with_products then abs na bk b - else - let () = match bk with - | Implicit -> - Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ - Name.print na ++ strbrk " and following binders") - | _ -> () - in [] - | GLambda (na, bk, t, b) -> abs na bk b - | GLetIn (na, b, t, c) -> aux i b - | GRec (fix_kind, nas, args, tys, bds) -> - let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in - List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) - | _ -> [] + match DAst.get c with + | GProd (na, bk, t, b) -> + if with_products then abs na bk b + else + let () = match bk with + | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc + | _ -> () + in [] + | GLambda (na, bk, t, b) -> abs na bk b + | GLetIn (na, b, t, c) -> aux i b + | GRec (fix_kind, nas, args, tys, bds) -> + let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in + List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) + | _ -> [] in aux 1 l diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index b9815f34d5..437fef1753 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 bb22cf468d..aa20bda705 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,14 +1,16 @@ +Constrexpr +Genredexpr +Redops Tactypes Stdarg +Notation_term Genintern Notation_ops Notation Syntax_def Smartlocate Constrexpr_ops -Ppextend Dumpglob -Topconstr Reserve Impargs Implicit_quantifiers diff --git a/interp/modintern.ml b/interp/modintern.ml index dc93d8dc4d..60056dfd90 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 @@ -59,15 +61,54 @@ let lookup_module_or_modtype kind {CAst.loc;v=qid} = let lookup_module lqid = fst (lookup_module_or_modtype Module lqid) -let transl_with_decl env = function +let lookup_polymorphism env base kind fqid = + let m = match kind with + | Module -> (Environ.lookup_module base env).mod_type + | ModType -> (Environ.lookup_modtype base env).mod_type + | ModAny -> assert false + in + let rec defunctor = function + | NoFunctor m -> m + | MoreFunctor (_,_,m) -> defunctor m + in + let rec aux m fqid = + let open Names in + match fqid with + | [] -> assert false + | [id] -> + let test (lab,obj) = + match Id.equal (Label.to_id lab) id, obj with + | false, _ | _, (SFBmodule _ | SFBmodtype _) -> None + | true, SFBmind mind -> Some (Declareops.inductive_is_polymorphic mind) + | true, SFBconst const -> Some (Declareops.constant_is_polymorphic const) + in + (try CList.find_map test m with Not_found -> false (* error later *)) + | id::rem -> + let next = function + | MoreFunctor _ -> false (* error later *) + | NoFunctor body -> aux body rem + in + let test (lab,obj) = + match Id.equal (Label.to_id lab) id, obj with + | false, _ | _, (SFBconst _ | SFBmind _) -> None + | true, SFBmodule body -> Some (next body.mod_type) + | true, SFBmodtype body -> (* XXX is this valid? If not error later *) + Some (next body.mod_type) + in + (try CList.find_map test m with Not_found -> false (* error later *)) + in + aux (defunctor m) fqid + +let transl_with_decl env base kind = 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 -> - let inst, ctx = Univ.abstract_universes ctx in + let poly = lookup_polymorphism env base kind fqid in + begin match UState.check_univ_decl ~poly ectx udecl with + | Entries.Polymorphic_const_entry (nas, ctx) -> + let inst, ctx = Univ.abstract_universes nas ctx in let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in let c = EConstr.to_constr sigma c in WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty @@ -83,24 +124,25 @@ 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 - (MEident mp, kind, cst) + let (mp,kind) = lookup_module_or_modtype kind qid in + (MEident mp, mp, kind, cst) | {CAst.loc;v=CMapply (me1,me2)} -> - let me1',kind1, cst = interp_module_ast env kind me1 cst in - let me2',kind2, cst = interp_module_ast env ModAny me2 cst in + let me1', base, kind1, cst = interp_module_ast env kind me1 cst in + let me2', _, kind2, cst = interp_module_ast env ModAny me2 cst in let mp2 = match me2' with | MEident mp -> mp | _ -> error_application_to_not_path (loc_of_module me2) me2' in if kind2 == ModType then error_application_to_module_type (loc_of_module me2); - (MEapply (me1',mp2), kind1, cst) + (MEapply (me1',mp2), base, kind1, cst) | {CAst.loc;v=CMwith (me,decl)} -> - let me,kind,cst = interp_module_ast env kind me cst in + let me,base,kind,cst = interp_module_ast env kind me cst in if kind == Module then error_incorrect_with_in_module m.CAst.loc; - let decl, cst' = transl_with_decl env decl in + let decl, cst' = transl_with_decl env base kind decl in let cst = Univ.ContextSet.union cst cst' in - (MEwith(me,decl), kind, cst) + (MEwith(me,decl), base, kind, cst) let interp_module_ast env kind m = - interp_module_ast env kind m Univ.ContextSet.empty + let me, _, kind, cst = interp_module_ast env kind m Univ.ContextSet.empty in + me, kind, cst diff --git a/interp/modintern.mli b/interp/modintern.mli index ef37aead8a..529c438c1a 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 47d6481350..db8ee5bc18 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 *) @@ -49,17 +72,13 @@ type notation_location = (DirPath.t * DirPath.t) * string type notation_data = { not_interp : interpretation; not_location : notation_location; - not_onlyprinting : bool; } 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 @@ -67,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 } @@ -79,56 +98,40 @@ 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 warn_undeclared_scope = + CWarnings.create ~name:"undeclared-scope" ~category:"deprecated" + (fun (scope) -> + strbrk "Declaring a scope implicitly is deprecated; use in advance an explicit " + ++ str "\"Declare Scope " ++ str scope ++ str ".\".") let declare_scope scope = try let _ = String.Map.find scope !scope_map in () with Not_found -> -(* Flags.if_warn message ("Creating scope "^scope);*) scope_map := String.Map.add scope empty_scope !scope_map let error_unknown_scope sc = user_err ~hdr:"Notation" (str "Scope " ++ str sc ++ str " is not declared.") -let find_scope scope = +let find_scope ?(tolerant=false) scope = try String.Map.find scope !scope_map - with Not_found -> error_unknown_scope scope + with Not_found -> + if tolerant then + (* tolerant mode to be turn off after deprecation phase *) + begin + warn_undeclared_scope scope; + scope_map := String.Map.add scope empty_scope !scope_map; + empty_scope + end + else + error_unknown_scope scope + +let check_scope ?(tolerant=false) scope = + let _ = find_scope ~tolerant scope in () -let check_scope sc = let _ = find_scope sc in () +let ensure_scope scope = check_scope ~tolerant:true scope + +let find_scope scope = find_scope scope (* [sc] might be here a [scope_name] or a [delimiter] (now allowed after Open Scope) *) @@ -144,12 +147,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 @@ -201,8 +204,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) @@ -259,11 +260,11 @@ 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 -| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2 +| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2 | RefKey _, Oth -> -1 | Oth, RefKey _ -> 1 | Oth, Oth -> 0 @@ -284,16 +285,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, _) -> @@ -321,77 +320,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 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 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 ofNumeral n s = + 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 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 mkString = function + | None -> None + | Some s -> if Unicode.is_utf8 s then Some (String s) else None + + 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 -let delay dir int ?loc x = (dir, (fun () -> int ?loc x)) +(* 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 ? *) +} -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign +(* 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 (GlobRef.Map.empty : (scope_name * prim_token_interp_info * bool) GlobRef.Map.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 + check_scope ~tolerant:true 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 := + GlobRef.Map.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]). +*) + +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 *) @@ -419,7 +862,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 @@ -428,41 +871,32 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function (* Can we switch to [scope]? Yes if it has defined delimiters *) find_with_delimiters ntn_scope -(* Uninterpreted notation levels *) - -let declare_notation_level ntn level = - if String.Map.mem ntn !notation_level_map then - anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level."); - notation_level_map := String.Map.add ntn level !notation_level_map - -let level_of_notation ntn = - String.Map.find ntn !notation_level_map - (* The mapping between notations and their interpretation *) let warn_notation_overridden = 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 = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in - let () = - if String.Map.mem ntn sc.notations then - let which_scope = match scopt with - | None -> mt () - | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in - warn_notation_overridden (ntn,which_scope) - in - let notdata = { - not_interp = pat; - not_location = df; - not_onlyprinting = onlyprint; - } in - let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in - let () = scope_map := String.Map.add scope sc !scope_map in + if not onlyprint then begin + let () = + if NotationMap.mem ntn sc.notations then + let which_scope = match scopt with + | None -> mt () + | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in + warn_notation_overridden (ntn,which_scope) + in + let notdata = { + not_interp = pat; + not_location = df; + } in + let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in + scope_map := String.Map.add scope sc !scope_map + end; begin match scopt with | None -> scope_stack := SingleNotation ntn :: !scope_stack | Some _ -> () @@ -477,7 +911,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 *) @@ -486,13 +920,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 () = if n.not_onlyprinting then raise Not_found 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 = @@ -504,21 +937,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 = @@ -543,7 +980,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) @@ -557,47 +994,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,_) = GlobRef.Map.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) @@ -618,7 +1169,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 @@ -630,8 +1182,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 - onlyprint = n.not_onlyprinting && + let n = NotationMap.find ntn sc.notations in interpretation_eq n.not_interp r with Not_found -> false @@ -715,7 +1266,7 @@ let rec update_scopes cls scl = match cls, scl with | _, [] -> List.map find_scope_class_opt cls | cl :: cls, sco :: scl -> update_scope cl sco :: update_scopes cls scl -let arguments_scope = ref Refmap.empty +let arguments_scope = ref GlobRef.Map.empty type arguments_scope_discharge_request = | ArgsScopeAuto @@ -725,7 +1276,7 @@ type arguments_scope_discharge_request = let load_arguments_scope _ (_,(_,r,n,scl,cls)) = List.iter (Option.iter check_scope) scl; let initial_stamp = ScopeClassMap.empty in - arguments_scope := Refmap.add r (scl,cls,initial_stamp) !arguments_scope + arguments_scope := GlobRef.Map.add r (scl,cls,initial_stamp) !arguments_scope let cache_arguments_scope o = load_arguments_scope 1 o @@ -741,7 +1292,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,_)) = @@ -753,7 +1304,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) = vars |> List.map fst |> List.filter is_local_assum |> List.length with Not_found (* Not a ref defined in this section *) -> 0 in - Some (req,Lib.discharge_global r,n,l,[]) + Some (req,r,n,l,[]) let classify_arguments_scope (req,_,_,_,_ as obj) = if req == ArgsScopeNoDischarge then Dispose else Substitute obj @@ -763,7 +1314,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = | ArgsScopeNoDischarge -> assert false | ArgsScopeAuto -> let env = Global.env () in (*FIXME?*) - let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in + let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in let scs,cls = compute_arguments_scope_full sigma typ in (req,r,List.length scs,scs,cls) | ArgsScopeManual -> @@ -771,14 +1322,14 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) = for the extra parameters of the section. Discard the classes of the manually given scopes to avoid further re-computations. *) let env = Global.env () in (*FIXME?*) - let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in + let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in let l',cls = compute_arguments_scope_full sigma typ in let l1 = List.firstn n l' in let cls1 = List.firstn n cls in (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 @@ -806,19 +1357,19 @@ let declare_arguments_scope local r scl = let find_arguments_scope r = try - let (scl,cls,stamp) = Refmap.find r !arguments_scope in + let (scl,cls,stamp) = GlobRef.Map.find r !arguments_scope in let cur_stamp = !scope_class_map in if stamp == cur_stamp then scl else (* Recent changes in the Bind Scope base, we re-compute the scopes *) let scl' = update_scopes cls scl in - arguments_scope := Refmap.add r (scl',cls,cur_stamp) !arguments_scope; + arguments_scope := GlobRef.Map.add r (scl',cls,cur_stamp) !arguments_scope; scl' with Not_found -> [] let declare_ref_arguments_scope sigma ref = let env = Global.env () in (* FIXME? *) - let typ = EConstr.of_constr @@ fst @@ Global.type_of_global_in_context env ref in + let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in let (scs,cls as o) = compute_arguments_scope_full sigma typ in declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o @@ -847,10 +1398,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 +1416,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 +1445,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 +1467,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 +1480,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 +1535,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 +1552,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 @@ -1051,7 +1602,7 @@ let locate_notation prglob ntn scope = | [] -> str "Unknown notation" | _ -> str "Notation" ++ fnl () ++ - prlist (fun (ntn,l) -> + prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in prlist (fun (sc,r,(_,df)) -> @@ -1060,15 +1611,14 @@ let locate_notation prglob ntn scope = (if String.equal sc default_scope then mt () else (spc () ++ str ": " ++ str sc)) ++ (if Option.equal String.equal (Some sc) scope - then spc () ++ str "(default interpretation)" else mt ()) - ++ fnl ())) + then spc () ++ str "(default interpretation)" else mt ()))) l) ntns let collect_notation_in_scope scope sc known = 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 = @@ -1081,10 +1631,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 @@ -1114,64 +1664,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 := GlobRef.Map.empty let _ = Summary.declare_summary "symbols" diff --git a/interp/notation.mli b/interp/notation.mli index 6803a7e517..734198bbf6 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,13 +39,12 @@ 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 +(* To be removed after deprecation phase *) +val ensure_scope : scope_name -> unit -val level_eq : level -> level -> bool +val current_scopes : unit -> scopes (** Check where a scope is opened or not in a scope list, or in * the current opened scopes *) @@ -66,33 +77,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 +191,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 +208,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 +221,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 : notation -> level -> unit -val level_of_notation : notation -> level (** raise [Not_found] if no level *) - (** {6 Miscellaneous} *) -val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> bool) -> - notation -> delimiters option -> global_reference +val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> + notation_key -> delimiters option -> GlobRef.t (** Checks for already existing notations *) val exists_notation_in_scope : scope_name option -> notation -> @@ -152,9 +235,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 +248,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 +269,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 +279,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 a0d69ce796..7a525f84a5 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,14 +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 -| NProj (p1, c1), NProj (p2, c2) -> - Projection.equal p1 p2 && eq_notation_constr vars c1 c2 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _ | NProj _), _ -> false + | NRec _ | NSort _ | NCast _ ), _ -> false (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) @@ -154,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 @@ -165,15 +166,15 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = | NApp (a,args) -> GApp (f e a, List.map (f e) args) | NList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in - let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in + let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in let inner = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in - let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in + let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in DAst.get (subst_glob_vars outerl it) | NBinderList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in - let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in + let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in let inner = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in - let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in + let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in DAst.get (subst_glob_vars outerl it) | NLambda (na,ty,c) -> let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c)) @@ -183,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 @@ -210,16 +211,15 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let e',na = protect g e na in GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2) | NRec (fk,idl,dll,tl,bl) -> - let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) -> + let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) -> let e,na = protect g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = Array.fold_left_map (to_id (protect g)) e idl in 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) - | NProj (p,c) -> GProj (p, f e c) let glob_constr_of_notation_constr ?loc x = let rec aux () x = @@ -433,13 +433,12 @@ 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; NHole (w, naming, arg) | GRef (r,_) -> NRef r - | GProj (p, c) -> NProj (p, aux c) | GEvar _ | GPatVar _ -> user_err Pp.(str "Existential variables not allowed in notations.") ) x @@ -509,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; @@ -521,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) @@ -536,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') @@ -566,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) -> @@ -581,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')) @@ -594,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 @@ -610,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') @@ -628,23 +629,15 @@ 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') - | NProj (p, c) -> - let kn = Projection.constant p in - let b = Projection.unfolded p in - let kn' = subst_constant subst kn in - let c' = subst_notation_constr subst bound c in - if kn' == kn && c' == c then raw else NProj(Projection.make kn' b, c') - - let subst_interpretation subst (metas,pat) = let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in (metas,subst_notation_constr subst bound pat) @@ -663,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 @@ -684,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 @@ -899,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 *) @@ -1007,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 *) @@ -1054,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 = @@ -1123,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 = @@ -1191,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 @@ -1205,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 @@ -1217,12 +1212,9 @@ let rec match_ inner u alp metas sigma a1 a2 = match_names metas (alp,sigma) (Name id') na in match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2 - | GProj(p1, t1), NProj(p2, t2) when Projection.equal p1 p2 -> - match_in u alp metas sigma t1 t2 - | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ - | GCast _ | GProj _ ), _ -> raise No_match + | GCast _ ), _ -> raise No_match and match_in u = match_ true u @@ -1238,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)}] -> @@ -1335,10 +1327,10 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 = match DAst.get a1, a2 with | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) - | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> + | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 -> let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in sigma,(0,l) - | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) + | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index f038b5be1a..58fa221b16 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 0000000000..5fb0ca1b43 --- /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 c75d9e12f7..0000000000 --- a/interp/ppextend.ml +++ /dev/null @@ -1,43 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open Notation_term - -(*s Pretty-print. *) - -type ppbox = - | PpHB of int - | PpHOVB of int - | PpHVB of int - | PpVB of int - -type ppcut = - | PpBrk of int * int - | PpFnl - -let ppcmd_of_box = function - | PpHB n -> h n - | PpHOVB n -> hov n - | PpHVB n -> hv n - | PpVB n -> v n - -let ppcmd_of_cut = function - | PpFnl -> fnl () - | PpBrk(n1,n2) -> brk(n1,n2) - -type unparsing = - | UnpMetaVar of int * parenRelation - | UnpBinderMetaVar of int * parenRelation - | UnpListMetaVar of int * parenRelation * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list - | UnpTerminal of string - | UnpBox of ppbox * unparsing Loc.located list - | UnpCut of ppcut diff --git a/interp/redops.ml b/interp/redops.ml new file mode 100644 index 0000000000..b9a74136e4 --- /dev/null +++ b/interp/redops.ml @@ -0,0 +1,64 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Genredexpr + +let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *) + +let make_red_flag l = + let rec add_flag red = function + | [] -> red + | FBeta :: lf -> add_flag { red with rBeta = true } lf + | FMatch :: lf -> add_flag { red with rMatch = true } lf + | FFix :: lf -> add_flag { red with rFix = true } lf + | FCofix :: lf -> add_flag { red with rCofix = true } lf + | FZeta :: lf -> add_flag { red with rZeta = true } lf + | FConst l :: lf -> + if red.rDelta then + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); + add_flag { red with rConst = union_consts red.rConst l } lf + | FDeltaBut l :: lf -> + if red.rConst <> [] && not red.rDelta then + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); + add_flag + { red with rConst = union_consts red.rConst l; rDelta = true } + lf + in + add_flag + {rBeta = false; rMatch = false; rFix = false; rCofix = false; + rZeta = false; rDelta = false; rConst = []} + l + + +let all_flags = + {rBeta = true; rMatch = true; rFix = true; rCofix = true; + rZeta = true; rDelta = true; rConst = []} + +(** Mapping [red_expr_gen] *) + +let map_flags f flags = + { flags with rConst = List.map f flags.rConst } + +let map_occs f (occ,e) = (occ,f e) + +let map_red_expr_gen f g h = function + | Fold l -> Fold (List.map f l) + | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l) + | Simpl (flags,occs_o) -> + Simpl (map_flags g flags, Option.map (map_occs (Util.map_union g h)) occs_o) + | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l) + | Cbv flags -> Cbv (map_flags g flags) + | Lazy flags -> Lazy (map_flags g flags) + | CbvVm occs_o -> CbvVm (Option.map (map_occs (Util.map_union g h)) occs_o) + | CbvNative occs_o -> CbvNative (Option.map (map_occs (Util.map_union g h)) occs_o) + | Cbn flags -> Cbn (map_flags g flags) + | ExtraRedExpr _ | Red _ | Hnf as x -> x diff --git a/interp/ppextend.mli b/interp/redops.mli index c81058e725..7254f29b25 100644 --- a/interp/ppextend.mli +++ b/interp/redops.mli @@ -8,29 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Notation_term +open Genredexpr -(** {6 Pretty-print. } *) +val make_red_flag : 'a red_atom list -> 'a glob_red_flag -type ppbox = - | PpHB of int - | PpHOVB of int - | PpHVB of int - | PpVB of int +val all_flags : 'a glob_red_flag -type ppcut = - | PpBrk of int * int - | PpFnl +(** Mapping [red_expr_gen] *) -val ppcmd_of_box : ppbox -> Pp.t -> Pp.t - -val ppcmd_of_cut : ppcut -> Pp.t - -type unparsing = - | UnpMetaVar of int * parenRelation - | UnpBinderMetaVar of int * parenRelation - | UnpListMetaVar of int * parenRelation * unparsing list - | UnpBinderListMetaVar of int * bool * unparsing list - | UnpTerminal of string - | UnpBox of ppbox * unparsing Loc.located list - | UnpCut of ppcut +val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) -> + ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen diff --git a/interp/reserve.ml b/interp/reserve.ml index 36005121b1..edbdf1dbba 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -22,13 +22,13 @@ open Notation_ops open Globnames type key = - | RefKey of global_reference + | RefKey of GlobRef.t | Oth (** TODO: share code from Notation *) let key_compare k1 k2 = match k1, k2 with -| RefKey gr1, RefKey gr2 -> RefOrdered.compare gr1 gr2 +| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2 | RefKey _, Oth -> -1 | Oth, RefKey _ -> 1 | Oth, Oth -> 0 @@ -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 daee58639f..a10858e71f 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 1f4a93a6f3..91491bdf8d 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 7ff7e899e2..e41ef78913 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 e5ed58be6b..7b01b6dc1c 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 53d1a522d3..5e5e43ed38 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 47faa5885c..b73d238c22 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -15,7 +15,6 @@ open Names open Libnames open Libobject open Lib -open Nametab open Notation_term (* Syntactic definitions. *) @@ -38,7 +37,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = let is_alias_of_already_visible_name sp = function | _,NRef ref -> - let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in + let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in DirPath.is_empty dir && Id.equal id (basename sp) | _ -> false @@ -77,17 +76,17 @@ 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 () -let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) +let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) let pr_compat_warning (kn, def, v) = let pp_def = match def with - | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r + | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r | _ -> strbrk " is a compatibility notation" in pr_syndef kn ++ pp_def @@ -96,13 +95,13 @@ let warn_compatibility_notation = CWarnings.(create ~name:"compatibility-notation" ~category:"deprecated" ~default:Enabled pr_compat_warning) -let verbose_compat kn def = function +let verbose_compat ?loc kn def = function | Some v when Flags.version_strictly_greater v -> - warn_compatibility_notation (kn, def, v) + warn_compatibility_notation ?loc (kn, def, v) | _ -> () -let search_syntactic_definition kn = +let search_syntactic_definition ?loc kn = let pat,v = KNmap.find kn !syntax_table in let def = out_pat pat in - verbose_compat kn def v; + verbose_compat ?loc kn def v; def diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 1933b8a9ae..c5b6655ff8 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -18,4 +18,4 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr val declare_syntactic_definition : bool -> Id.t -> Flags.compat_version option -> syndef_interpretation -> unit -val search_syntactic_definition : KerName.t -> syndef_interpretation +val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation diff --git a/interp/tactypes.ml b/interp/tactypes.ml deleted file mode 100644 index 83e42be89f..0000000000 --- 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 7d2d75d9cb..0000000000 --- a/interp/topconstr.ml +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Constrexpr_ops - -let asymmetric_patterns = asymmetric_patterns -let error_invalid_pattern_notation = error_invalid_pattern_notation -let split_at_annot = split_at_annot -let ntn_loc = ntn_loc -let patntn_loc = patntn_loc -let map_constr_expr_with_binders = map_constr_expr_with_binders -let fold_constr_expr_with_binders = fold_constr_expr_with_binders -let ids_of_cases_indtype = ids_of_cases_indtype -let occur_var_constr_expr = occur_var_constr_expr -let free_vars_of_constr_expr = free_vars_of_constr_expr -let replace_vars_constr_expr = replace_vars_constr_expr diff --git a/interp/topconstr.mli b/interp/topconstr.mli deleted file mode 100644 index c86502015a..0000000000 --- a/interp/topconstr.mli +++ /dev/null @@ -1,53 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constrexpr - -(** Topconstr: This whole module is deprecated in favor of Constrexpr_ops *) -val asymmetric_patterns : bool ref -[@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"] - -(** Utilities on constr_expr *) -val split_at_annot : local_binder_expr list -> Misctypes.lident option -> local_binder_expr list * local_binder_expr list -[@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"] - -val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list -[@@ocaml.deprecated "use Constrexpr_ops.ntn_loc"] -val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list -[@@ocaml.deprecated "use Constrexpr_ops.patntn_loc"] - -(** For cases pattern parsing errors *) -val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a -[@@ocaml.deprecated "use Constrexpr_ops.error_invalid_pattern_notation"] - -(*************************************************************************) -val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr -[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] - -val free_vars_of_constr_expr : constr_expr -> Id.Set.t -[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] - -val occur_var_constr_expr : Id.t -> constr_expr -> bool -[@@ocaml.deprecated "use Constrexpr_ops.occur_var_constr_expr"] - -(** Specific function for interning "in indtype" syntax of "match" *) -val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t -[@@ocaml.deprecated "use Constrexpr_ops.ids_of_cases_indtype"] - -(** Used in typeclasses *) -val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> - ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b -[@@ocaml.deprecated "use Constrexpr_ops.fold_constr_expr_with_binders"] - -val map_constr_expr_with_binders : - (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> - 'a -> constr_expr -> constr_expr -[@@ocaml.deprecated "use Constrexpr_ops.map_constr_expr_with_binders"] |