aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml12
-rw-r--r--interp/constrexpr_ops.ml16
-rw-r--r--interp/constrexpr_ops.mli6
-rw-r--r--interp/constrextern.ml7
-rw-r--r--interp/constrintern.ml63
-rw-r--r--interp/constrintern.mli14
-rw-r--r--interp/declare.ml30
-rw-r--r--interp/dumpglob.mli1
-rw-r--r--interp/genredexpr.ml65
-rw-r--r--interp/impargs.ml2
-rw-r--r--interp/impargs.mli1
-rw-r--r--interp/interp.mllib2
-rw-r--r--interp/notation.ml314
-rw-r--r--interp/notation.mli28
-rw-r--r--interp/notation_ops.ml12
-rw-r--r--interp/notation_term.ml4
-rw-r--r--interp/redops.ml64
-rw-r--r--interp/redops.mli20
-rw-r--r--interp/stdarg.ml5
-rw-r--r--interp/stdarg.mli13
-rw-r--r--interp/syntax_def.ml7
-rw-r--r--interp/syntax_def.mli3
22 files changed, 347 insertions, 342 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 77d612cfd9..757d186c8b 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -80,8 +80,8 @@ type cases_pattern_expr_r =
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 *)
+ cases_pattern_expr list * (* for constr subterms *)
+ cases_pattern_expr list list (* for recursive notations *)
and constr_expr_r =
| CRef of qualid * instance_expr option
@@ -142,10 +142,10 @@ and local_binder_expr =
| 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) *)
+ 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
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 3a4969a3ee..95a0039b0a 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -140,7 +140,7 @@ let rec constr_expr_eq e1 e2 =
in
List.equal field_eq l1 l2
| CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) ->
- (** Don't care about the case_style *)
+ (* Don't care about the case_style *)
Option.equal constr_expr_eq r1 r2 &&
List.equal case_expr_eq a1 a2 &&
List.equal branch_expr_eq brl1 brl2
@@ -220,7 +220,7 @@ and local_binder_eq l1 l2 = match l1, l2 with
| CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
| CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
- (** Don't care about the [binder_kind] *)
+ (* Don't care about the [binder_kind] *)
List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2
| _ -> false
@@ -258,7 +258,6 @@ let local_binders_loc bll = match bll with
| h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll))
(** Folds and maps *)
-
let is_constructor id =
try Globnames.isConstructRef
(Smartlocate.global_of_extended_global
@@ -294,9 +293,6 @@ let ids_of_pattern_list =
(List.fold_left (cases_pattern_fold_names Id.Set.add))
Id.Set.empty
-let ids_of_cases_indtype p =
- cases_pattern_fold_names Id.Set.add Id.Set.empty p
-
let ids_of_cases_tomatch tms =
List.fold_right
(fun (_, ona, indnal) l ->
@@ -367,6 +363,14 @@ let free_vars_of_constr_expr c =
| c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
in aux [] Id.Set.empty c
+let names_of_constr_expr c =
+ let vars = ref Id.Set.empty in
+ let rec aux () () = function
+ | { CAst.v = CRef (qid, _) } when qualid_is_ident qid ->
+ let id = qualid_basename qid in vars := Id.Set.add id !vars
+ | c -> fold_constr_expr_with_binders (fun a () -> vars := Id.Set.add a !vars) aux () () c
+ in aux () () c; !vars
+
let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)
(* Used in correctness and interface *)
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 7f14eb4583..f1a8ed202f 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -113,12 +113,12 @@ val map_constr_expr_with_binders :
val replace_vars_constr_expr :
Id.t Id.Map.t -> constr_expr -> constr_expr
-(** Specific function for interning "in indtype" syntax of "match" *)
-val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
-
val free_vars_of_constr_expr : constr_expr -> Id.Set.t
val occur_var_constr_expr : Id.t -> constr_expr -> bool
+(** Return all (non-qualified) names treating binders as names *)
+val names_of_constr_expr : constr_expr -> Id.Set.t
+
val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list
val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> notation -> (int * int) list
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fba03b9de9..444ac5ab6d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -67,10 +67,7 @@ let print_no_symbol = ref false
(**********************************************************************)
(* Turning notations and scopes on and off for printing *)
-module IRuleSet = Set.Make(struct
- type t = interp_rule
- let compare x y = Pervasives.compare x y
- end)
+module IRuleSet = InterpRuleSet
let inactive_notations_table =
Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty)
@@ -960,7 +957,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
| GSort s -> CSort (extern_glob_sort s)
- | GHole (e,naming,_) -> CHole (Some e, naming, None) (** TODO: extern tactics. *)
+ | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *)
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6313f2d7ba..c8c38ffe05 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -573,12 +573,17 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id =
(* TODO binders *)
next_ident_away_from id (fun id -> Id.Set.mem id fvs3)
-let is_var store pat =
+let is_patvar c =
+ match DAst.get c with
+ | PatVar _ -> true
+ | _ -> false
+
+let is_patvar_store store pat =
match DAst.get pat with
| PatVar na -> ignore(store na); true
| _ -> false
-let out_var pat =
+let out_patvar pat =
match pat.v with
| CPatAtom (Some qid) when qualid_is_ident qid ->
Name (qualid_basename qid)
@@ -600,7 +605,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in
let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
let pat, na = match disjpat with
- | [pat] when is_var store pat -> let na = get () in None, na
+ | [pat] when is_patvar_store store pat -> let na = get () in None, na
| _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
(renaming,env), pat, na
with Not_found ->
@@ -610,7 +615,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
let env = set_env_scopes env scopes in
if onlyident then
(* Do not try to interpret a variable as a constructor *)
- let na = out_var pat in
+ let na = out_patvar pat in
let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in
(renaming,env), None, na
else
@@ -618,7 +623,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
let pat, na =
match disjpat with
- | [pat] when is_var store pat -> let na = get () in None, na
+ | [pat] when is_patvar_store store pat -> let na = get () in None, na
| _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
(renaming,env), pat, na
with Not_found ->
@@ -743,7 +748,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
if onlyident then
- let na = out_var c in term_of_name na, None
+ let na = out_patvar c in term_of_name na, None
else
let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
match disjpat with
@@ -805,7 +810,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
(* and since we are only interested in the pattern as a term *)
let env = reset_hidden_inductive_implicit_test env in
if onlyident then
- term_of_name (out_var pat)
+ term_of_name (out_patvar pat)
else
let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
match disjpat with
@@ -1507,7 +1512,7 @@ let drop_notations_pattern looked_for genv =
let test_kind top =
if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
in
- (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
+ (* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
let rec rcp_of_glob scopes x = DAst.(map (function
| GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes))
| GHole (_,_,_) -> RCPatAtom (None)
@@ -1527,8 +1532,8 @@ let drop_notations_pattern looked_for genv =
try
match Nametab.locate_extended qid with
| SynDef sp ->
- let (vars,a) = Syntax_def.search_syntactic_definition sp in
- (match a with
+ let filter (vars,a) =
+ try match a with
| NRef g ->
(* Convention: do not deactivate implicit arguments and scopes for further arguments *)
test_kind top g;
@@ -1549,7 +1554,9 @@ let drop_notations_pattern looked_for genv =
let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in
let (_,argscs) = find_remaining_scopes pats1 pats2 g in
Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
- | _ -> raise Not_found)
+ | _ -> raise Not_found
+ with Not_found -> None in
+ Syntax_def.search_filtered_syntactic_definition filter sp
| TrueGlobal g ->
test_kind top g;
Dumpglob.add_glob ?loc:qid.loc g;
@@ -1739,7 +1746,7 @@ let intern_ind_pattern genv ntnvars scopes pat =
let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in
(with_letin,
match product_of_cases_patterns empty_alias idslpl with
- | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
+ | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin)
| _ -> error_bad_inductive_type ?loc)
| x -> error_bad_inductive_type ?loc
@@ -1977,30 +1984,30 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
end
| CCases (sty, rtnpo, tms, eqns) ->
let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
- Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc)
- (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na)
- inb) Id.Set.empty tms in
+ (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na))
+ Id.Set.empty tms in
(* as, in & return vars *)
let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in
- let tms,ex_ids,match_from_in = List.fold_right
- (fun citm (inds,ex_ids,matchs) ->
- let ((tm,ind),extra_id,match_td) = intern_case_item env forbidden_vars citm in
- (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs)
- tms ([],Id.Set.empty,[]) in
+ let tms,ex_ids,aliases,match_from_in = List.fold_right
+ (fun citm (inds,ex_ids,asubst,matchs) ->
+ let ((tm,ind),extra_id,(ind_ids,alias_subst,match_td)) =
+ intern_case_item env forbidden_vars citm in
+ (tm,ind)::inds,
+ Id.Set.union ind_ids (Option.fold_right Id.Set.add extra_id ex_ids),
+ merge_subst alias_subst asubst,
+ List.rev_append match_td matchs)
+ tms ([],Id.Set.empty,Id.Map.empty,[]) in
let env' = Id.Set.fold
(fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var))
(Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
(* PatVars before a real pattern do not need to be matched *)
let stripped_match_from_in =
- let is_patvar c = match DAst.get c with
- | PatVar _ -> true
- | _ -> false
- in
let rec aux = function
| [] -> []
| (_, c) :: q when is_patvar c -> aux q
| l -> l
in aux match_from_in in
+ let rtnpo = Option.map (replace_vars_constr_expr aliases) rtnpo in
let rtnpo = match stripped_match_from_in with
| [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *)
| l ->
@@ -2148,7 +2155,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(* the "in" part *)
let match_td,typ = match t with
| Some t ->
- let with_letin,(ind,l) = intern_ind_pattern globalenv ntnvars (None,env.scopes) t in
+ let with_letin,(ind,ind_ids,alias_subst,l) =
+ intern_ind_pattern globalenv ntnvars (None,env.scopes) t in
let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in
let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in
(* for "in Vect n", we answer (["n","n"],[(loc,"n")])
@@ -2184,9 +2192,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let _,args_rel =
List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
canonize_args args_rel l forbidden_names_for_gen [] [] in
- match_to_do, Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal))
+ (Id.Set.of_list (List.map (fun id -> id.CAst.v) ind_ids),alias_subst,match_to_do),
+ Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal))
| None ->
- [], None in
+ (Id.Set.empty,Id.Map.empty,[]), None in
(tm',(na.CAst.v, typ)), extra_id, match_td
and intern_impargs c env l subscopes args =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 035e4bc644..61acd09d65 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -45,13 +45,15 @@ type var_internalization_type =
type var_internalization_data =
var_internalization_type *
- (** type of the "free" variable, for coqdoc, e.g. while typing the
- constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+ (* type of the "free" variable, for coqdoc, e.g. while typing the
+ constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+
Id.t list *
- (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
- in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
- Impargs.implicit_status list * (** signature of impargs of the variable *)
- Notation_term.scope_name option list (** subscopes of the args of the variable *)
+ (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
+ in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
+
+ Impargs.implicit_status list * (* signature of impargs of the variable *)
+ Notation_term.scope_name option list (* subscopes of the args of the variable *)
(** A map of free variables to their implicit arguments and scopes *)
type internalization_env = var_internalization_data Id.Map.t
diff --git a/interp/declare.ml b/interp/declare.ml
index a809a856b9..6778fa1e7a 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -56,7 +56,7 @@ let load_constant i ((sp,kn), obj) =
(* Opening means making the name without its module qualification available *)
let open_constant i ((sp,kn), obj) =
- (** Never open a local definition *)
+ (* Never open a local definition *)
if obj.cst_locl then ()
else
let con = Global.constant_of_delta_kn kn in
@@ -166,9 +166,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
export_seff ||
not de.const_entry_opaque ||
is_poly de ->
- (** This globally defines the side-effects in the environment. We mark
- exported constants as being side-effect not to redeclare them at
- caching time. *)
+ (* This globally defines the side-effects in the environment. We mark
+ exported constants as being side-effect not to redeclare them at
+ caching time. *)
let de, export = Global.export_private_constants ~in_section de in
export, ConstantEntry (PureEntry, DefinitionEntry de)
| _ -> [], ConstantEntry (EffectEntry, cd)
@@ -191,7 +191,6 @@ let declare_definition ?(internal=UserIndividualRequest)
(Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
(** Declaration of section variables and local definitions *)
-
type section_variable_entry =
| SectionLocalDef of Safe_typing.private_constants definition_entry
| SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
@@ -214,16 +213,16 @@ let cache_variable ((sp,_),o) =
| SectionLocalDef (de) ->
let (de, eff) = Global.export_private_constants ~in_section:true de in
let () = List.iter register_side_effect eff in
- (** The body should already have been forced upstream because it is a
- section-local definition, but it's not enforced by typing *)
+ (* The body should already have been forced upstream because it is a
+ section-local definition, but it's not enforced by typing *)
let (body, uctx), () = Future.force de.const_entry_body in
let poly, univs = match de.const_entry_universes with
| Monomorphic_const_entry uctx -> false, uctx
| Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
in
let univs = Univ.ContextSet.union uctx univs in
- (** We must declare the universe constraints before type-checking the
- term. *)
+ (* We must declare the universe constraints before type-checking the
+ term. *)
let () = Global.push_context_set (not poly) univs in
let se = {
secdef_body = body;
@@ -262,7 +261,6 @@ let declare_variable id obj =
oname
(** Declaration of inductive blocks *)
-
let declare_inductive_argument_scopes kn mie =
List.iteri (fun i {mind_entry_consnames=lc} ->
Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i));
@@ -360,7 +358,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
let id = Label.to_id label in
let univs = match univs with
| Monomorphic_ind_entry _ ->
- (** Global constraints already defined through the inductive *)
+ (* Global constraints already defined through the inductive *)
Monomorphic_const_entry Univ.ContextSet.empty
| Polymorphic_ind_entry (nas, ctx) ->
Polymorphic_const_entry (nas, ctx)
@@ -447,11 +445,9 @@ let assumption_message id =
(** Monomorphic universes need to survive sections. *)
let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
- declare_object
- { (default_object "Monomorphic section universes") with
- cache_function = (fun (na, uctx) -> Global.push_context_set false uctx);
- discharge_function = (fun (_, x) -> Some x);
- classify_function = (fun a -> Dispose) }
+ declare_object @@ local_object "Monomorphic section universes"
+ ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
+ ~discharge:(fun (_, x) -> Some x)
let declare_universe_context poly ctx =
if poly then
@@ -511,7 +507,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
load_function = load_univ_names;
open_function = open_univ_names;
discharge_function = discharge_univ_names;
- subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
+ subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
classify_function = (fun a -> Substitute a) }
let declare_univ_binders gr pl =
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 931d05a975..554da7603f 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -18,6 +18,7 @@ val dump : unit -> bool
val noglob : unit -> unit
val dump_into_file : string -> unit (** special handling of "stdout" *)
+
val dump_to_dotglob : unit -> unit
val feedback_glob : unit -> unit
diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
deleted file mode 100644
index 607f2258fd..0000000000
--- a/interp/genredexpr.ml
+++ /dev/null
@@ -1,65 +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) *)
-(************************************************************************)
-
-(** Reduction expressions *)
-
-(** The parsing produces initially a list of [red_atom] *)
-
-type 'a red_atom =
- | FBeta
- | FMatch
- | FFix
- | FCofix
- | FZeta
- | FConst of 'a list
- | FDeltaBut of 'a list
-
-(** This list of atoms is immediately converted to a [glob_red_flag] *)
-
-type 'a glob_red_flag = {
- rBeta : bool;
- rMatch : bool;
- rFix : bool;
- rCofix : bool;
- rZeta : bool;
- rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
- rConst : 'a list
-}
-
-(** Generic kinds of reductions *)
-
-type ('a,'b,'c) red_expr_gen =
- | Red of bool
- | Hnf
- | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
- | Cbv of 'b glob_red_flag
- | Cbn of 'b glob_red_flag
- | Lazy of 'b glob_red_flag
- | Unfold of 'b Locus.with_occurrences list
- | Fold of 'a list
- | Pattern of 'a Locus.with_occurrences list
- | ExtraRedExpr of string
- | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
- | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
-
-type ('a,'b,'c) may_eval =
- | ConstrTerm of 'a
- | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
- | ConstrContext of Names.lident * 'a
- | ConstrTypeOf of 'a
-
-open Libnames
-open Constrexpr
-
-type r_trm = constr_expr
-type r_pat = constr_pattern_expr
-type r_cst = qualid or_by_notation
-
-type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d024a9e808..8a89bcdf26 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -448,7 +448,7 @@ let compute_mib_implicits flags kn =
Array.to_list
(Array.mapi (* No need to lift, arities contain no de Bruijn *)
(fun i mip ->
- (** No need to care about constraints here *)
+ (* No need to care about constraints here *)
let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in
Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
mib.mind_packets) in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index ea5aa90f68..4afc2af5e9 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -65,6 +65,7 @@ type implicit_explanation =
operational only if [conclusion_matters] is true. *)
type maximal_insertion = bool (** true = maximal contextual insertion *)
+
type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
type implicit_status = (Id.t * implicit_explanation *
diff --git a/interp/interp.mllib b/interp/interp.mllib
index aa20bda705..147eaf20dc 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,6 +1,4 @@
Constrexpr
-Genredexpr
-Redops
Tactypes
Stdarg
Notation_term
diff --git a/interp/notation.ml b/interp/notation.ml
index 0af75b5bfa..ca27d439fb 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -50,15 +50,25 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with
| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2
| (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false
+let notation_entry_level_compare s1 s2 = match (s1,s2) with
+| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> 0
+| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) ->
+ pair_compare String.compare Int.compare (s1,n1) (s2,n2)
+| InConstrEntrySomeLevel, _ -> -1
+| InCustomEntryLevel _, _ -> 1
+
let notation_eq (from1,ntn1) (from2,ntn2) =
notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2
let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s
+let notation_compare =
+ pair_compare notation_entry_level_compare String.compare
+
module NotationOrd =
struct
type t = notation
- let compare = Pervasives.compare
+ let compare = notation_compare
end
module NotationSet = Set.Make(NotationOrd)
@@ -178,6 +188,17 @@ type scoped_notation_rule_core = scope_name * notation * interpretation * int op
type notation_rule_core = interp_rule * interpretation * int option
type notation_rule = notation_rule_core * delimiters option * bool
+let interp_rule_compare r1 r2 = match r1, r2 with
+ | NotationRule (sc1,ntn1), NotationRule (sc2,ntn2) ->
+ pair_compare (Option.compare String.compare) notation_compare (sc1,ntn1) (sc2,ntn2)
+ | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2
+ | (NotationRule _ | SynDefRule _), _ -> -1
+
+module InterpRuleSet = Set.Make(struct
+ type t = interp_rule
+ let compare = interp_rule_compare
+ end)
+
(* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and *)
type uninterp_scope_elem =
@@ -308,7 +329,7 @@ let declare_delimiters scope key =
| None -> scope_map := String.Map.add scope newsc !scope_map
| Some oldkey when String.equal oldkey key -> ()
| Some oldkey ->
- (** FIXME: implement multikey scopes? *)
+ (* FIXME: implement multikey scopes? *)
Flags.if_verbose Feedback.msg_info
(str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
scope_map := String.Map.add scope newsc !scope_map
@@ -530,11 +551,11 @@ let prim_token_uninterpreters =
(*******************************************************)
(* Numeral notation interpretation *)
-type numeral_notation_error =
+type prim_token_notation_error =
| UnexpectedTerm of Constr.t
| UnexpectedNonOptionTerm of Constr.t
-exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error
type numnot_option =
| Nop
@@ -554,20 +575,26 @@ type target_kind =
| UInt of Names.inductive (* Coq.Init.Decimal.uint *)
| Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
+type string_target_kind =
+ | ListByte
+ | Byte
+
type option_kind = Option | Direct
-type conversion_kind = target_kind * option_kind
+type 'target conversion_kind = 'target * option_kind
-type numeral_notation_obj =
- { to_kind : conversion_kind;
+type ('target, 'warning) prim_token_notation_obj =
+ { to_kind : 'target conversion_kind;
to_ty : GlobRef.t;
- of_kind : conversion_kind;
+ of_kind : 'target conversion_kind;
of_ty : GlobRef.t;
- num_ty : Libnames.qualid; (* for warnings / error messages *)
- warning : numnot_option }
+ ty_name : Libnames.qualid; (* for warnings / error messages *)
+ warning : 'warning }
-module Numeral = struct
-(** * Numeral notation *)
+type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
+type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
+module PrimTokenNotation = struct
+(** * Code shared between Numeral notation and String notation *)
(** Reduction
The constr [c] below isn't necessarily well-typed, since we
@@ -596,7 +623,69 @@ let eval_constr env sigma (c : Constr.t) =
let eval_constr_app env sigma c1 c2 =
eval_constr env sigma (mkApp (c1,[| c2 |]))
-exception NotANumber
+exception NotAValidPrimToken
+
+(** The uninterp function below work at the level of [glob_constr]
+ which is too low for us here. So here's a crude conversion back
+ to [constr] for the subset that concerns us. *)
+
+let rec constr_of_glob env sigma g = match DAst.get g with
+ | Glob_term.GRef (ConstructRef c, _) ->
+ let sigma,c = Evd.fresh_constructor_instance env sigma c in
+ sigma,mkConstructU c
+ | Glob_term.GApp (gc, gcl) ->
+ let sigma,c = constr_of_glob env sigma gc in
+ let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
+ sigma,mkApp (c, Array.of_list cl)
+ | _ ->
+ raise NotAValidPrimToken
+
+let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
+ | App (c, ca) ->
+ let c = glob_of_constr token_kind ?loc env sigma c in
+ let cel = List.map (glob_of_constr token_kind ?loc env sigma) (Array.to_list ca) in
+ DAst.make ?loc (Glob_term.GApp (c, cel))
+ | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None))
+ | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
+ | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
+ | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
+ | _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c))
+
+let no_such_prim_token uninterpreted_token_kind ?loc ty =
+ CErrors.user_err ?loc
+ (str ("Cannot interpret this "^uninterpreted_token_kind^" as a value of type ") ++
+ pr_qualid ty)
+
+let interp_option uninterpreted_token_kind token_kind ty ?loc env sigma c =
+ match Constr.kind c with
+ | App (_Some, [| _; c |]) -> glob_of_constr token_kind ?loc env sigma c
+ | App (_None, [| _ |]) -> no_such_prim_token uninterpreted_token_kind ?loc ty
+ | x -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedNonOptionTerm c))
+
+let uninterp_option c =
+ match Constr.kind c with
+ | App (_Some, [| _; x |]) -> x
+ | _ -> raise NotAValidPrimToken
+
+let uninterp to_raw o (Glob_term.AnyGlobConstr n) =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in
+ let of_ty = EConstr.Unsafe.to_constr of_ty in
+ try
+ let sigma,n = constr_of_glob env sigma n in
+ let c = eval_constr_app env sigma of_ty n in
+ let c = if snd o.of_kind == Direct then c else uninterp_option c in
+ Some (to_raw (fst o.of_kind, c))
+ with
+ | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
+ | NotAValidPrimToken -> None (* all other functions except big2raw *)
+
+end
+
+module Numeral = struct
+(** * Numeral notation *)
+open PrimTokenNotation
let warn_large_num =
CWarnings.create ~name:"large-number" ~category:"numbers"
@@ -670,15 +759,15 @@ let rawnum_of_coquint c =
| Construct ((_,n), _) (* D0 to D9 *) ->
let () = Buffer.add_char buf (char_of_digit n) in
of_uint_loop a buf
- | _ -> raise NotANumber)
- | _ -> raise NotANumber
+ | _ -> raise NotAValidPrimToken)
+ | _ -> raise NotAValidPrimToken
in
let buf = Buffer.create 64 in
let () = of_uint_loop c buf in
if Int.equal (Buffer.length buf) 0 then
(* To avoid ambiguities between Nil and (D0 Nil), we choose
to not display Nil alone as "0" *)
- raise NotANumber
+ raise NotAValidPrimToken
else Buffer.contents buf
let rawnum_of_coqint c =
@@ -687,8 +776,8 @@ let rawnum_of_coqint c =
(match Constr.kind c with
| Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true)
| Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false)
- | _ -> raise NotANumber)
- | _ -> raise NotANumber
+ | _ -> raise NotAValidPrimToken)
+ | _ -> raise NotAValidPrimToken
(***********************************************************************)
@@ -718,9 +807,9 @@ let rec bigint_of_pos c = match Constr.kind c with
| 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d)
| n -> assert false (* no other constructor of type positive *)
end
- | x -> raise NotANumber
+ | x -> raise NotAValidPrimToken
end
- | x -> raise NotANumber
+ | x -> raise NotAValidPrimToken
(** Now, [Z] from/to bigint *)
@@ -745,51 +834,9 @@ let bigint_of_z z = match Constr.kind z with
| 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d)
| n -> assert false (* no other constructor of type Z *)
end
- | _ -> raise NotANumber
+ | _ -> raise NotAValidPrimToken
end
- | _ -> raise NotANumber
-
-(** The uninterp function below work at the level of [glob_constr]
- which is too low for us here. So here's a crude conversion back
- to [constr] for the subset that concerns us. *)
-
-let rec constr_of_glob env sigma g = match DAst.get g with
- | Glob_term.GRef (ConstructRef c, _) ->
- let sigma,c = Evd.fresh_constructor_instance env sigma c in
- sigma,mkConstructU c
- | Glob_term.GApp (gc, gcl) ->
- let sigma,c = constr_of_glob env sigma gc in
- let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
- sigma,mkApp (c, Array.of_list cl)
- | _ ->
- raise NotANumber
-
-let rec glob_of_constr ?loc env sigma c = match Constr.kind c with
- | App (c, ca) ->
- let c = glob_of_constr ?loc env sigma c in
- let cel = List.map (glob_of_constr ?loc env sigma) (Array.to_list ca) in
- DAst.make ?loc (Glob_term.GApp (c, cel))
- | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None))
- | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
- | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
- | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
- | _ -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedTerm c))
-
-let no_such_number ?loc ty =
- CErrors.user_err ?loc
- (str "Cannot interpret this number as a value of type " ++
- pr_qualid ty)
-
-let interp_option ty ?loc env sigma c =
- match Constr.kind c with
- | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c
- | App (_None, [| _ |]) -> no_such_number ?loc ty
- | x -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedNonOptionTerm c))
-
-let uninterp_option c =
- match Constr.kind c with
- | App (_Some, [| _; x |]) -> x
- | _ -> raise NotANumber
+ | _ -> raise NotAValidPrimToken
let big2raw n =
if Bigint.is_pos_or_zero n then (Bigint.to_string n, true)
@@ -801,13 +848,13 @@ let raw2big (n,s) =
let interp o ?loc n =
begin match o.warning with
| Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 ->
- warn_large_num o.num_ty
+ warn_large_num o.ty_name
| _ -> ()
end;
let c = match fst o.to_kind with
| Int int_ty -> coqint_of_rawnum int_ty n
| UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n)
- | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty
+ | UInt _ (* n <= 0 *) -> no_such_prim_token "number" ?loc o.ty_name
| Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n)
in
let env = Global.env () in
@@ -816,30 +863,120 @@ let interp o ?loc n =
let to_ty = EConstr.Unsafe.to_constr to_ty in
match o.warning, snd o.to_kind with
| Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 ->
- warn_abstract_large_num (o.num_ty,o.to_ty);
- glob_of_constr ?loc env sigma (mkApp (to_ty,[|c|]))
+ warn_abstract_large_num (o.ty_name,o.to_ty);
+ glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|]))
| _ ->
let res = eval_constr_app env sigma to_ty c in
match snd o.to_kind with
- | Direct -> glob_of_constr ?loc env sigma res
- | Option -> interp_option o.num_ty ?loc env sigma res
+ | Direct -> glob_of_constr "numeral" ?loc env sigma res
+ | Option -> interp_option "number" "numeral" o.ty_name ?loc env sigma res
+
+let uninterp o n =
+ PrimTokenNotation.uninterp
+ begin function
+ | (Int _, c) -> rawnum_of_coqint c
+ | (UInt _, c) -> (rawnum_of_coquint c, true)
+ | (Z _, c) -> big2raw (bigint_of_z c)
+ end o n
+end
+
+module Strings = struct
+(** * String notation *)
+open PrimTokenNotation
+
+let qualid_of_ref n =
+ n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+
+let q_list () = qualid_of_ref "core.list.type"
+let q_byte () = qualid_of_ref "core.byte.type"
+
+let unsafe_locate_ind q =
+ match Nametab.locate q with
+ | IndRef i -> i
+ | _ -> raise Not_found
+
+let locate_list () = unsafe_locate_ind (q_list ())
+let locate_byte () = unsafe_locate_ind (q_byte ())
+
+(***********************************************************************)
+
+(** ** Conversion between Coq [list Byte.byte] and internal raw string *)
+
+let coqbyte_of_char_code byte c =
+ mkConstruct (byte, 1 + c)
-let uninterp o (Glob_term.AnyGlobConstr n) =
+let coqbyte_of_string ?loc byte s =
+ let p =
+ if Int.equal (String.length s) 1 then int_of_char s.[0]
+ else
+ if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
+ then int_of_string s
+ else
+ user_err ?loc ~hdr:"coqbyte_of_string"
+ (str "Expects a single character or a three-digits ascii code.") in
+ coqbyte_of_char_code byte p
+
+let coqbyte_of_char byte c = coqbyte_of_char_code byte (Char.code c)
+
+let make_ascii_string n =
+ if n>=32 && n<=126 then String.make 1 (char_of_int n)
+ else Printf.sprintf "%03d" n
+
+let char_code_of_coqbyte c =
+ match Constr.kind c with
+ | Construct ((_,c), _) -> c - 1
+ | _ -> raise NotAValidPrimToken
+
+let string_of_coqbyte c = make_ascii_string (char_code_of_coqbyte c)
+
+let coqlist_byte_of_string byte_ty list_ty str =
+ let cbyte = mkInd byte_ty in
+ let nil = mkApp (mkConstruct (list_ty, 1), [|cbyte|]) in
+ let cons x xs = mkApp (mkConstruct (list_ty, 2), [|cbyte; x; xs|]) in
+ let rec do_chars s i acc =
+ if i < 0 then acc
+ else
+ let b = coqbyte_of_char byte_ty s.[i] in
+ do_chars s (i-1) (cons b acc)
+ in
+ do_chars str (String.length str - 1) nil
+
+(* N.B. We rely on the fact that [nil] is the first constructor and [cons] is the second constructor, for [list] *)
+let string_of_coqlist_byte c =
+ let rec of_coqlist_byte_loop c buf =
+ match Constr.kind c with
+ | App (_nil, [|_ty|]) -> ()
+ | App (_cons, [|_ty;b;c|]) ->
+ let () = Buffer.add_char buf (Char.chr (char_code_of_coqbyte b)) in
+ of_coqlist_byte_loop c buf
+ | _ -> raise NotAValidPrimToken
+ in
+ let buf = Buffer.create 64 in
+ let () = of_coqlist_byte_loop c buf in
+ Buffer.contents buf
+
+let interp o ?loc n =
+ let byte_ty = locate_byte () in
+ let list_ty = locate_list () in
+ let c = match fst o.to_kind with
+ | ListByte -> coqlist_byte_of_string byte_ty list_ty n
+ | Byte -> coqbyte_of_string ?loc byte_ty n
+ in
let env = Global.env () in
let sigma = Evd.from_env env in
- let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in
- let of_ty = EConstr.Unsafe.to_constr of_ty in
- try
- let sigma,n = constr_of_glob env sigma n in
- let c = eval_constr_app env sigma of_ty n in
- let c = if snd o.of_kind == Direct then c else uninterp_option c in
- match fst o.of_kind with
- | Int _ -> Some (rawnum_of_coqint c)
- | UInt _ -> Some (rawnum_of_coquint c, true)
- | Z _ -> Some (big2raw (bigint_of_z c))
- with
- | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
- | NotANumber -> None (* all other functions except big2raw *)
+ let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in
+ let to_ty = EConstr.Unsafe.to_constr to_ty in
+ let res = eval_constr_app env sigma to_ty c in
+ match snd o.to_kind with
+ | Direct -> glob_of_constr "string" ?loc env sigma res
+ | Option -> interp_option "string" "string" o.ty_name ?loc env sigma res
+
+let uninterp o n =
+ PrimTokenNotation.uninterp
+ begin function
+ | (ListByte, c) -> string_of_coqlist_byte c
+ | (Byte, c) -> string_of_coqbyte c
+ end o n
end
(* A [prim_token_infos], which is synchronized with the document
@@ -853,6 +990,7 @@ end
type prim_token_interp_info =
Uid of prim_token_uid
| NumeralNotation of numeral_notation_obj
+ | StringNotation of string_notation_obj
type prim_token_infos = {
pt_local : bool; (** Is this interpretation local? *)
@@ -1081,6 +1219,7 @@ let find_prim_token check_allowed ?loc p sc =
let interp = match info with
| Uid uid -> Hashtbl.find prim_token_interpreters uid
| NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o)
+ | StringNotation o -> InnerPrimToken.StringInterp (Strings.interp o)
in
let pat = InnerPrimToken.do_interp ?loc interp p in
check_allowed pat;
@@ -1270,6 +1409,7 @@ let uninterp_prim_token c =
let uninterp = match info with
| Uid uid -> Hashtbl.find prim_token_uninterpreters uid
| NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+ | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
in
match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
| None -> raise Notation_ops.No_match
@@ -1289,6 +1429,8 @@ let availability_of_prim_token n printer_scope local_scopes =
match n, uid with
| Numeral _, NumeralNotation _ -> true
| _, NumeralNotation _ -> false
+ | String _, StringNotation _ -> true
+ | _, StringNotation _ -> false
| _, Uid uid ->
let interp = Hashtbl.find prim_token_interpreters uid in
match n, interp with
@@ -1781,7 +1923,7 @@ let pr_visibility prglob = function
(**********************************************************************)
(* Synchronisation with reset *)
-let freeze _ =
+let freeze ~marshallable =
(!scope_map, !scope_stack, !uninterp_scope_stack, !arguments_scope,
!delimiters_map, !notations_key_table, !scope_class_map,
!prim_token_interp_infos, !prim_token_uninterp_infos,
@@ -1818,7 +1960,7 @@ let _ =
Summary.init_function = init }
let with_notation_protection f x =
- let fs = freeze false in
+ let fs = freeze ~marshallable:false in
try let a = f x in unfreeze fs; a
with reraise ->
let reraise = CErrors.push reraise in
diff --git a/interp/notation.mli b/interp/notation.mli
index 3480d1c8f2..a482e00e81 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -54,7 +54,7 @@ val scope_is_open : scope_name -> bool
(** Open scope *)
val open_close_scope :
- (** locality *) bool * (* open *) bool * scope_name -> unit
+ (* locality *) bool * (* open *) bool * scope_name -> unit
(** Extend a list of scopes *)
val empty_scope_stack : scopes
@@ -104,11 +104,11 @@ val register_string_interpretation :
(** * Numeral notation *)
-type numeral_notation_error =
+type prim_token_notation_error =
| UnexpectedTerm of Constr.t
| UnexpectedNonOptionTerm of Constr.t
-exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error
type numnot_option =
| Nop
@@ -128,20 +128,28 @@ type target_kind =
| UInt of Names.inductive (* Coq.Init.Decimal.uint *)
| Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
+type string_target_kind =
+ | ListByte
+ | Byte
+
type option_kind = Option | Direct
-type conversion_kind = target_kind * option_kind
+type 'target conversion_kind = 'target * option_kind
-type numeral_notation_obj =
- { to_kind : conversion_kind;
+type ('target, 'warning) prim_token_notation_obj =
+ { to_kind : 'target conversion_kind;
to_ty : GlobRef.t;
- of_kind : conversion_kind;
+ of_kind : 'target conversion_kind;
of_ty : GlobRef.t;
- num_ty : Libnames.qualid; (* for warnings / error messages *)
- warning : numnot_option }
+ ty_name : Libnames.qualid; (* for warnings / error messages *)
+ warning : 'warning }
+
+type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
+type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
type prim_token_interp_info =
Uid of prim_token_uid
| NumeralNotation of numeral_notation_obj
+ | StringNotation of string_notation_obj
type prim_token_infos = {
pt_local : bool; (** Is this interpretation local? *)
@@ -202,6 +210,8 @@ type interp_rule =
| NotationRule of scope_name option * notation
| SynDefRule of KerName.t
+module InterpRuleSet : Set.S with type elt = interp_rule
+
val declare_notation_interpretation : notation -> scope_name option ->
interpretation -> notation_location -> onlyprint:bool -> unit
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7a525f84a5..8d225fe683 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -37,7 +37,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
| _ -> false)
| NApp (t1, a1), NApp (t2, a2) ->
(eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
-| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
+| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *)
| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
(eq_notation_constr vars) u1 u2 && b1 == b2
@@ -51,7 +51,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
Name.equal na1 na2 && eq_notation_constr vars b1 b2 &&
Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
+| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *)
let eqpat (p1, t1) (p2, t2) =
List.equal cases_pattern_eq p1 p2 &&
(eq_notation_constr vars) t1 t2
@@ -75,7 +75,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
Option.equal (eq_notation_constr vars) o1 o2 &&
(eq_notation_constr vars) u1 u2 &&
(eq_notation_constr vars) r1 r2
-| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *)
+| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *)
let eq (na1, o1, t1) (na2, o2, t2) =
Name.equal na1 na2 &&
Option.equal (eq_notation_constr vars) o1 o2 &&
@@ -530,8 +530,10 @@ let rec subst_notation_constr subst bound raw =
match raw with
| NRef ref ->
let ref',t = subst_global subst ref in
- if ref' == ref then raw else
- fst (notation_constr_of_constr bound t)
+ if ref' == ref then raw else (match t with
+ | None -> NRef ref'
+ | Some t ->
+ fst (notation_constr_of_constr bound t.Univ.univ_abstracted_value))
| NVar _ -> raw
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 5fb0ca1b43..0ef1f267f6 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -20,13 +20,13 @@ open Glob_term
as well as non global expressions such as existential variables. *)
type notation_constr =
- (** Part common to [glob_constr] and [cases_pattern] *)
+ (* Part common to [glob_constr] and [cases_pattern] *)
| NRef of GlobRef.t
| NVar of Id.t
| NApp of notation_constr * notation_constr list
| NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
| NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
- (** Part only in [glob_constr] *)
+ (* 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
diff --git a/interp/redops.ml b/interp/redops.ml
deleted file mode 100644
index b9a74136e4..0000000000
--- a/interp/redops.ml
+++ /dev/null
@@ -1,64 +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 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/redops.mli b/interp/redops.mli
deleted file mode 100644
index 7254f29b25..0000000000
--- a/interp/redops.mli
+++ /dev/null
@@ -1,20 +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 Genredexpr
-
-val make_red_flag : 'a red_atom list -> 'a glob_red_flag
-
-val all_flags : 'a glob_red_flag
-
-(** Mapping [red_expr_gen] *)
-
-val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
- ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 7b01b6dc1c..bf3a8fe215 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -11,8 +11,6 @@
open Genarg
open Geninterp
-type 'a and_short_name = 'a * Names.lident option
-
let make0 ?dyn name =
let wit = Genarg.make0 name in
let () = register_val0 wit dyn in
@@ -53,8 +51,6 @@ let wit_uconstr = make0 "uconstr"
let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
-let wit_red_expr = make0 "redexpr"
-
let wit_clause_dft_concl =
make0 "clause_dft_concl"
@@ -65,4 +61,3 @@ let wit_preident = wit_pre_ident
let wit_reference = wit_ref
let wit_global = wit_ref
let wit_clause = wit_clause_dft_concl
-let wit_redexpr = wit_red_expr
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 5e5e43ed38..c974a4403c 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -14,15 +14,11 @@ open Loc
open Names
open EConstr
open Libnames
-open Genredexpr
-open Pattern
open Constrexpr
open Genarg
open Genintern
open Locus
-type 'a and_short_name = 'a * lident option
-
val wit_unit : unit uniform_genarg_type
val wit_bool : bool uniform_genarg_type
@@ -52,11 +48,6 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_
val wit_open_constr :
(constr_expr, glob_constr_and_expr, constr) genarg_type
-val wit_red_expr :
- ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
- (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
- (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
-
val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
(** Aliases for compatibility *)
@@ -66,7 +57,3 @@ val wit_preident : string uniform_genarg_type
val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_global : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
-val wit_redexpr :
- ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
- (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
- (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index b73d238c22..49273c4146 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -105,3 +105,10 @@ let search_syntactic_definition ?loc kn =
let def = out_pat pat in
verbose_compat ?loc kn def v;
def
+
+let search_filtered_syntactic_definition ?loc filter kn =
+ let pat,v = KNmap.find kn !syntax_table in
+ let def = out_pat pat in
+ let res = filter def in
+ (match res with Some _ -> verbose_compat ?loc kn def v | None -> ());
+ res
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index c5b6655ff8..77873f8f67 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -19,3 +19,6 @@ val declare_syntactic_definition : bool -> Id.t ->
Flags.compat_version option -> syndef_interpretation -> unit
val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation
+
+val search_filtered_syntactic_definition : ?loc:Loc.t ->
+ (syndef_interpretation -> 'a option) -> KerName.t -> 'a option
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:52:28 +0000