diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 152 | ||||
| -rw-r--r-- | interp/constrexpr_ops.ml | 35 | ||||
| -rw-r--r-- | interp/constrexpr_ops.mli | 15 | ||||
| -rw-r--r-- | interp/constrextern.ml | 9 | ||||
| -rw-r--r-- | interp/constrintern.ml | 26 | ||||
| -rw-r--r-- | interp/declare.ml | 8 | ||||
| -rw-r--r-- | interp/declare.mli | 2 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 2 | ||||
| -rw-r--r-- | interp/dumpglob.mli | 4 | ||||
| -rw-r--r-- | interp/genredexpr.ml | 66 | ||||
| -rw-r--r-- | interp/impargs.ml | 10 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 8 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 6 | ||||
| -rw-r--r-- | interp/interp.mllib | 5 | ||||
| -rw-r--r-- | interp/modintern.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 101 | ||||
| -rw-r--r-- | interp/notation.mli | 23 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 35 | ||||
| -rw-r--r-- | interp/notation_term.ml | 37 | ||||
| -rw-r--r-- | interp/ppextend.ml | 43 | ||||
| -rw-r--r-- | interp/redops.ml | 64 | ||||
| -rw-r--r-- | interp/redops.mli (renamed from interp/ppextend.mli) | 28 | ||||
| -rw-r--r-- | interp/reserve.ml | 4 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 8 | ||||
| -rw-r--r-- | interp/syntax_def.mli | 2 | ||||
| -rw-r--r-- | interp/topconstr.ml | 23 | ||||
| -rw-r--r-- | interp/topconstr.mli | 53 |
27 files changed, 412 insertions, 359 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml new file mode 100644 index 0000000000..ca6ea94f09 --- /dev/null +++ b/interp/constrexpr.ml @@ -0,0 +1,152 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Libnames +open Misctypes +open Decl_kinds + +(** {6 Concrete syntax for terms } *) + +(** [constr_expr] is the abstract syntax tree produced by the parser *) +type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl + +type ident_decl = lident * universe_decl_expr option +type name_decl = lname * universe_decl_expr option + +type notation = string + +type explicitation = + | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *) + | ExplByName of Id.t + +type binder_kind = + | Default of binding_kind + | Generalized of binding_kind * binding_kind * bool + (** Inner binding, outer bindings, typeclass-specific flag + for implicit generalization of superclasses *) + +type abstraction_kind = AbsLambda | AbsPi + +type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) + +(** Representation of integer literals that appear in Coq scripts. + We now use raw strings of digits in base 10 (big-endian), and a separate + sign flag. Note that this representation is not unique, due to possible + multiple leading zeros, and -0 = +0 *) + +type sign = bool +type raw_natural_number = string + +type prim_token = + | Numeral of raw_natural_number * sign + | String of string + +type instance_expr = Glob_term.glob_level list + +type cases_pattern_expr_r = + | CPatAlias of cases_pattern_expr * lname + | CPatCstr of reference + * cases_pattern_expr list option * cases_pattern_expr list + (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) + | CPatAtom of reference option + | CPatOr of cases_pattern_expr list + | CPatNotation of notation * cases_pattern_notation_substitution + * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents + (notation n applied with substitution l1) + applied to arguments l2 *) + | CPatPrim of prim_token + | CPatRecord of (reference * cases_pattern_expr) list + | CPatDelimiters of string * cases_pattern_expr + | CPatCast of cases_pattern_expr * constr_expr +and cases_pattern_expr = cases_pattern_expr_r CAst.t + +and cases_pattern_notation_substitution = + cases_pattern_expr list * (** for constr subterms *) + cases_pattern_expr list list (** for recursive notations *) + +and constr_expr_r = + | CRef of reference * instance_expr option + | CFix of lident * fix_expr list + | CCoFix of lident * cofix_expr list + | CProdN of local_binder_expr list * constr_expr + | CLambdaN of local_binder_expr list * constr_expr + | CLetIn of lname * constr_expr * constr_expr option * constr_expr + | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list + | CApp of (proj_flag * constr_expr) * + (constr_expr * explicitation CAst.t option) list + | CRecord of (reference * constr_expr) list + + (* representation of the "let" and "match" constructs *) + | CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *) + * constr_expr option (* return-clause *) + * case_expr list + * branch_expr list (* branches *) + + | CLetTuple of lname list * (lname option * constr_expr option) * + constr_expr * constr_expr + | CIf of constr_expr * (lname option * constr_expr option) + * constr_expr * constr_expr + | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option + | CPatVar of patvar + | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list + | CSort of Glob_term.glob_sort + | CCast of constr_expr * constr_expr cast_type + | CNotation of notation * constr_notation_substitution + | CGeneralization of binding_kind * abstraction_kind option * constr_expr + | CPrim of prim_token + | CDelimiters of string * constr_expr + | CProj of reference * constr_expr +and constr_expr = constr_expr_r CAst.t + +and case_expr = constr_expr (* expression that is being matched *) + * lname option (* as-clause *) + * cases_pattern_expr option (* in-clause *) + +and branch_expr = + (cases_pattern_expr list list * constr_expr) CAst.t + +and fix_expr = + lident * (lident option * recursion_order_expr) * + local_binder_expr list * constr_expr * constr_expr + +and cofix_expr = + lident * local_binder_expr list * constr_expr * constr_expr + +and recursion_order_expr = + | CStructRec + | CWfRec of constr_expr + | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) + +(* Anonymous defs allowed ?? *) +and local_binder_expr = + | CLocalAssum of lname list * binder_kind * constr_expr + | CLocalDef of lname * constr_expr * constr_expr option + | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t + +and constr_notation_substitution = + constr_expr list * (** for constr subterms *) + constr_expr list list * (** for recursive notations *) + cases_pattern_expr list * (** for binders *) + local_binder_expr list list (** for binder lists (recursive notations) *) + +type constr_pattern_expr = constr_expr + +(** Concrete syntax for modules and module types *) + +type with_declaration_ast = + | CWith_Module of Id.t list CAst.t * qualid CAst.t + | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr + +type module_ast_r = + | CMident of qualid + | CMapply of module_ast * module_ast + | CMwith of module_ast * with_declaration_ast +and module_ast = module_ast_r CAst.t diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 4ee13c961f..1be1dd96cb 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -601,7 +601,34 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> asymmetric_patterns:=a); } -(************************************************************************) -(* Deprecated *) -let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c -let prod_constr_expr c bl = mkCProdN ?loc:(local_binders_loc bl) bl c +(** Local universe and constraint declarations. *) + +let interp_univ_constraints env evd cstrs = + let interp (evd,cstrs) (u, d, u') = + let ul = Pretyping.interp_known_glob_level evd u in + let u'l = Pretyping.interp_known_glob_level evd u' in + let cstr = (ul,d,u'l) in + let cstrs' = Univ.Constraint.add cstr cstrs in + try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in + evd, cstrs' + with Univ.UniverseInconsistency e -> + CErrors.user_err ~hdr:"interp_constraint" + (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e) + in + List.fold_left interp (evd,Univ.Constraint.empty) cstrs + +let interp_univ_decl env decl = + let open UState in + let pl : lident list = decl.univdecl_instance in + let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in + let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in + let decl = { univdecl_instance = pl; + univdecl_extensible_instance = decl.univdecl_extensible_instance; + univdecl_constraints = cstrs; + univdecl_extensible_constraints = decl.univdecl_extensible_constraints } + in evd, decl + +let interp_univ_decl_opt env l = + match l with + | None -> Evd.from_env env, UState.default_univ_decl + | Some decl -> interp_univ_decl env decl diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index d038bd71ab..b4f0886acf 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -60,14 +60,6 @@ val mkCPatOr : ?loc:Loc.t -> cases_pattern_expr list -> cases_pattern_expr val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list -> cases_pattern_expr (** Apply a list of pattern arguments to a pattern *) -(** @deprecated variant of mkCLambdaN *) -val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr -[@@ocaml.deprecated "deprecated variant of mkCLambdaN"] - -(** @deprecated variant of mkCProdN *) -val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr -[@@ocaml.deprecated "deprecated variant of mkCProdN"] - (** {6 Destructors}*) val coerce_reference_to_id : reference -> Id.t @@ -124,3 +116,10 @@ val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a (** Placeholder for global option, should be moved to a parameter *) val asymmetric_patterns : bool ref + +(** Local universe and constraint declarations. *) +val interp_univ_decl : Environ.env -> universe_decl_expr -> + Evd.evar_map * UState.universe_decl + +val interp_univ_decl_opt : Environ.env -> universe_decl_expr option -> + Evd.evar_map * UState.universe_decl diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 7792eff664..86f6ce9ae8 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -28,7 +28,6 @@ open Pattern open Nametab open Notation open Detyping -open Misctypes open Decl_kinds module NamedDecl = Context.Named.Declaration @@ -931,7 +930,7 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes) and factorize_prod scopes vars na bk aty c = let store, get = set_temporary_memory () in match na, DAst.get c with - | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) + | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 -> (match get () with | [{CAst.v=(ids,disj_of_patl,b)}] -> @@ -959,7 +958,7 @@ and factorize_prod scopes vars na bk aty c = and factorize_lambda inctx scopes vars na bk aty c = let store, get = set_temporary_memory () in match na, DAst.get c with - | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) + | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 -> (match get () with | [{CAst.v=(ids,disj_of_patl,b)}] -> @@ -1209,7 +1208,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | PIf (c,b1,b2) -> GIf (glob_of_pat avoid env sigma c, (Anonymous,None), glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2) - | PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) -> + | PCase ({cip_style=Constr.LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) -> let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b) | PCase (info,p,tm,bl) -> @@ -1228,7 +1227,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 diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 48f15f8979..848180743f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -14,6 +14,7 @@ open Util open CAst open Names open Nameops +open Constr open Namegen open Libnames open Globnames @@ -525,7 +526,7 @@ let rec expand_binders ?loc mk bl c = let tm = DAst.make ?loc (GVar id) in (* Distribute the disjunctive patterns over the shared right-hand side *) let eqnl = List.map (fun pat -> CAst.make ?loc (ids,[pat],c)) disjpat in - let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in + let c = DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c) (**********************************************************************) @@ -819,11 +820,11 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) -> + | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent -> + | NtnTypeBinder NtnBinderParsedAsConstr AsIdent -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') @@ -998,7 +999,7 @@ let intern_qualid qid intern env ntnvars us args = match intern_extended_global_of_qualid qid with | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> - let (ids,c) = Syntax_def.search_syntactic_definition sp in + let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments ?loc; let args1,args2 = List.chop nids args in @@ -1140,9 +1141,18 @@ let check_number_of_pattern loc n l = if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = - if List.exists (fun ids' -> not (List.eq_set (fun {loc;v=id} {v=id'} -> Id.equal id id') ids ids')) idsl then - user_err ?loc (str - "The components of this disjunctive pattern must bind the same variables.") + let eq_id {v=id} {v=id'} = Id.equal id id' in + (* Collect remaining patterns which do not have the same variables as the first pattern *) + let idsl = List.filter (fun ids' -> not (List.eq_set eq_id ids ids')) idsl in + match idsl with + | ids'::_ -> + (* Look for an [id] which is either in [ids] and not in [ids'] or in [ids'] and not in [ids] *) + let ids'' = List.subtract eq_id ids ids' in + let ids'' = if ids'' = [] then List.subtract eq_id ids' ids else ids'' in + user_err ?loc + (strbrk "The components of this disjunctive pattern must bind the same variables (" ++ + Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).") + | [] -> () (** Use only when params were NOT asked to the user. @return if letin are included *) @@ -1965,7 +1975,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = if List.for_all (irrefutable globalenv) thepats then [] else [CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *) DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in - Some (DAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) + Some (DAst.make @@ GCases(RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in DAst.make ?loc @@ diff --git a/interp/declare.ml b/interp/declare.ml index c55a6c69ba..bc2d2068a2 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -487,7 +487,7 @@ let add_universe src (dp, i) = Option.iter (fun poly -> let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in Global.push_context_set poly ctx; - Universes.add_global_universe level poly; + UnivNames.add_global_universe level poly; if poly then Lib.add_section_context ctx) optpoly @@ -538,7 +538,7 @@ let input_universe : universe_decl -> Libobject.obj = let declare_univ_binders gr pl = if Global.is_polymorphic gr then - Universes.register_universe_binders gr pl + UnivNames.register_universe_binders gr pl else let l = match gr with | ConstRef c -> Label.to_id @@ Constant.label c @@ -564,7 +564,7 @@ let do_universe poly l = in let l = List.map (fun {CAst.v=id} -> - let lev = Universes.new_univ_id () in + let lev = UnivGen.new_univ_id () in (id, lev)) l in let src = if poly then BoundUniv else UnqualifiedUniv in @@ -595,7 +595,7 @@ let input_constraints : constraint_decl -> Libobject.obj = let do_constraint poly l = let u_of_id x = let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - Universes.is_polymorphic level, level + UnivNames.is_polymorphic level, level in let in_section = Lib.sections_are_opened () in let () = diff --git a/interp/declare.mli b/interp/declare.mli index de4d8346a4..4a9f542783 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -83,7 +83,7 @@ val recursive_message : bool (** true = fixpoint *) -> val exists_name : Id.t -> bool (** Global universe contexts, names and constraints *) -val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit +val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index bc6a1ef3aa..74618a2905 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -254,7 +254,7 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc -> let dump_definition {CAst.loc;v=id} sec s = dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id) -let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty = +let dump_constraint { CAst.loc; v = n } sec ty = match n with | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty | Names.Anonymous -> () diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 8dfb4f8f7f..bf83d2df40 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -38,8 +38,8 @@ val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit val dump_notation : (Constrexpr.notation * Notation.notation_location) Loc.located -> Notation_term.scope_name option -> bool -> unit -val dump_constraint : - Vernacexpr.typeclass_constraint -> bool -> string -> unit + +val dump_constraint : Misctypes.lname -> bool -> string -> unit val dump_string : string -> unit diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml new file mode 100644 index 0000000000..80697461a6 --- /dev/null +++ b/interp/genredexpr.ml @@ -0,0 +1,66 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Reduction expressions *) + +(** The parsing produces initially a list of [red_atom] *) + +type 'a red_atom = + | FBeta + | FMatch + | FFix + | FCofix + | FZeta + | FConst of 'a list + | FDeltaBut of 'a list + +(** This list of atoms is immediately converted to a [glob_red_flag] *) + +type 'a glob_red_flag = { + rBeta : bool; + rMatch : bool; + rFix : bool; + rCofix : bool; + rZeta : bool; + rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*) + rConst : 'a list +} + +(** Generic kinds of reductions *) + +type ('a,'b,'c) red_expr_gen = + | Red of bool + | Hnf + | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option + | Cbv of 'b glob_red_flag + | Cbn of 'b glob_red_flag + | Lazy of 'b glob_red_flag + | Unfold of 'b Locus.with_occurrences list + | Fold of 'a list + | Pattern of 'a Locus.with_occurrences list + | ExtraRedExpr of string + | CbvVm of ('b,'c) Util.union Locus.with_occurrences option + | CbvNative of ('b,'c) Util.union Locus.with_occurrences option + +type ('a,'b,'c) may_eval = + | ConstrTerm of 'a + | ConstrEval of ('a,'b,'c) red_expr_gen * 'a + | ConstrContext of Misctypes.lident * 'a + | ConstrTypeOf of 'a + +open Libnames +open Constrexpr +open Misctypes + +type r_trm = constr_expr +type r_pat = constr_pattern_expr +type r_cst = reference or_by_notation + +type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen diff --git a/interp/impargs.ml b/interp/impargs.ml index 7e4c4ef4f7..8aa1e62504 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -237,11 +237,11 @@ let is_rigid env sigma t = 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 @@ -249,7 +249,7 @@ let compute_implicits_names_gen all env sigma 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 + 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 @@ -538,7 +538,7 @@ let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) let subst_implicits (subst,(req,l)) = - (ImplLocal,List.smartmap (subst_implicits_decl subst) l) + (ImplLocal,List.Smart.map (subst_implicits_decl subst) l) let impls_of_context ctx = let map (decl, impl) = match impl with diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 58df9abc4a..b48db9ac54 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -17,12 +17,14 @@ open Glob_term open Constrexpr open Libnames open Typeclasses -open Typeclasses_errors open Pp open Libobject open Nameops open Context.Rel.Declaration +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) +let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) + module RelDecl = Context.Rel.Declaration (*i*) @@ -58,7 +60,7 @@ let in_generalizable : bool * Misctypes.lident list option -> obj = classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj) } -let declare_generalizable local gen = +let declare_generalizable ~local gen = Lib.add_anonymous_leaf (in_generalizable (local, gen)) let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table @@ -238,7 +240,7 @@ let implicit_application env ?(allow_partial=true) f ty = let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in if not (Int.equal needlen applen) then - Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd + mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd end; let pars = List.rev (List.combine ci rd) in let args, avoid = combine_params avoid f par pars in diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 5f4129ae0c..e64c5c5427 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -13,7 +13,7 @@ open Glob_term open Constrexpr open Libnames -val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit +val declare_generalizable : local:bool -> Misctypes.lident list option -> unit val ids_of_list : Id.t list -> Id.Set.t val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t @@ -45,3 +45,7 @@ val implicit_application : Id.Set.t -> ?allow_partial:bool -> (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t + +(* Should be likely located elsewhere *) +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) +val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Context.Rel.t -> 'a diff --git a/interp/interp.mllib b/interp/interp.mllib index 61313acc48..3668455aeb 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,3 +1,6 @@ +Constrexpr +Genredexpr +Redops Tactypes Stdarg Genintern @@ -7,9 +10,7 @@ Notation Syntax_def Smartlocate Constrexpr_ops -Ppextend Dumpglob -Topconstr Reserve Impargs Implicit_quantifiers diff --git a/interp/modintern.ml b/interp/modintern.ml index dc93d8dc4d..fefd2ab6f5 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -63,7 +63,7 @@ let transl_with_decl env = function | CWith_Module ({CAst.v=fqid},qid) -> WithMod (fqid,lookup_module qid), Univ.ContextSet.empty | CWith_Definition ({CAst.v=fqid},udecl,c) -> - let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in + let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in let c, ectx = interp_constr env sigma c in begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with | Entries.Polymorphic_const_entry ctx -> diff --git a/interp/notation.ml b/interp/notation.ml index e6df7b96c9..05fcd0e7f5 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -20,7 +20,6 @@ open Constrexpr open Notation_term open Glob_term open Glob_ops -open Ppextend open Context.Named.Declaration (*i*) @@ -56,9 +55,6 @@ type scope = { delimiters: delimiters option } -(* Uninterpreted notation map: notation -> level * DirPath.t *) -let notation_level_map = ref String.Map.empty - (* Scopes table: scope_name -> symbol_interpretation *) let scope_map = ref String.Map.empty @@ -75,44 +71,6 @@ let default_scope = "" (* empty name, not available from outside *) let init_scope_map () = scope_map := String.Map.add default_scope empty_scope !scope_map -(**********************************************************************) -(* Operations on scopes *) - -let parenRelation_eq t1 t2 = match t1, t2 with -| L, L | E, E | Any, Any -> true -| Prec l1, Prec l2 -> Int.equal l1 l2 -| _ -> false - -open Extend - -let production_level_eq l1 l2 = true (* (l1 = l2) *) - -let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with -| NextLevel, NextLevel -> true -| NumLevel n1, NumLevel n2 -> Int.equal n1 n2 -| (NextLevel | NumLevel _), _ -> false *) - -let constr_entry_key_eq eq v1 v2 = match v1, v2 with -| ETName, ETName -> true -| ETReference, ETReference -> true -| ETBigint, ETBigint -> true -| ETBinder b1, ETBinder b2 -> b1 == b2 -| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2 -| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2 -| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 -| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' -| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false - -let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) = - let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in - let prod_eq (l1,pp1) (l2,pp2) = - if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2 - else production_level_eq l1 l2 in - Int.equal l1 l2 && List.equal tolerability_eq t1 t2 - && List.equal (constr_entry_key_eq prod_eq) u1 u2 - -let level_eq = level_eq_gen false - let declare_scope scope = try let _ = String.Map.find scope !scope_map in () with Not_found -> @@ -427,18 +385,6 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function (* Can we switch to [scope]? Yes if it has defined delimiters *) find_with_delimiters ntn_scope -(* Uninterpreted notation levels *) - -let declare_notation_level ?(onlyprint=false) ntn level = - if String.Map.mem ntn !notation_level_map then - anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level."); - notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map - -let level_of_notation ?(onlyprint=false) ntn = - let (level,onlyprint') = String.Map.find ntn !notation_level_map in - if onlyprint' && not onlyprint then raise Not_found; - level - (* The mapping between notations and their interpretation *) let warn_notation_overridden = @@ -741,7 +687,7 @@ let subst_arguments_scope (subst,(req,r,n,scl,cls)) = match subst_scope_class subst cl with | Some cl' as ocl' when cl' != cl -> ocl' | _ -> ocl in - let cls' = List.smartmap subst_cl cls in + let cls' = List.Smart.map subst_cl cls in (ArgsScopeNoDischarge,r',n,scl,cls') let discharge_arguments_scope (_,(req,r,n,l,_)) = @@ -1113,63 +1059,24 @@ let pr_visibility prglob = function | None -> pr_scope_stack prglob !scope_stack (**********************************************************************) -(* Mapping notations to concrete syntax *) - -type unparsing_rule = unparsing list * precedence -type extra_unparsing_rules = (string * string) list -(* Concrete syntax for symbolic-extension table *) -let notation_rules = - ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t) - -let declare_notation_rule ntn ~extra unpl gram = - notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules - -let find_notation_printing_rule ntn = - try pi1 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".") -let find_notation_extra_printing_rules ntn = - try pi2 (String.Map.find ntn !notation_rules) - with Not_found -> [] -let find_notation_parsing_rules ntn = - try pi3 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".") - -let get_defined_notations () = - String.Set.elements @@ String.Map.domain !notation_rules - -let add_notation_extra_printing_rule ntn k v = - try - notation_rules := - let p, pp, gr = String.Map.find ntn !notation_rules in - String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules - with Not_found -> - user_err ~hdr:"add_notation_extra_printing_rule" - (str "No such Notation.") - -(**********************************************************************) (* Synchronisation with reset *) let freeze _ = - (!scope_map, !notation_level_map, !scope_stack, !arguments_scope, - !delimiters_map, !notations_key_table, !notation_rules, - !scope_class_map) + (!scope_map, !scope_stack, !arguments_scope, + !delimiters_map, !notations_key_table, !scope_class_map) -let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) = +let unfreeze (scm,scs,asc,dlm,fkm,clsc) = scope_map := scm; - notation_level_map := nlm; scope_stack := scs; delimiters_map := dlm; arguments_scope := asc; notations_key_table := fkm; - notation_rules := pprules; scope_class_map := clsc let init () = init_scope_map (); - notation_level_map := String.Map.empty; delimiters_map := String.Map.empty; notations_key_table := KeyMap.empty; - notation_rules := String.Map.empty; scope_class_map := initial_scope_class_map let _ = diff --git a/interp/notation.mli b/interp/notation.mli index ccc67fe491..b177b7f1e0 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -14,7 +14,6 @@ open Libnames open Constrexpr open Glob_term open Notation_term -open Ppextend (** Notations *) @@ -32,8 +31,6 @@ val declare_scope : scope_name -> unit val current_scopes : unit -> scopes -val level_eq : level -> level -> bool - (** Check where a scope is opened or not in a scope list, or in * the current opened scopes *) val scope_is_open_in_scopes : scope_name -> scopes -> bool @@ -135,11 +132,6 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list val availability_of_notation : scope_name option * notation -> local_scopes -> (scope_name option * delimiters option) option -(** {6 Declare and test the level of a (possibly uninterpreted) notation } *) - -val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit -val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *) - (** {6 Miscellaneous} *) val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> @@ -200,21 +192,6 @@ val locate_notation : (glob_constr -> Pp.t) -> notation -> val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t -(** {6 Printing rules for notations} *) - -(** Declare and look for the printing rule for symbolic notations *) -type unparsing_rule = unparsing list * precedence -type extra_unparsing_rules = (string * string) list -val declare_notation_rule : - notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit -val find_notation_printing_rule : notation -> unparsing_rule -val find_notation_extra_printing_rules : notation -> extra_unparsing_rules -val find_notation_parsing_rules : notation -> notation_grammar -val add_notation_extra_printing_rule : notation -> string -> string -> unit - -(** Returns notations with defined parsing/printing rules *) -val get_defined_notations : unit -> notation list - (** Rem: printing rules for primitive token are canonical *) val with_notation_protection : ('a -> 'b) -> 'a -> 'b diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index b806dce0b1..f208b23fb6 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -13,6 +13,7 @@ open CErrors open Util open Names open Nameops +open Constr open Globnames open Decl_kinds open Misctypes @@ -509,7 +510,9 @@ let notation_constr_of_glob_constr nenv a = let notation_constr_of_constr avoiding t = let t = EConstr.of_constr t in - let t = Detyping.detype Detyping.Now false avoiding (Global.env()) Evd.empty t in + let env = Global.env () in + let evd = Evd.from_env env in + let t = Detyping.detype Detyping.Now false avoiding env evd t in let nenv = { ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; @@ -521,7 +524,7 @@ let rec subst_pat subst pat = | PatVar _ -> pat | PatCstr (((kn,i),j),cpl,n) -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_pat subst) cpl in + and cpl' = List.Smart.map (subst_pat subst) cpl in if kn' == kn && cpl' == cpl then pat else DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n) @@ -536,7 +539,7 @@ let rec subst_notation_constr subst bound raw = | NApp (r,rl) -> let r' = subst_notation_constr subst bound r - and rl' = List.smartmap (subst_notation_constr subst bound) rl in + and rl' = List.Smart.map (subst_notation_constr subst bound) rl in if r' == r && rl' == rl then raw else NApp(r',rl') @@ -566,14 +569,14 @@ let rec subst_notation_constr subst bound raw = | NLetIn (n,r1,t,r2) -> let r1' = subst_notation_constr subst bound r1 in - let t' = Option.smartmap (subst_notation_constr subst bound) t in + let t' = Option.Smart.map (subst_notation_constr subst bound) t in let r2' = subst_notation_constr subst bound r2 in if r1' == r1 && t == t' && r2' == r2 then raw else NLetIn (n,r1',t',r2') | NCases (sty,rtntypopt,rl,branches) -> - let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt - and rl' = List.smartmap + let rtntypopt' = Option.Smart.map (subst_notation_constr subst bound) rtntypopt + and rl' = List.Smart.map (fun (a,(n,signopt) as x) -> let a' = subst_notation_constr subst bound a in let signopt' = Option.map (fun ((indkn,i),nal as z) -> @@ -581,9 +584,9 @@ let rec subst_notation_constr subst bound raw = if indkn == indkn' then z else ((indkn',i),nal)) signopt in if a' == a && signopt' == signopt then x else (a',(n,signopt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun (cpl,r as branch) -> - let cpl' = List.smartmap (subst_pat subst) cpl + let cpl' = List.Smart.map (subst_pat subst) cpl and r' = subst_notation_constr subst bound r in if cpl' == cpl && r' == r then branch else (cpl',r')) @@ -594,14 +597,14 @@ let rec subst_notation_constr subst bound raw = NCases (sty,rtntypopt',rl',branches') | NLetTuple (nal,(na,po),b,c) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po + let po' = Option.Smart.map (subst_notation_constr subst bound) po and b' = subst_notation_constr subst bound b and c' = subst_notation_constr subst bound c in if po' == po && b' == b && c' == c then raw else NLetTuple (nal,(na,po'),b',c') | NIf (c,(na,po),b1,b2) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po + let po' = Option.Smart.map (subst_notation_constr subst bound) po and b1' = subst_notation_constr subst bound b1 and b2' = subst_notation_constr subst bound b2 and c' = subst_notation_constr subst bound c in @@ -610,12 +613,12 @@ let rec subst_notation_constr subst bound raw = | NRec (fk,idl,dll,tl,bl) -> let dll' = - Array.smartmap (List.smartmap (fun (na,oc,b as x) -> - let oc' = Option.smartmap (subst_notation_constr subst bound) oc in + Array.Smart.map (List.Smart.map (fun (na,oc,b as x) -> + let oc' = Option.Smart.map (subst_notation_constr subst bound) oc in let b' = subst_notation_constr subst bound b in if oc' == oc && b' == b then x else (na,oc',b'))) dll in - let tl' = Array.smartmap (subst_notation_constr subst bound) tl in - let bl' = Array.smartmap (subst_notation_constr subst bound) bl in + let tl' = Array.Smart.map (subst_notation_constr subst bound) tl in + let bl' = Array.Smart.map (subst_notation_constr subst bound) bl in if dll' == dll && tl' == tl && bl' == bl then raw else NRec (fk,idl,dll',tl',bl') @@ -628,7 +631,7 @@ let rec subst_notation_constr subst bound raw = if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) | _ -> knd in - let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in + let nsolve = Option.Smart.map (Genintern.generic_substitute subst) solve in if nsolve == solve && nknd == knd then raw else NHole (nknd, naming, nsolve) @@ -684,7 +687,7 @@ let is_onlybinding_meta id metas = let is_onlybinding_pattern_like_meta isvar id metas = try match Id.List.assoc id metas with | _,NtnTypeBinder (NtnBinderParsedAsConstr - (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true + (AsIdentOrPattern | AsStrictPattern)) -> true | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar) | _ -> false with Not_found -> false diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 1a46746cc9..52a6354a0c 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -62,6 +62,11 @@ type subscopes = tmp_scope_name option * scope_name list (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y *) +type constr_as_binder_kind = + | AsIdent + | AsIdentOrPattern + | AsStrictPattern + type notation_binder_source = (* This accepts only pattern *) (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *) @@ -69,7 +74,7 @@ type notation_binder_source = (* This accepts only ident *) | NtnParsedAsIdent (* This accepts ident, or pattern, or both *) - | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind + | NtnBinderParsedAsConstr of constr_as_binder_kind type notation_var_instance_type = | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList @@ -91,33 +96,3 @@ type notation_interp_env = { ninterp_var_type : notation_var_internalization_type Id.Map.t; ninterp_rec_vars : Id.t Id.Map.t; } - -type grammar_constr_prod_item = - | GramConstrTerminal of Tok.t - | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool * int - (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list when true; additionally release - the p last items as if they were parsed autonomously *) - -(** Dealing with precedences *) - -type precedence = int -type parenRelation = L | E | Any | Prec of precedence -type tolerability = precedence * parenRelation - -type level = precedence * tolerability list * Extend.constr_entry_key list - -(** Grammar rules for a notation *) - -type one_notation_grammar = { - notgram_level : level; - notgram_assoc : Extend.gram_assoc option; - notgram_notation : Constrexpr.notation; - notgram_prods : grammar_constr_prod_item list list; -} - -type notation_grammar = { - notgram_onlyprinting : bool; - notgram_rules : one_notation_grammar list -} 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 b57103cf22..071248f01f 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -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/syntax_def.ml b/interp/syntax_def.ml index 47faa5885c..a4f20fd739 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -96,13 +96,13 @@ let warn_compatibility_notation = CWarnings.(create ~name:"compatibility-notation" ~category:"deprecated" ~default:Enabled pr_compat_warning) -let verbose_compat kn def = function +let verbose_compat ?loc kn def = function | Some v when Flags.version_strictly_greater v -> - warn_compatibility_notation (kn, def, v) + warn_compatibility_notation ?loc (kn, def, v) | _ -> () -let search_syntactic_definition kn = +let search_syntactic_definition ?loc kn = let pat,v = KNmap.find kn !syntax_table in let def = out_pat pat in - verbose_compat kn def v; + verbose_compat ?loc kn def v; def diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 1933b8a9ae..c5b6655ff8 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -18,4 +18,4 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr val declare_syntactic_definition : bool -> Id.t -> Flags.compat_version option -> syndef_interpretation -> unit -val search_syntactic_definition : KerName.t -> syndef_interpretation +val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation diff --git a/interp/topconstr.ml b/interp/topconstr.ml deleted file mode 100644 index 7d2d75d9cb..0000000000 --- a/interp/topconstr.ml +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Constrexpr_ops - -let asymmetric_patterns = asymmetric_patterns -let error_invalid_pattern_notation = error_invalid_pattern_notation -let split_at_annot = split_at_annot -let ntn_loc = ntn_loc -let patntn_loc = patntn_loc -let map_constr_expr_with_binders = map_constr_expr_with_binders -let fold_constr_expr_with_binders = fold_constr_expr_with_binders -let ids_of_cases_indtype = ids_of_cases_indtype -let occur_var_constr_expr = occur_var_constr_expr -let free_vars_of_constr_expr = free_vars_of_constr_expr -let replace_vars_constr_expr = replace_vars_constr_expr diff --git a/interp/topconstr.mli b/interp/topconstr.mli deleted file mode 100644 index c86502015a..0000000000 --- a/interp/topconstr.mli +++ /dev/null @@ -1,53 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constrexpr - -(** Topconstr: This whole module is deprecated in favor of Constrexpr_ops *) -val asymmetric_patterns : bool ref -[@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"] - -(** Utilities on constr_expr *) -val split_at_annot : local_binder_expr list -> Misctypes.lident option -> local_binder_expr list * local_binder_expr list -[@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"] - -val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list -[@@ocaml.deprecated "use Constrexpr_ops.ntn_loc"] -val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list -[@@ocaml.deprecated "use Constrexpr_ops.patntn_loc"] - -(** For cases pattern parsing errors *) -val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a -[@@ocaml.deprecated "use Constrexpr_ops.error_invalid_pattern_notation"] - -(*************************************************************************) -val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr -[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] - -val free_vars_of_constr_expr : constr_expr -> Id.Set.t -[@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] - -val occur_var_constr_expr : Id.t -> constr_expr -> bool -[@@ocaml.deprecated "use Constrexpr_ops.occur_var_constr_expr"] - -(** Specific function for interning "in indtype" syntax of "match" *) -val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t -[@@ocaml.deprecated "use Constrexpr_ops.ids_of_cases_indtype"] - -(** Used in typeclasses *) -val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> - ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b -[@@ocaml.deprecated "use Constrexpr_ops.fold_constr_expr_with_binders"] - -val map_constr_expr_with_binders : - (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> - 'a -> constr_expr -> constr_expr -[@@ocaml.deprecated "use Constrexpr_ops.map_constr_expr_with_binders"] |