aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml48
-rw-r--r--interp/constrextern.mli8
-rw-r--r--interp/constrintern.ml26
-rw-r--r--interp/constrintern.mli11
-rw-r--r--interp/declare.ml8
-rw-r--r--interp/declare.mli4
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--interp/dumpglob.mli8
-rw-r--r--interp/impargs.ml306
-rw-r--r--interp/impargs.mli11
-rw-r--r--interp/implicit_quantifiers.ml38
-rw-r--r--interp/implicit_quantifiers.mli7
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/notation.ml53
-rw-r--r--interp/notation.mli17
-rw-r--r--interp/notation_ops.ml50
-rw-r--r--interp/notation_term.ml123
-rw-r--r--interp/reserve.ml6
-rw-r--r--interp/smartlocate.mli8
-rw-r--r--interp/stdarg.mli7
20 files changed, 459 insertions, 283 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 19444988b9..7792eff664 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -14,7 +14,6 @@ open CErrors
open Util
open Names
open Nameops
-open Constr
open Termops
open Libnames
open Globnames
@@ -479,7 +478,8 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
if is_inactive_rule keyrule then raise No_match;
let loc = t.loc in
match DAst.get t with
- | PatCstr (cstr,_,na) ->
+ | PatCstr (cstr,args,na) ->
+ let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in
let p = apply_notation_to_pattern ?loc (ConstructRef cstr)
(match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
insert_pat_alias ?loc p na
@@ -590,11 +590,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
@@ -1223,8 +1229,36 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
in
GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
- | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
- | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
+ | PFix ((ln,i),(lna,tl,bl)) ->
+ let def_avoid, def_env, lfi =
+ Array.fold_left
+ (fun (avoid, env, l) na ->
+ let id = Namegen.next_name_away na avoid in
+ (Id.Set.add id avoid, Name id :: env, id::l))
+ (avoid, env, []) lna in
+ let n = Array.length tl in
+ let v = Array.map3
+ (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t))
+ bl tl ln in
+ GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi),
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
+ | PCoFix (ln,(lna,tl,bl)) ->
+ let def_avoid, def_env, lfi =
+ Array.fold_left
+ (fun (avoid, env, l) na ->
+ let id = Namegen.next_name_away na avoid in
+ (Id.Set.add id avoid, Name id :: env, id::l))
+ (avoid, env, []) lna in
+ let ntys = Array.length tl in
+ let v = Array.map2
+ (fun c t -> share_pattern_names glob_of_pat 0 [] def_avoid def_env sigma c (Patternops.lift_pattern ntys t))
+ bl tl in
+ GRec(GCoFix ln,Array.of_list (List.rev lfi),
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
| PSort s -> GSort s
let extern_constr_pattern env sigma pat =
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 8ab70283c8..73c108319f 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -13,13 +13,11 @@ open Termops
open EConstr
open Environ
open Libnames
-open Globnames
open Glob_term
open Pattern
open Constrexpr
open Notation_term
open Notation
-open Misctypes
open Ltac_pretype
(** Translation of pattern, cases pattern, glob_constr and term into syntax
@@ -40,7 +38,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
+val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference
val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
val extern_rel_context : constr option -> env -> Evd.evar_map ->
@@ -58,9 +56,9 @@ val print_projections : bool ref
(** Customization of the global_reference printer *)
val set_extern_reference :
- (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
+ (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) -> unit
val get_extern_reference :
- unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
+ unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference)
(** WARNING: The following functions are evil due to
side-effects. Think of the following case as used in the printer:
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f2cd07c94e..48f15f8979 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -433,7 +433,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
(na,bk,Some c,t)
| GLocalPattern (_,_,_,_) ->
- Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.")
+ Loc.raise ?loc (Stream.Error "pattern with quote not allowed here")
)
let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
@@ -980,17 +980,17 @@ let intern_reference ref =
in
Smartlocate.global_of_extended_global r
-let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option =
+let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option =
match info with
- | Misctypes.UAnonymous -> None
- | Misctypes.UUnknown -> None
- | Misctypes.UNamed id -> Some (id, 0)
+ | UAnonymous -> None
+ | UUnknown -> None
+ | UNamed id -> Some (id, 0)
-let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort =
+let glob_sort_of_level (level: glob_level) : glob_sort =
match level with
- | Misctypes.GProp -> Misctypes.GProp
- | Misctypes.GSet -> Misctypes.GSet
- | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info]
+ | GProp -> GProp
+ | GSet -> GSet
+ | GType info -> GType [sort_info_of_level_info info]
(* Is it a global reference or a syntactic definition? *)
let intern_qualid qid intern env ntnvars us args =
@@ -1024,7 +1024,7 @@ let intern_qualid qid intern env ntnvars us args =
DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
| _ -> err ()
end
- | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+ | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
| Some [_old_level], GSort _new_sort ->
(* TODO: add old_level and new_sort to the error message *)
user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v)
@@ -1077,7 +1077,7 @@ let interp_reference vars r =
(** Private internalization patterns *)
type 'a raw_cases_pattern_expr_r =
| RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
- | RCPatCstr of Globnames.global_reference
+ | RCPatCstr of GlobRef.t
* 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
(** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
| RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
@@ -1314,7 +1314,7 @@ let sort_fields ~complete loc fields completer =
| [] -> (idx, acc_first_idx, acc)
| (Some field_glob_id) :: projs ->
let field_glob_ref = ConstRef field_glob_id in
- let first_field = eq_gr field_glob_ref first_field_glob_ref in
+ let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
begin match proj_kinds with
| [] -> anomaly (Pp.str "Number of projections mismatch.")
| (_, regular) :: proj_kinds ->
@@ -1352,7 +1352,7 @@ let sort_fields ~complete loc fields completer =
user_err ?loc ~hdr:"intern"
(str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
let remaining_projs, (field_index, _) =
- let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
+ let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
try CList.extract_first the_proj remaining_projs
with Not_found ->
user_err ?loc
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f5e32dc4cd..4dd719e1f3 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -13,7 +13,6 @@ open Evd
open Environ
open Misctypes
open Libnames
-open Globnames
open Glob_term
open Pattern
open EConstr
@@ -143,7 +142,7 @@ val intern_constr_pattern :
constr_pattern_expr -> patvar list * constr_pattern
(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
-val intern_reference : reference -> global_reference
+val intern_reference : reference -> GlobRef.t
(** Expands abbreviations (syndef); raise an error if not existing *)
val interp_reference : ltac_sign -> reference -> glob_constr
@@ -175,11 +174,11 @@ val interp_context_evars :
(** Locating references of constructions, possibly via a syntactic definition
(these functions do not modify the glob file) *)
-val locate_reference : Libnames.qualid -> Globnames.global_reference
+val locate_reference : Libnames.qualid -> GlobRef.t
val is_global : Id.t -> bool
-val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference
-val global_reference : Id.t -> Globnames.global_reference
-val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference
+val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> GlobRef.t
+val global_reference : Id.t -> GlobRef.t
+val global_reference_in_absolute_module : DirPath.t -> Id.t -> GlobRef.t
(** Interprets a term as the left-hand side of a notation. The returned map is
guaranteed to have the same domain as the input one. *)
diff --git a/interp/declare.ml b/interp/declare.ml
index c55a6c69ba..bc2d2068a2 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -487,7 +487,7 @@ let add_universe src (dp, i) =
Option.iter (fun poly ->
let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
Global.push_context_set poly ctx;
- Universes.add_global_universe level poly;
+ UnivNames.add_global_universe level poly;
if poly then Lib.add_section_context ctx)
optpoly
@@ -538,7 +538,7 @@ let input_universe : universe_decl -> Libobject.obj =
let declare_univ_binders gr pl =
if Global.is_polymorphic gr then
- Universes.register_universe_binders gr pl
+ UnivNames.register_universe_binders gr pl
else
let l = match gr with
| ConstRef c -> Label.to_id @@ Constant.label c
@@ -564,7 +564,7 @@ let do_universe poly l =
in
let l =
List.map (fun {CAst.v=id} ->
- let lev = Universes.new_univ_id () in
+ let lev = UnivGen.new_univ_id () in
(id, lev)) l
in
let src = if poly then BoundUniv else UnqualifiedUniv in
@@ -595,7 +595,7 @@ let input_constraints : constraint_decl -> Libobject.obj =
let do_constraint poly l =
let u_of_id x =
let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
- Universes.is_polymorphic level, level
+ UnivNames.is_polymorphic level, level
in
let in_section = Lib.sections_are_opened () in
let () =
diff --git a/interp/declare.mli b/interp/declare.mli
index 084d746e68..4a9f542783 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -83,10 +83,10 @@ val recursive_message : bool (** true = fixpoint *) ->
val exists_name : Id.t -> bool
(** Global universe contexts, names and constraints *)
-val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit
+val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
val do_universe : polymorphic -> Misctypes.lident list -> unit
-val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
+val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list ->
unit
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index bc6a1ef3aa..74618a2905 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -254,7 +254,7 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc ->
let dump_definition {CAst.loc;v=id} sec s =
dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
-let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty =
+let dump_constraint { CAst.loc; v = n } sec ty =
match n with
| Names.Name id -> dump_definition CAst.(make ?loc id) sec ty
| Names.Anonymous -> ()
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 43c100008c..bf83d2df40 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -24,7 +24,7 @@ val feedback_glob : unit -> unit
val pause : unit -> unit
val continue : unit -> unit
-val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
+val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
val dump_definition : Misctypes.lident -> bool -> string -> unit
@@ -38,9 +38,9 @@ val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit
val dump_notation :
(Constrexpr.notation * Notation.notation_location) Loc.located ->
Notation_term.scope_name option -> bool -> unit
-val dump_constraint :
- Vernacexpr.typeclass_constraint -> bool -> string -> unit
+
+val dump_constraint : Misctypes.lname -> bool -> string -> unit
val dump_string : string -> unit
-val type_of_global_ref : Globnames.global_reference -> string
+val type_of_global_ref : Names.GlobRef.t -> string
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 9ad62c0de3..8aa1e62504 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -139,7 +139,7 @@ let argument_less = function
| Hyp _, Conclusion -> true
| Conclusion, _ -> false
-let update pos rig (na,st) =
+let update pos rig st =
let e =
if rig then
match st with
@@ -163,7 +163,7 @@ let update pos rig (na,st) =
| Some (DepFlex fpos as x) ->
if argument_less (pos,fpos) then DepFlex pos else x
| Some Manual -> assert false
- in na, Some e
+ in Some e
(* modified is_rigid_reference with a truncated env *)
let is_flexible_reference env sigma bound depth f =
@@ -214,6 +214,8 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in
acc
+(* compute the list of implicit arguments *)
+
let rec is_rigid_head sigma t = match kind sigma t with
| Rel _ | Evar _ -> false
| Ind _ | Const _ | Var _ | Sort _ -> true
@@ -226,51 +228,69 @@ let rec is_rigid_head sigma t = match kind sigma t with
| Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
| Prod _ | Meta _ | Cast _ -> assert false
-(* calcule la liste des arguments implicites *)
+let is_rigid env sigma t =
+ let open Context.Rel.Declaration in
+ let t = whd_all env sigma t in
+ match kind sigma t with
+ | Prod (na,a,b) ->
+ let (_,t) = splay_prod (push_rel (LocalAssum (na,a)) env) sigma b in
+ is_rigid_head sigma t
+ | _ -> true
-let find_displayed_name_in all avoid na (env, b) =
+let find_displayed_name_in sigma all avoid na (env, b) =
let envnames_b = (env, b) in
let flag = RenamingElsewhereFor envnames_b in
- if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
- else compute_displayed_name_in Evd.empty flag avoid na b
+ if all then compute_and_force_displayed_name_in sigma flag avoid na b
+ else compute_displayed_name_in sigma flag avoid na b
+
+let compute_implicits_names_gen all env sigma t =
+ let open Context.Rel.Declaration in
+ let rec aux env avoid names t =
+ let t = whd_all env sigma t in
+ match kind sigma t with
+ | Prod (na,a,b) ->
+ let na',avoid' = find_displayed_name_in sigma all avoid na (names,b) in
+ aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b
+ | _ -> List.rev names
+ in aux env Id.Set.empty [] t
+
+let compute_implicits_names = compute_implicits_names_gen true
-let compute_implicits_gen strict strongly_strict revpat contextual all env sigma (t : EConstr.t) =
- let rigid = ref true in
+let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t =
let open Context.Rel.Declaration in
- let rec aux env avoid n names (t : EConstr.t) =
+ let rec aux env n t =
let t = whd_all env sigma t in
match kind sigma t with
- | Prod (na,a,b) ->
- let na',avoid' = find_displayed_name_in all avoid na (names,b) in
- add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1))
- (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b)
- | _ ->
- rigid := is_rigid_head sigma t;
- let names = List.rev names in
- let v = Array.map (fun na -> na,None) (Array.of_list names) in
- if contextual then
- add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v
- else v
+ | Prod (na,a,b) ->
+ add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1))
+ (aux (push_rel (LocalAssum (na,a)) env) (n+1) b)
+ | _ ->
+ let v = Array.make n None in
+ if contextual then
+ add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v
+ else v
in
match kind sigma (whd_all env sigma t) with
- | Prod (na,a,b) ->
- let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in
- let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
- !rigid, Array.to_list v
- | _ -> true, []
+ | Prod (na,a,b) ->
+ let v = aux (push_rel (LocalAssum (na,a)) env) 1 b in
+ Array.to_list v
+ | _ -> []
-let compute_implicits_flags env sigma f all t =
- compute_implicits_gen
+let compute_implicits_explanation_flags env sigma f t =
+ compute_implicits_explanation_gen
(f.strict || f.strongly_strict) f.strongly_strict
- f.reversible_pattern f.contextual all env sigma t
+ f.reversible_pattern f.contextual env sigma t
-let compute_auto_implicits env sigma flags enriching t =
- if enriching then compute_implicits_flags env sigma flags true t
- else compute_implicits_gen false false false true true env sigma t
+let compute_implicits_flags env sigma f all t =
+ List.combine
+ (compute_implicits_names_gen all env sigma t)
+ (compute_implicits_explanation_flags env sigma f t)
-let compute_implicits_names env sigma t =
- let _, impls = compute_implicits_gen false false false false true env sigma t in
- List.map fst impls
+let compute_auto_implicits env sigma flags enriching t =
+ List.combine
+ (compute_implicits_names env sigma t)
+ (if enriching then compute_implicits_explanation_flags env sigma flags t
+ else compute_implicits_explanation_gen false false false true env sigma t)
(* Extra information about implicit arguments *)
@@ -329,13 +349,16 @@ let rec prepare_implicits f = function
Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
| _::imps -> None :: prepare_implicits f imps
-let set_implicit id imp insmax =
- (id,(match imp with None -> Manual | Some imp -> imp),insmax)
-
-let rec assoc_by_pos k = function
- (ExplByPos (k', x), b) :: tl when Int.equal k k' -> (x,b), tl
- | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
- | [] -> raise Not_found
+(*
+If found, returns Some (x,(b,fi,fo)) and l with the entry removed,
+otherwise returns None and l unchanged.
+ *)
+let assoc_by_pos k l =
+ let rec aux = function
+ (ExplByPos (k', x), b) :: tl when Int.equal k k' -> Some (x,b), tl
+ | hd :: tl -> let (x, tl) = aux tl in x, hd :: tl
+ | [] -> raise Not_found
+ in try aux l with Not_found -> None, l
let check_correct_manual_implicits autoimps l =
List.iter (function
@@ -352,70 +375,65 @@ let check_correct_manual_implicits autoimps l =
(str "Cannot set implicit argument number " ++ int i ++
str ": it has no name.")) l
-let set_manual_implicits env flags enriching autoimps l =
- let try_forced k l =
- try
- let (id, (b, fi, fo)), l' = assoc_by_pos k l in
- if fo then
- let id = match id with Some id -> id | None -> Id.of_string ("arg_" ^ string_of_int k) in
- l', Some (id,Manual,(b,fi))
- else l, None
- with Not_found -> l, None
- in
+(* Take a list l of explicitations, and map them to positions. *)
+let flatten_explicitations l autoimps =
+ let rec aux k l = function
+ | (Name id,_)::imps ->
+ let value, l' =
+ try
+ let eq = explicitation_eq in
+ let flags = List.assoc_f eq (ExplByName id) l in
+ Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l
+ with Not_found -> assoc_by_pos k l
+ in value :: aux (k+1) l' imps
+ | (Anonymous,_)::imps ->
+ let value, l' = assoc_by_pos k l
+ in value :: aux (k+1) l' imps
+ | [] when List.is_empty l -> []
+ | [] ->
+ check_correct_manual_implicits autoimps l;
+ []
+ in aux 1 l autoimps
+
+let set_manual_implicits flags enriching autoimps l =
if not (List.distinct l) then
user_err Pp.(str "Some parameters are referred more than once.");
(* Compare with automatic implicits to recover printing data and names *)
- let rec merge k l = function
- | (Name id,imp)::imps ->
- let l',imp,m =
- try
- let eq = explicitation_eq in
- let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in
- List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi))
- with Not_found ->
- try
- let (id, (b, fi, fo)), l' = assoc_by_pos k l in
- l', (Some Manual), (Some (b,fi))
- with Not_found ->
- let m = match enriching, imp with
- | true, Some _ -> Some (flags.maximal, true)
- | _ -> None
- in
- l, imp, m
- in
- let imps' = merge (k+1) l' imps in
- let m = Option.map (fun (b,f) ->
- (* match imp with Some Manual -> (b,f) *)
- (* | _ -> *)set_maximality imps' b, f) m in
- Option.map (set_implicit id imp) m :: imps'
- | (Anonymous,imp)::imps ->
- let l', forced = try_forced k l in
- forced :: merge (k+1) l' imps
- | [] when begin match l with [] -> true | _ -> false end -> []
- | [] ->
- check_correct_manual_implicits autoimps l;
- []
- in
- merge 1 l autoimps
-
-let compute_semi_auto_implicits env sigma f manual t =
- match manual with
- | [] ->
- if not f.auto then [DefaultImpArgs, []]
- else let _,l = compute_implicits_flags env sigma f false t in
- [DefaultImpArgs, prepare_implicits f l]
- | _ ->
- let _,autoimpls = compute_auto_implicits env sigma f f.auto t in
- [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual]
+ let rec merge k autoimps explimps = match autoimps, explimps with
+ | autoimp::autoimps, explimp::explimps ->
+ let imps' = merge (k+1) autoimps explimps in
+ begin match autoimp, explimp with
+ | (Name id,_), Some (_, (b, fi, _)) ->
+ Some (id, Manual, (set_maximality imps' b, fi))
+ | (Name id,Some exp), None when enriching ->
+ Some (id, exp, (set_maximality imps' flags.maximal, true))
+ | (Name _,_), None -> None
+ | (Anonymous,_), Some (Some id, (b, fi, true)) ->
+ Some (id,Manual,(b,fi))
+ | (Anonymous,_), Some (None, (b, fi, true)) ->
+ let id = Id.of_string ("arg_" ^ string_of_int k) in
+ Some (id,Manual,(b,fi))
+ | (Anonymous,_), Some (_, (_, _, false)) -> None
+ | (Anonymous,_), None -> None
+ end :: imps'
+ | [], [] -> []
+ (* flatten_explicitations returns a list of the same length as autoimps *)
+ | _ -> assert false
+ in merge 1 autoimps (flatten_explicitations l autoimps)
+
+let compute_semi_auto_implicits env sigma f t =
+ if not f.auto then [DefaultImpArgs, []]
+ else let l = compute_implicits_flags env sigma f false t in
+ [DefaultImpArgs, prepare_implicits f l]
(*s Constants. *)
-let compute_constant_implicits flags manual cst =
+let compute_constant_implicits flags cst =
let env = Global.env () in
let sigma = Evd.from_env env in
let cb = Environ.lookup_constant cst env in
let ty = of_constr cb.const_type in
- let impls = compute_semi_auto_implicits env sigma flags manual ty in
+ let impls = compute_semi_auto_implicits env sigma flags ty in
impls
(*s Inductives and constructors. Their implicit arguments are stored
@@ -423,7 +441,7 @@ let compute_constant_implicits flags manual cst =
$i$ are the implicit arguments of the inductive and $v$ the array of
implicit arguments of the constructors. *)
-let compute_mib_implicits flags manual kn =
+let compute_mib_implicits flags kn =
let env = Global.env () in
let sigma = Evd.from_env env in
let mib = Environ.lookup_mind kn env in
@@ -439,34 +457,34 @@ let compute_mib_implicits flags manual kn =
let imps_one_inductive i mip =
let ind = (kn,i) in
let ar, _ = Global.type_of_global_in_context env (IndRef ind) in
- ((IndRef ind,compute_semi_auto_implicits env sigma flags manual (of_constr ar)),
+ ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)),
Array.mapi (fun j c ->
- (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags manual c))
+ (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c))
(Array.map of_constr mip.mind_nf_lc))
in
Array.mapi imps_one_inductive mib.mind_packets
-let compute_all_mib_implicits flags manual kn =
- let imps = compute_mib_implicits flags manual kn in
+let compute_all_mib_implicits flags kn =
+ let imps = compute_mib_implicits flags kn in
List.flatten
(Array.map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps)
(*s Variables. *)
-let compute_var_implicits flags manual id =
+let compute_var_implicits flags id =
let env = Global.env () in
let sigma = Evd.from_env env in
- compute_semi_auto_implicits env sigma flags manual (NamedDecl.get_type (lookup_named id env))
+ compute_semi_auto_implicits env sigma flags (NamedDecl.get_type (lookup_named id env))
(* Implicits of a global reference. *)
-let compute_global_implicits flags manual = function
- | VarRef id -> compute_var_implicits flags manual id
- | ConstRef kn -> compute_constant_implicits flags manual kn
+let compute_global_implicits flags = function
+ | VarRef id -> compute_var_implicits flags id
+ | ConstRef kn -> compute_constant_implicits flags kn
| IndRef (kn,i) ->
- let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps
+ let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps
| ConstructRef ((kn,i),j) ->
- let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1)
+ let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1)
(* Merge a manual explicitation with an implicit_status list *)
@@ -487,7 +505,7 @@ type implicit_discharge_request =
| ImplLocal
| ImplConstant of Constant.t * implicits_flags
| ImplMutualInductive of MutInd.t * implicits_flags
- | ImplInteractive of global_reference * implicits_flags *
+ | ImplInteractive of GlobRef.t * implicits_flags *
implicit_interactive_request
let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
@@ -520,7 +538,7 @@ let subst_implicits_decl subst (r,imps as o) =
let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
let subst_implicits (subst,(req,l)) =
- (ImplLocal,List.smartmap (subst_implicits_decl subst) l)
+ (ImplLocal,List.Smart.map (subst_implicits_decl subst) l)
let impls_of_context ctx =
let map (decl, impl) = match impl with
@@ -573,34 +591,34 @@ let rebuild_implicits (req,l) =
| ImplLocal -> assert false
| ImplConstant (con,flags) ->
let oldimpls = snd (List.hd l) in
- let newimpls = compute_constant_implicits flags [] con in
+ let newimpls = compute_constant_implicits flags con in
req, [ConstRef con, List.map2 merge_impls oldimpls newimpls]
| ImplMutualInductive (kn,flags) ->
- let newimpls = compute_all_mib_implicits flags [] kn in
+ let newimpls = compute_all_mib_implicits flags kn in
let rec aux olds news =
- match olds, news with
- | (_, oldimpls) :: old, (gr, newimpls) :: tl ->
- (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl
- | [], [] -> []
- | _, _ -> assert false
+ match olds, news with
+ | (_, oldimpls) :: old, (gr, newimpls) :: tl ->
+ (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl
+ | [], [] -> []
+ | _, _ -> assert false
in req, aux l newimpls
| ImplInteractive (ref,flags,o) ->
(if isVarRef ref && is_in_section ref then ImplLocal else req),
match o with
| ImplAuto ->
- let oldimpls = snd (List.hd l) in
- let newimpls = compute_global_implicits flags [] ref in
- [ref,List.map2 merge_impls oldimpls newimpls]
+ let oldimpls = snd (List.hd l) in
+ let newimpls = compute_global_implicits flags ref in
+ [ref,List.map2 merge_impls oldimpls newimpls]
| ImplManual userimplsize ->
- let oldimpls = snd (List.hd l) in
- if flags.auto then
- let newimpls = List.hd (compute_global_implicits flags [] ref) in
- let p = List.length (snd newimpls) - userimplsize in
- let newimpls = on_snd (List.firstn p) newimpls in
- [ref,List.map (fun o -> merge_impls o newimpls) oldimpls]
- else
- [ref,oldimpls]
+ let oldimpls = snd (List.hd l) in
+ if flags.auto then
+ let newimpls = List.hd (compute_global_implicits flags ref) in
+ let p = List.length (snd newimpls) - userimplsize in
+ let newimpls = on_snd (List.firstn p) newimpls in
+ [ref,List.map (fun o -> merge_impls o newimpls) oldimpls]
+ else
+ [ref,oldimpls]
let classify_implicits (req,_ as obj) = match req with
| ImplLocal -> Dispose
@@ -608,7 +626,7 @@ let classify_implicits (req,_ as obj) = match req with
type implicits_obj =
implicit_discharge_request *
- (global_reference * implicits_list list) list
+ (GlobRef.t * implicits_list list) list
let inImplicits : implicits_obj -> obj =
declare_object {(default_object "IMPLICITS") with
@@ -622,7 +640,7 @@ let inImplicits : implicits_obj -> obj =
let is_local local ref = local || isVarRef ref && is_in_section ref
let declare_implicits_gen req flags ref =
- let imps = compute_global_implicits flags [] ref in
+ let imps = compute_global_implicits flags ref in
add_anonymous_leaf (inImplicits (req,[ref,imps]))
let declare_implicits local ref =
@@ -643,7 +661,7 @@ let declare_mib_implicits kn =
let flags = !implicit_args in
let imps = Array.map_to_list
(fun (ind,cstrs) -> ind::(Array.to_list cstrs))
- (compute_mib_implicits flags [] kn) in
+ (compute_mib_implicits flags kn) in
add_anonymous_leaf
(inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
@@ -653,8 +671,8 @@ type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
type manual_implicits = manual_explicitation list
let compute_implicits_with_manual env sigma typ enriching l =
- let _,autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
- set_manual_implicits env !implicit_args enriching autoimpls l
+ let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
+ set_manual_implicits !implicit_args enriching autoimpls l
let check_inclusion l =
(* Check strict inclusion *)
@@ -679,26 +697,26 @@ let declare_manual_implicits local ref ?enriching l =
let env = Global.env () in
let sigma = Evd.from_env env in
let t, _ = Global.type_of_global_in_context env ref in
+ let t = of_constr t in
let enriching = Option.default flags.auto enriching in
- let isrigid,autoimpls = compute_auto_implicits env sigma flags enriching (of_constr t) in
+ let autoimpls = compute_auto_implicits env sigma flags enriching t in
let l' = match l with
| [] -> assert false
| [l] ->
- [DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l]
+ [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l]
| _ ->
- check_rigidity isrigid;
- let l = List.map (fun imps -> (imps,List.length imps)) l in
- let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
- check_inclusion l;
- let nargs = List.length autoimpls in
- List.map (fun (imps,n) ->
- (LessArgsThan (nargs-n),
- set_manual_implicits env flags enriching autoimpls imps)) l in
+ check_rigidity (is_rigid env sigma t);
+ let l = List.map (fun imps -> (imps,List.length imps)) l in
+ let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
+ check_inclusion l;
+ let nargs = List.length autoimpls in
+ List.map (fun (imps,n) ->
+ (LessArgsThan (nargs-n),
+ set_manual_implicits flags enriching autoimpls imps)) l in
let req =
if is_local local ref then ImplLocal
else ImplInteractive(ref,flags,ImplManual (List.length autoimpls))
- in
- add_anonymous_leaf (inImplicits (req,[ref,l']))
+ in add_anonymous_leaf (inImplicits (req,[ref,l']))
let maybe_declare_manual_implicits local ref ?enriching l =
match l with
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 1eeb8e41ae..ea5aa90f68 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -10,7 +10,6 @@
open Names
open EConstr
-open Globnames
open Environ
(** {6 Implicit Arguments } *)
@@ -103,7 +102,7 @@ val declare_var_implicits : variable -> unit
val declare_constant_implicits : Constant.t -> unit
val declare_mib_implicits : MutInd.t -> unit
-val declare_implicits : bool -> global_reference -> unit
+val declare_implicits : bool -> GlobRef.t -> unit
(** [declare_manual_implicits local ref enriching l]
Manual declaration of which arguments are expected implicit.
@@ -111,15 +110,15 @@ val declare_implicits : bool -> global_reference -> unit
implicits depending on the current state.
Unsets implicits if [l] is empty. *)
-val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
+val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
manual_implicits list -> unit
(** If the list is empty, do nothing, otherwise declare the implicits. *)
-val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
+val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
manual_implicits -> unit
-val implicits_of_global : global_reference -> implicits_list list
+val implicits_of_global : GlobRef.t -> implicits_list list
val extract_impargs_data :
implicits_list list -> ((int * int) option * implicit_status list) list
@@ -130,7 +129,7 @@ val make_implicits_list : implicit_status list -> implicits_list list
val drop_first_implicits : int -> implicits_list -> implicits_list
-val projection_implicits : env -> projection -> implicit_status list ->
+val projection_implicits : env -> Projection.t -> implicit_status list ->
implicit_status list
val select_impargs_size : int -> implicits_list list -> implicit_status list
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a1a3be70f1..289890544f 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -58,7 +58,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
@@ -245,6 +245,12 @@ let implicit_application env ?(allow_partial=true) f ty =
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 +266,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..39d0174f99 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -12,9 +12,8 @@ open Names
open Glob_term
open Constrexpr
open Libnames
-open Globnames
-val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit
+val declare_generalizable : local:bool -> Misctypes.lident list option -> unit
val ids_of_list : Id.t list -> Id.Set.t
val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
@@ -39,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
val combine_params_freevar :
- Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
+ Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t ->
Constrexpr.constr_expr * Id.Set.t
val implicit_application : Id.Set.t -> ?allow_partial:bool ->
- (Id.Set.t -> global_reference option * Context.Rel.Declaration.t ->
+ (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t ->
Constrexpr.constr_expr * Id.Set.t) ->
constr_expr -> constr_expr * Id.Set.t
diff --git a/interp/interp.mllib b/interp/interp.mllib
index bb22cf468d..61313acc48 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,6 +1,7 @@
Tactypes
Stdarg
Genintern
+Notation_term
Notation_ops
Notation
Syntax_def
diff --git a/interp/notation.ml b/interp/notation.ml
index 47d6481350..192c477be7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -49,7 +49,6 @@ type notation_location = (DirPath.t * DirPath.t) * string
type notation_data = {
not_interp : interpretation;
not_location : notation_location;
- not_onlyprinting : bool;
}
type scope = {
@@ -259,7 +258,7 @@ type interp_rule =
according to the key of the pattern (adapted from Chet Murthy by HH) *)
type key =
- | RefKey of global_reference
+ | RefKey of GlobRef.t
| Oth
let key_compare k1 k2 = match k1, k2 with
@@ -430,13 +429,15 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
(* Uninterpreted notation levels *)
-let declare_notation_level ntn level =
+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 !notation_level_map
+ notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map
-let level_of_notation ntn =
- String.Map.find ntn !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 *)
@@ -449,20 +450,21 @@ let warn_notation_overridden =
let declare_notation_interpretation ntn scopt pat df ~onlyprint =
let scope = match scopt with Some s -> s | None -> default_scope in
let sc = find_scope scope in
- let () =
- if String.Map.mem ntn sc.notations then
- let which_scope = match scopt with
- | None -> mt ()
- | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
- warn_notation_overridden (ntn,which_scope)
- in
- let notdata = {
- not_interp = pat;
- not_location = df;
- not_onlyprinting = onlyprint;
- } in
- let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
- let () = scope_map := String.Map.add scope sc !scope_map in
+ if not onlyprint then begin
+ let () =
+ if String.Map.mem ntn sc.notations then
+ let which_scope = match scopt with
+ | None -> mt ()
+ | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
+ warn_notation_overridden (ntn,which_scope)
+ in
+ let notdata = {
+ not_interp = pat;
+ not_location = df;
+ } in
+ let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
+ scope_map := String.Map.add scope sc !scope_map
+ end;
begin match scopt with
| None -> scope_stack := SingleNotation ntn :: !scope_stack
| Some _ -> ()
@@ -487,7 +489,6 @@ let rec find_interpretation ntn find = function
let find_notation ntn sc =
let n = String.Map.find ntn (find_scope sc).notations in
- let () = if n.not_onlyprinting then raise Not_found in
(n.not_interp, n.not_location)
let notation_of_prim_token = function
@@ -631,7 +632,6 @@ let exists_notation_in_scope scopt ntn onlyprint r =
try
let sc = String.Map.find scope !scope_map in
let n = String.Map.find ntn sc.notations in
- onlyprint = n.not_onlyprinting &&
interpretation_eq n.not_interp r
with Not_found -> false
@@ -741,7 +741,7 @@ let subst_arguments_scope (subst,(req,r,n,scl,cls)) =
match subst_scope_class subst cl with
| Some cl' as ocl' when cl' != cl -> ocl'
| _ -> ocl in
- let cls' = List.smartmap subst_cl cls in
+ let cls' = List.Smart.map subst_cl cls in
(ArgsScopeNoDischarge,r',n,scl,cls')
let discharge_arguments_scope (_,(req,r,n,l,_)) =
@@ -778,7 +778,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
(req,r,0,l1@l,cls1)
type arguments_scope_obj =
- arguments_scope_discharge_request * global_reference *
+ arguments_scope_discharge_request * GlobRef.t *
(* Used to communicate information from discharge to rebuild *)
(* set to 0 otherwise *) int *
scope_name option list * scope_class option list
@@ -1051,7 +1051,7 @@ let locate_notation prglob ntn scope =
| [] -> str "Unknown notation"
| _ ->
str "Notation" ++ fnl () ++
- prlist (fun (ntn,l) ->
+ prlist_with_sep fnl (fun (ntn,l) ->
let scope = find_default ntn scopes in
prlist
(fun (sc,r,(_,df)) ->
@@ -1060,8 +1060,7 @@ let locate_notation prglob ntn scope =
(if String.equal sc default_scope then mt ()
else (spc () ++ str ": " ++ str sc)) ++
(if Option.equal String.equal (Some sc) scope
- then spc () ++ str "(default interpretation)" else mt ())
- ++ fnl ()))
+ then spc () ++ str "(default interpretation)" else mt ())))
l) ntns
let collect_notation_in_scope scope sc known =
diff --git a/interp/notation.mli b/interp/notation.mli
index 6803a7e517..ccc67fe491 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -11,7 +11,6 @@
open Bigint
open Names
open Libnames
-open Globnames
open Constrexpr
open Glob_term
open Notation_term
@@ -91,7 +90,7 @@ val declare_string_interpreter : scope_name -> required_module ->
val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes ->
glob_constr * (notation_location * scope_name option)
(* This function returns a glob_const representing a pattern *)
-val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> unit) -> prim_token ->
+val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) -> prim_token ->
local_scopes -> glob_constr * (notation_location * scope_name option)
(** Return the primitive token associated to a [term]/[cases_pattern];
@@ -138,13 +137,13 @@ val availability_of_notation : scope_name option * notation -> local_scopes ->
(** {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 *)
+val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
+val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
(** {6 Miscellaneous} *)
-val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> bool) ->
- notation -> delimiters option -> global_reference
+val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
+ notation -> delimiters option -> GlobRef.t
(** Checks for already existing notations *)
val exists_notation_in_scope : scope_name option -> notation ->
@@ -152,9 +151,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 +164,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
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index a0d69ce796..448881dcf9 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -28,7 +28,7 @@ open Notation_term
let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
-| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2
| NVar id1, NVar id2 -> (
match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
| Some n,Some m -> Int.equal n m
@@ -165,15 +165,15 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
| NApp (a,args) -> GApp (f e a, List.map (f e) args)
| NList (x,y,iter,tail,swap) ->
let t = f e tail in let it = f e iter in
- let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in
+ let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in
let inner = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in
- let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
+ let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in
DAst.get (subst_glob_vars outerl it)
| NBinderList (x,y,iter,tail,swap) ->
let t = f e tail in let it = f e iter in
- let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in
+ let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in
let inner = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in
- let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
+ let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in
DAst.get (subst_glob_vars outerl it)
| NLambda (na,ty,c) ->
let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
@@ -210,7 +210,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let e',na = protect g e na in
GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2)
| NRec (fk,idl,dll,tl,bl) ->
- let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) ->
+ let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) ->
let e,na = protect g e na in
(e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
@@ -509,7 +509,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 +523,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 +538,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 +568,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 +583,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 +596,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 +612,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 +630,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)
@@ -1123,7 +1125,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
(* Matching compositionally *)
| GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
- | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
+ | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma
| GApp (f1,l1), NApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
let f1,l1,f2,l2 =
@@ -1335,10 +1337,10 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
match DAst.get a1, a2 with
| r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
| PatVar Anonymous, NHole _ -> sigma,(0,[])
- | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
+ | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in
sigma,(0,l)
- | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
+ | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2)
when eq_constructor r1 r2 ->
let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in
let le2 = List.length l2 in
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
new file mode 100644
index 0000000000..1a46746cc9
--- /dev/null
+++ b/interp/notation_term.ml
@@ -0,0 +1,123 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Misctypes
+open Glob_term
+
+(** [notation_constr] *)
+
+(** [notation_constr] is the subtype of [glob_constr] allowed in syntactic
+ extensions (i.e. notations).
+ No location since intended to be substituted at any place of a text.
+ Complex expressions such as fixpoints and cofixpoints are excluded,
+ as well as non global expressions such as existential variables. *)
+
+type notation_constr =
+ (** Part common to [glob_constr] and [cases_pattern] *)
+ | NRef of GlobRef.t
+ | NVar of Id.t
+ | NApp of notation_constr * notation_constr list
+ | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
+ | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
+ (** Part only in [glob_constr] *)
+ | NLambda of Name.t * notation_constr * notation_constr
+ | NProd of Name.t * notation_constr * notation_constr
+ | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
+ | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
+ | NCases of Constr.case_style * notation_constr option *
+ (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
+ (cases_pattern list * notation_constr) list
+ | NLetTuple of Name.t list * (Name.t * notation_constr option) *
+ notation_constr * notation_constr
+ | NIf of notation_constr * (Name.t * notation_constr option) *
+ notation_constr * notation_constr
+ | NRec of fix_kind * Id.t array *
+ (Name.t * notation_constr option * notation_constr) list array *
+ notation_constr array * notation_constr array
+ | NSort of glob_sort
+ | NCast of notation_constr * notation_constr cast_type
+ | NProj of Projection.t * notation_constr
+
+(** Note concerning NList: first constr is iterator, second is terminator;
+ first id is where each argument of the list has to be substituted
+ in iterator and snd id is alternative name just for printing;
+ boolean is associativity *)
+
+(** Types concerning notations *)
+
+type scope_name = string
+
+type tmp_scope_name = scope_name
+
+type subscopes = tmp_scope_name option * scope_name list
+
+(** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
+ x carries the sequence of objects bound to the list x..y *)
+
+type 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 Extend.constr_as_binder_kind
+
+type notation_var_instance_type =
+ | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
+
+(** Type of variables when interpreting a constr_expr as a notation_constr:
+ in a recursive pattern x..y, both x and y carry the individual type
+ of each element of the list x..y *)
+type notation_var_internalization_type =
+ | NtnInternTypeAny | NtnInternTypeOnlyBinder
+
+(** This characterizes to what a notation is interpreted to *)
+type interpretation =
+ (Id.t * (subscopes * notation_var_instance_type)) list *
+ notation_constr
+
+type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list
+
+type notation_interp_env = {
+ ninterp_var_type : notation_var_internalization_type Id.Map.t;
+ ninterp_rec_vars : Id.t Id.Map.t;
+}
+
+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/reserve.ml b/interp/reserve.ml
index 36005121b1..071248f01f 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -22,7 +22,7 @@ open Notation_ops
open Globnames
type key =
- | RefKey of global_reference
+ | RefKey of GlobRef.t
| Oth
(** TODO: share code from Notation *)
@@ -112,7 +112,9 @@ let revert_reserved_type t =
let t = EConstr.Unsafe.to_constr t in
let reserved = KeyMap.find (constr_key t) !reserve_revtable in
let t = EConstr.of_constr t in
- let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let t = Detyping.detype Detyping.Now false Id.Set.empty env evd t in
(* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
then I've introduced a bug... *)
let filter _ pat =
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 7ff7e899e2..45037b8b36 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -18,22 +18,22 @@ open Misctypes
if not bound in the global env; raise a [UserError] if bound to a
syntactic def that does not denote a reference *)
-val locate_global_with_alias : ?head:bool -> qualid CAst.t -> global_reference
+val locate_global_with_alias : ?head:bool -> qualid CAst.t -> GlobRef.t
(** Extract a global_reference from a reference that can be an "alias" *)
-val global_of_extended_global : extended_global_reference -> global_reference
+val global_of_extended_global : extended_global_reference -> GlobRef.t
(** Locate a reference taking into account possible "alias" notations.
May raise [Nametab.GlobalizationError _] for an unknown reference,
or a [UserError] if bound to a syntactic def that does not denote
a reference. *)
-val global_with_alias : ?head:bool -> reference -> global_reference
+val global_with_alias : ?head:bool -> reference -> GlobRef.t
(** The same for inductive types *)
val global_inductive_with_alias : reference -> inductive
(** Locate a reference taking into account notations and "aliases" *)
-val smart_global : ?head:bool -> reference or_by_notation -> global_reference
+val smart_global : ?head:bool -> reference or_by_notation -> GlobRef.t
(** The same for inductive types *)
val smart_global_inductive : reference or_by_notation -> inductive
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 53d1a522d3..dc9c370a1b 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -14,7 +14,6 @@ open Loc
open Names
open EConstr
open Libnames
-open Globnames
open Genredexpr
open Pattern
open Constrexpr
@@ -42,7 +41,7 @@ val wit_ident : Id.t uniform_genarg_type
val wit_var : (lident, lident, Id.t) genarg_type
-val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
@@ -81,8 +80,8 @@ val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr,
val wit_integer : int uniform_genarg_type
val wit_preident : string uniform_genarg_type
-val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
-val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
+val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
+val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 09:01:12 +0000