Merge PR #7570: [api] Move `Constrexpr` to the `interp` module.

16 files changed, 351 insertions, 222 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
new file mode 100644
index 000000000..ca6ea94f0
--- /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 3eb5acfc5..1be1dd96c 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -600,3 +600,35 @@ let _ = Goptions.declare_bool_option {
   Goptions.optread = (fun () -> !asymmetric_patterns);
   Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
 }
+
+(** 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 2df9e5a8c..b4f0886ac 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -116,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/constrintern.ml b/interp/constrintern.ml
index 3a88284e4..45c0e9c42 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -820,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')
diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
new file mode 100644
index 000000000..80697461a
--- /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/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 289890544..b48db9ac5 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*)
 
@@ -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 39d0174f9..e64c5c542 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -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 37a327a7d..3668455ae 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,6 @@
+Constrexpr
+Genredexpr
+Redops
 Tactypes
 Stdarg
 Genintern
@@ -7,7 +10,6 @@ Notation
 Syntax_def
 Smartlocate
 Constrexpr_ops
-Ppextend
 Dumpglob
 Reserve
 Impargs
diff --git a/interp/modintern.ml b/interp/modintern.ml
index dc93d8dc4..fefd2ab6f 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 192c477be..05fcd0e7f 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 =
@@ -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 ccc67fe49..b177b7f1e 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 b0480aa70..f208b23fb 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -687,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 1a46746cc..52a6354a0 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 c75d9e12f..000000000
--- 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 000000000..b9a74136e
--- /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 c81058e72..7254f29b2 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