aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrarg.ml73
-rw-r--r--interp/constrarg.mli28
-rw-r--r--interp/constrexpr_ops.ml2
-rw-r--r--interp/constrextern.ml96
-rw-r--r--interp/constrintern.ml238
-rw-r--r--interp/dumpglob.ml6
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/notation.ml59
-rw-r--r--interp/notation.mli11
-rw-r--r--interp/notation_ops.ml209
-rw-r--r--interp/notation_ops.mli32
-rw-r--r--interp/stdarg.ml25
-rw-r--r--interp/stdarg.mli5
-rw-r--r--interp/syntax_def.ml2
-rw-r--r--interp/topconstr.ml12
-rw-r--r--interp/topconstr.mli4
16 files changed, 414 insertions, 390 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index a48d683754..011b31d9ae 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -8,9 +8,14 @@
open Loc
open Tacexpr
-open Term
open Misctypes
open Genarg
+open Geninterp
+
+let make0 ?dyn name =
+ let wit = Genarg.make0 name in
+ let () = Geninterp.register_val0 wit dyn in
+ wit
(** This is a hack for now, to break the dependency of Genarg on constr-related
types. We should use dedicated functions someday. *)
@@ -20,65 +25,47 @@ let loc_of_or_by_notation f = function
| ByNotation (loc,s,_) -> loc
let wit_int_or_var =
- Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "int_or_var"
+ make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var"
let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
- Genarg.make0 None "intropattern"
+ make0 "intropattern"
let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
- Genarg.make0 None "tactic"
+ make0 "tactic"
+
+let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
let wit_ident =
- Genarg.make0 None "ident"
+ make0 "ident"
let wit_var =
- Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) None "var"
-
-let wit_ref = Genarg.make0 None "ref"
+ make0 ~dyn:(val_tag (topwit wit_ident)) "var"
-let wit_quant_hyp = Genarg.make0 None "quant_hyp"
+let wit_ref = make0 "ref"
-let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
- Genarg.make0 None "sort"
+let wit_quant_hyp = make0 "quant_hyp"
let wit_constr =
- Genarg.make0 None "constr"
+ make0 "constr"
-let wit_constr_may_eval =
- Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval"
+let wit_uconstr = make0 "uconstr"
-let wit_uconstr = Genarg.make0 None "uconstr"
+let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
-let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "open_constr"
+let wit_constr_with_bindings = make0 "constr_with_bindings"
-let wit_constr_with_bindings = Genarg.make0 None "constr_with_bindings"
+let wit_bindings = make0 "bindings"
-let wit_bindings = Genarg.make0 None "bindings"
+let wit_red_expr = make0 "redexpr"
-let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
- Genarg.make0 None "hyp_location_flag"
+let wit_clause_dft_concl =
+ make0 "clause_dft_concl"
-let wit_red_expr = Genarg.make0 None "redexpr"
+(** Aliases *)
-let wit_clause_dft_concl =
- Genarg.make0 None "clause_dft_concl"
-
-(** Register location *)
-
-let () =
- register_name0 wit_int_or_var "Constrarg.wit_int_or_var";
- register_name0 wit_ref "Constrarg.wit_ref";
- register_name0 wit_ident "Constrarg.wit_ident";
- register_name0 wit_var "Constrarg.wit_var";
- register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
- register_name0 wit_tactic "Constrarg.wit_tactic";
- register_name0 wit_sort "Constrarg.wit_sort";
- register_name0 wit_constr "Constrarg.wit_constr";
- register_name0 wit_uconstr "Constrarg.wit_uconstr";
- register_name0 wit_open_constr "Constrarg.wit_open_constr";
- register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval";
- register_name0 wit_red_expr "Constrarg.wit_red_expr";
- register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl";
- register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp";
- register_name0 wit_bindings "Constrarg.wit_bindings";
- register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings";
+let wit_reference = wit_ref
+let wit_global = wit_ref
+let wit_clause = wit_clause_dft_concl
+let wit_quantified_hypothesis = wit_quant_hyp
+let wit_intropattern = wit_intro_pattern
+let wit_redexpr = wit_red_expr
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 5c26af3c2a..70c9c0de2c 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -38,15 +38,8 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
-
val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
-val wit_constr_may_eval :
- ((constr_expr,reference or_by_notation,constr_expr) may_eval,
- (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
- constr) genarg_type
-
val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
val wit_open_constr :
@@ -62,13 +55,28 @@ val wit_bindings :
glob_constr_and_expr bindings,
constr bindings delayed_open) genarg_type
-val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type
-
val wit_red_expr :
((constr_expr,reference 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_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
+val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type
+
+(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their
+ toplevel interpretation. The one of [wit_ltac] forces the tactic and
+ discards the result. *)
+val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type
val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+
+(** Aliases for compatibility *)
+
+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_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located 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 located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+val wit_redexpr :
+ ((constr_expr,reference 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/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 9c577034e8..c5730e6261 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -66,7 +66,7 @@ let rec cases_pattern_expr_eq p1 p2 =
Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
| CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) ->
eq_reference c1 c2 &&
- List.equal cases_pattern_expr_eq a1 a2 &&
+ Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
List.equal cases_pattern_expr_eq b1 b2
| CPatAtom(_,r1), CPatAtom(_,r2) ->
Option.equal eq_reference r1 r2
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3675441353..57091ca898 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -175,6 +175,10 @@ let add_patt_for_params ind l =
if !Flags.in_debugger then l else
Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l
+let add_cpatt_for_params ind l =
+ if !Flags.in_debugger then l else
+ Util.List.addn (Inductiveops.inductive_nparamdecls ind) (PatVar (Loc.ghost,Anonymous)) l
+
let drop_implicits_in_patt cst nb_expl args =
let impl_st = (implicits_of_global cst) in
let impl_data = extract_impargs_data impl_st in
@@ -266,7 +270,7 @@ let make_pat_notation loc ntn (terms,termlists as subst) args =
let mkPat loc qid l =
(* Normally irrelevant test with v8 syntax, but let's do it anyway *)
- if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,[],l)
+ if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,None,l)
let pattern_printable_in_both_syntax (ind,_ as c) =
let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
@@ -286,7 +290,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
- CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
+ CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
| _ ->
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -299,7 +303,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
with No_match ->
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_symbol_pattern scopes vars pat
+ extern_notation_pattern scopes vars pat
(uninterp_cases_pattern_notations pat)
with No_match ->
match pat with
@@ -327,15 +331,15 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
with
Not_found | No_match | Exit ->
let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
- if !Topconstr.oldfashion_patterns then
+ if !Topconstr.asymmetric_patterns then
if pattern_printable_in_both_syntax cstrsp
- then CPatCstr (loc, c, [], args)
- else CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
+ then CPatCstr (loc, c, None, args)
+ else CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
else
let full_args = add_patt_for_params (fst cstrsp) args in
match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
- |Some true_args -> CPatCstr (loc, c, [], true_args)
- |None -> CPatCstr (loc, c, full_args, [])
+ |Some true_args -> CPatCstr (loc, c, None, true_args)
+ |None -> CPatCstr (loc, c, Some full_args, [])
in insert_pat_alias loc p na
and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
(tmp_scope, scopes as allscopes) vars =
@@ -358,7 +362,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
List.map (extern_cases_pattern_in_scope subscope vars) c)
substlist in
let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
- let l2' = if !Topconstr.oldfashion_patterns || not (List.is_empty ll) then l2
+ let l2' = if !Topconstr.asymmetric_patterns || not (List.is_empty ll) then l2
else
match drop_implicits_in_patt gr nb_to_drop l2 with
|Some true_args -> true_args
@@ -374,7 +378,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
subst in
let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
- let l2' = if !Topconstr.oldfashion_patterns then l2
+ let l2' = if !Topconstr.asymmetric_patterns then l2
else
match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
|Some true_args -> true_args
@@ -382,7 +386,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
in
assert (List.is_empty substlist);
mkPat loc qid (List.rev_append l1 l2')
-and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
+and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
try
@@ -395,9 +399,9 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
| PatVar (loc,Anonymous) -> CPatAtom (loc, None)
| PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id)))
with
- No_match -> extern_symbol_pattern allscopes vars t rules
+ No_match -> extern_notation_pattern allscopes vars t rules
-let rec extern_symbol_ind_pattern allscopes vars ind args = function
+let rec extern_notation_ind_pattern allscopes vars ind args = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
try
@@ -405,7 +409,7 @@ let rec extern_symbol_ind_pattern allscopes vars ind args = function
apply_notation_to_pattern Loc.ghost (IndRef ind)
(match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
with
- No_match -> extern_symbol_ind_pattern allscopes vars ind args rules
+ No_match -> extern_notation_ind_pattern allscopes vars ind args rules
let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
(* pboutill: There are letins in pat which is incompatible with notations and
@@ -413,7 +417,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
let c = extern_reference Loc.ghost vars (IndRef ind) in
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
- CPatCstr (Loc.ghost, c, add_patt_for_params ind args, [])
+ CPatCstr (Loc.ghost, c, Some (add_patt_for_params ind args), [])
else
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -425,14 +429,14 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
with No_match ->
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_symbol_ind_pattern scopes vars ind args
+ extern_notation_ind_pattern scopes vars ind args
(uninterp_ind_pattern_notations ind)
with No_match ->
let c = extern_reference Loc.ghost vars (IndRef ind) in
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
match drop_implicits_in_patt (IndRef ind) 0 args with
- |Some true_args -> CPatCstr (Loc.ghost, c, [], true_args)
- |None -> CPatCstr (Loc.ghost, c, args, [])
+ |Some true_args -> CPatCstr (Loc.ghost, c, None, true_args)
+ |None -> CPatCstr (Loc.ghost, c, Some args, [])
let extern_cases_pattern vars p =
extern_cases_pattern_in_scope (None,[]) vars p
@@ -477,15 +481,15 @@ let explicitize loc inctx impl (cf,f) args =
(!print_implicits && !print_implicits_explicit_args) ||
(is_needed_for_correct_partial_application tail imp) ||
(!print_implicits_defensive &&
- is_significant_implicit a &&
- not (is_inferable_implicit inctx n imp))
+ not (is_inferable_implicit inctx n imp) &&
+ is_significant_implicit (Lazy.force a))
in
if visible then
- (a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail
+ (Lazy.force a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail
else
tail
- | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
- | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*)
+ | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl)
+ | args, [] -> List.map (fun a -> (Lazy.force a,None)) args (*In case of polymorphism*)
| [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp ->
(* The non-explicit application cannot be parsed back with the same type *)
raise Expl
@@ -512,7 +516,7 @@ let explicitize loc inctx impl (cf,f) args =
with Expl ->
let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in
let ip = if !print_projections then ip else None in
- CAppExpl (loc, (ip, f', us), args)
+ CAppExpl (loc, (ip, f', us), List.map Lazy.force args)
let is_start_implicit = function
| imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
@@ -534,19 +538,21 @@ let extern_app loc inctx impl (cf,f) us args =
(!print_implicits && not !print_implicits_explicit_args)) &&
List.exists is_status_implicit impl)
then
+ let args = List.map Lazy.force args in
CAppExpl (loc, (is_projection (List.length args) cf,f,us), args)
else
explicitize loc inctx impl (cf,CRef (f,us)) args
-let rec extern_args extern scopes env args subscopes =
- match args with
- | [] -> []
- | a::args ->
- let argscopes, subscopes = match subscopes with
- | [] -> (None,scopes), []
- | scopt::subscopes -> (scopt,scopes), subscopes in
- extern argscopes env a :: extern_args extern scopes env args subscopes
+let rec fill_arg_scopes args subscopes scopes = match args, subscopes with
+| [], _ -> []
+| a :: args, scopt :: subscopes ->
+ (a, (scopt, scopes)) :: fill_arg_scopes args subscopes scopes
+| a :: args, [] ->
+ (a, (None, scopes)) :: fill_arg_scopes args [] scopes
+let extern_args extern env args =
+ let map (arg, argscopes) = lazy (extern argscopes env arg) in
+ List.map map args
let match_coercion_app = function
| GApp (loc,GRef (_,r,_),args) -> Some (loc, r, 0, args)
@@ -622,7 +628,7 @@ let rec extern inctx scopes vars r =
try
let r'' = flatten_application r' in
if !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_symbol scopes vars r'' (uninterp_notations r'')
+ extern_notation scopes vars r'' (uninterp_notations r'')
with No_match -> match r' with
| GRef (loc,ref,us) ->
extern_global loc (select_stronger_impargs (implicits_of_global ref))
@@ -643,8 +649,7 @@ let rec extern inctx scopes vars r =
(match f with
| GRef (rloc,ref,us) ->
let subscopes = find_arguments_scope ref in
- let args =
- extern_args (extern true) (snd scopes) vars args subscopes in
+ let args = fill_arg_scopes args subscopes (snd scopes) in
begin
try
if !Flags.raw_print then raise Exit;
@@ -679,12 +684,14 @@ let rec extern inctx scopes vars r =
match args with
| [] -> raise No_match
(* we give up since the constructor is not complete *)
- | head :: tail -> ip q locs' tail
- ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
+ | (arg, scopes) :: tail ->
+ let head = extern true scopes vars arg in
+ ip q locs' tail ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
in
CRecord (loc, List.rev (ip projs locals args []))
with
| Not_found | No_match | Exit ->
+ let args = extern_args (extern true) vars args in
extern_app loc inctx
(select_stronger_impargs (implicits_of_global ref))
(Some ref,extern_reference rloc vars ref) (extern_universes us) args
@@ -692,7 +699,7 @@ let rec extern inctx scopes vars r =
| _ ->
explicitize loc inctx [] (None,sub_extern false scopes vars f)
- (List.map (sub_extern true scopes vars) args))
+ (List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
| GLetIn (loc,na,t,c) ->
CLetIn (loc,(loc,na),sub_extern false scopes vars t,
@@ -730,9 +737,7 @@ let rec extern inctx scopes vars r =
na',
Option.map (fun (loc,ind,nal) ->
let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
- let fullargs =
- if !Flags.in_debugger then args else
- Notation_ops.add_patterns_for_params ind args in
+ let fullargs = add_cpatt_for_params ind args in
extern_ind_pattern_in_scope scopes vars ind fullargs
) x))
tml
@@ -793,7 +798,7 @@ let rec extern inctx scopes vars r =
Miscops.map_cast_type (extern_typ scopes vars) c')
and extern_typ (_,scopes) =
- extern true (Some Notation.type_scope,scopes)
+ extern true (Notation.current_type_scope_name (),scopes)
and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
@@ -842,7 +847,7 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
(loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
extern inctx scopes vars c)
-and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
+and extern_notation (tmp_scope,scopes as allscopes) vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
let loc = Glob_ops.loc_of_glob_constr t in
@@ -914,10 +919,11 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
if List.is_empty l then a else CApp (loc,(None,a),l) in
if List.is_empty args then e
else
- let args = extern_args (extern true) scopes vars args argsscopes in
+ let args = fill_arg_scopes args argsscopes scopes in
+ let args = extern_args (extern true) vars args in
explicitize loc false argsimpls (None,e) args
with
- No_match -> extern_symbol allscopes vars t rules
+ No_match -> extern_notation allscopes vars t rules
and extern_recursion_order scopes vars = function
GStructRec -> CStructRec
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 36f88fc3cc..50252a368f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -300,7 +300,7 @@ let set_var_scope loc id istermvar env ntnvars =
(* Not in a notation *)
()
-let set_type_scope env = {env with tmp_scope = Some Notation.type_scope}
+let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name ()}
let reset_tmp_scope env = {env with tmp_scope = None}
@@ -451,12 +451,15 @@ let intern_generalization intern env lvar loc bk ak c =
| Some AbsPi -> true
| Some _ -> false
| None ->
- let is_type_scope = match env.tmp_scope with
+ match Notation.current_type_scope_name () with
+ | Some type_scope ->
+ let is_type_scope = match env.tmp_scope with
+ | None -> false
+ | Some sc -> String.equal sc type_scope
+ in
+ is_type_scope ||
+ String.List.mem type_scope env.scopes
| None -> false
- | Some sc -> String.equal sc Notation.type_scope
- in
- is_type_scope ||
- String.List.mem Notation.type_scope env.scopes
in
if pi then
(fun (id, loc') acc ->
@@ -523,7 +526,7 @@ let rec subst_iterator y t = function
| GVar (_,id) as x -> if Id.equal id y then t else x
| x -> map_glob_constr (subst_iterator y t) x
-let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c =
+let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c =
let (terms,termlists,binders) = subst in
(* when called while defining a notation, avoid capturing the private binders
of the expression by variables bound by the notation (see #3892) *)
@@ -646,7 +649,7 @@ let intern_notation intern env lvar loc ntn fullargs =
let terms = make_subst ids args in
let termlists = make_subst idsl argslist in
let binders = make_subst idsbl bll in
- subst_aconstr_in_glob_constr loc intern lvar
+ instantiate_notation_constr loc intern lvar
(terms, termlists, binders) (Id.Map.empty, env) c
(**********************************************************************)
@@ -756,7 +759,15 @@ let intern_qualid loc qid intern env lvar us args =
let subst = (terms, Id.Map.empty, Id.Map.empty) in
let infos = (Id.Map.empty, env) in
let projapp = match c with NRef _ -> true | _ -> false in
- subst_aconstr_in_glob_constr loc intern lvar subst infos c, projapp, args2
+ let c = instantiate_notation_constr loc intern lvar subst infos c in
+ let c = match us, c with
+ | None, _ -> c
+ | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us)
+ | Some _, _ ->
+ user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++
+ str " cannot have a universe instance")
+ in
+ c, projapp, args2
(* Rule out section vars since these should have been found by intern_var *)
let intern_non_secvar_qualid loc qid intern env lvar us args =
@@ -918,7 +929,7 @@ let chop_params_pattern loc ind args with_letin =
args
let find_constructor loc add_params ref =
- let cstr = match ref with
+ let (ind,_ as cstr) = match ref with
| ConstructRef cstr -> cstr
| IndRef _ ->
let error = str "There is an inductive name deep in a \"in\" clause." in
@@ -927,15 +938,15 @@ let find_constructor loc add_params ref =
let error = str "This reference is not a constructor." in
user_err_loc (loc, "find_constructor", error)
in
- cstr, (function (ind,_ as c) -> match add_params with
- |Some nb_args ->
+ cstr, match add_params with
+ | Some nb_args ->
let nb =
- if Int.equal nb_args (Inductiveops.constructor_nrealdecls c)
+ if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr)
then Inductiveops.inductive_nparamdecls ind
else Inductiveops.inductive_nparams ind
in
List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))])
- |None -> []) cstr
+ | None -> []
let find_pattern_variable = function
| Ident (loc,id) -> id
@@ -1058,7 +1069,7 @@ let alias_of als = match als.alias_ids with
| id :: _ -> Name id
let message_redundant_alias id1 id2 =
- msg_warning
+ Feedback.msg_warning
(str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2)
(** {6 Expanding notations }
@@ -1091,41 +1102,42 @@ let drop_notations_pattern looked_for =
let test_kind top =
if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
in
- let rec drop_syndef top env re pats =
+ let rec drop_syndef top scopes re pats =
let (loc,qid) = qualid_of_reference re in
try
match locate_extended qid with
- |SynDef sp ->
+ | SynDef sp ->
let (vars,a) = Syntax_def.search_syntactic_definition sp in
(match a with
| NRef g ->
+ (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
test_kind top g;
let () = assert (List.is_empty vars) in
let (_,argscs) = find_remaining_scopes [] pats g in
- Some (g, [], List.map2 (in_pat_sc env) argscs pats)
- | NApp (NRef g,[]) -> (* special case : Syndef for @Cstr *)
+ Some (g, [], List.map2 (in_pat_sc scopes) argscs pats)
+ | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *)
test_kind top g;
let () = assert (List.is_empty vars) in
- let (argscs,_) = find_remaining_scopes pats [] g in
- Some (g, List.map2 (in_pat_sc env) argscs pats, [])
+ Some (g, List.map (in_pat false scopes) pats, [])
| NApp (NRef g,args) ->
+ (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
test_kind top g;
let nvars = List.length vars in
if List.length pats < nvars then error_not_enough_arguments loc;
let pats1,pats2 = List.chop nvars pats in
let subst = make_subst vars pats1 in
- let idspl1 = List.map (in_not false loc env (subst, Id.Map.empty) []) args in
+ let idspl1 = List.map (in_not false 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 env) argscs pats2)
+ Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
| _ -> raise Not_found)
- |TrueGlobal g ->
+ | TrueGlobal g ->
test_kind top g;
Dumpglob.add_glob loc g;
let (_,argscs) = find_remaining_scopes [] pats g in
- Some (g,[],List.map2 (fun x -> in_pat false {env with tmp_scope = x}) argscs pats)
+ Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
with Not_found -> None
- and in_pat top env = function
- | CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat top env p, id)
+ and in_pat top scopes = function
+ | CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat top scopes p, id)
| CPatRecord (loc, l) ->
let sorted_fields =
sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in
@@ -1133,56 +1145,58 @@ let drop_notations_pattern looked_for =
| None -> RCPatAtom (loc, None)
| Some (n, head, pl) ->
let pl =
- if !oldfashion_patterns then pl else
+ if !asymmetric_patterns then pl else
let pars = List.make n (CPatAtom (loc, None)) in
List.rev_append pars pl in
- match drop_syndef top env head pl with
+ match drop_syndef top scopes head pl with
|Some (a,b,c) -> RCPatCstr(loc, a, b, c)
|None -> raise (InternalizationError (loc,NotAConstructor head))
end
- | CPatCstr (loc, head, [], pl) ->
+ | CPatCstr (loc, head, None, pl) ->
begin
- match drop_syndef top env head pl with
+ match drop_syndef top scopes head pl with
| Some (a,b,c) -> RCPatCstr(loc, a, b, c)
| None -> raise (InternalizationError (loc,NotAConstructor head))
end
- | CPatCstr (loc, r, expl_pl, pl) ->
- let g = try
- (locate (snd (qualid_of_reference r)))
- with Not_found ->
+ | CPatCstr (loc, r, Some expl_pl, pl) ->
+ let g = try locate (snd (qualid_of_reference r))
+ with Not_found ->
raise (InternalizationError (loc,NotAConstructor r)) in
- let (argscs1,argscs2) = find_remaining_scopes expl_pl pl g in
- RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl, List.map2 (in_pat_sc env) argscs2 pl)
+ if expl_pl == [] then
+ (* Convention: (@r) deactivates all further implicit arguments and scopes *)
+ RCPatCstr (loc, g, List.map (in_pat false scopes) pl, [])
+ else
+ (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
+ (* but not scopes in expl_pl *)
+ let (argscs1,_) = find_remaining_scopes expl_pl pl g in
+ RCPatCstr (loc, g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
| CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[])
when Bigint.is_strictly_pos p ->
- fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p))
- (env.tmp_scope,env.scopes))
+ fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
| CPatNotation (_,"( _ )",([a],[]),[]) ->
- in_pat top env a
+ in_pat top scopes a
| CPatNotation (loc, ntn, fullargs,extrargs) ->
let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
- let ((ids',c),df) = Notation.interp_notation loc ntn (env.tmp_scope,env.scopes) in
+ let ((ids',c),df) = Notation.interp_notation loc ntn scopes in
let (ids',idsl',_) = split_by_type ids' in
Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
let substlist = make_subst idsl' argsl in
let subst = make_subst ids' args in
- in_not top loc env (subst,substlist) extrargs c
+ in_not top loc scopes (subst,substlist) extrargs c
| CPatDelimiters (loc, key, e) ->
- in_pat top {env with scopes=find_delimiters_scope loc key::env.scopes;
- tmp_scope = None} e
- | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p
- (env.tmp_scope,env.scopes))
+ in_pat top (None,find_delimiters_scope loc key::snd scopes) e
+ | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes)
| CPatAtom (loc, Some id) ->
begin
- match drop_syndef top env id [] with
+ match drop_syndef top scopes id [] with
|Some (a,b,c) -> RCPatCstr (loc, a, b, c)
|None -> RCPatAtom (loc, Some (find_pattern_variable id))
end
| CPatAtom (loc,None) -> RCPatAtom (loc,None)
| CPatOr (loc, pl) ->
- RCPatOr (loc,List.map (in_pat top env) pl)
- and in_pat_sc env x = in_pat false {env with tmp_scope = x}
- and in_not top loc env (subst,substlist as fullsubst) args = function
+ RCPatOr (loc,List.map (in_pat top scopes) pl)
+ and in_pat_sc scopes x = in_pat false (x,snd scopes)
+ and in_not top loc scopes (subst,substlist as fullsubst) args = function
| NVar id ->
let () = assert (List.is_empty args) in
begin
@@ -1190,8 +1204,7 @@ let drop_notations_pattern looked_for =
(* of the notations *)
try
let (a,(scopt,subscopes)) = Id.Map.find id subst in
- in_pat top {env with scopes=subscopes@env.scopes;
- tmp_scope = scopt} a
+ in_pat top (scopt,subscopes@snd scopes) a
with Not_found ->
if Id.equal id ldots_var then RCPatAtom (loc,Some id) else
anomaly (str "Unbound pattern notation variable: " ++ Id.print id)
@@ -1199,23 +1212,23 @@ let drop_notations_pattern looked_for =
| NRef g ->
ensure_kind top loc g;
let (_,argscs) = find_remaining_scopes [] args g in
- RCPatCstr (loc, g, [], List.map2 (in_pat_sc env) argscs args)
+ RCPatCstr (loc, g, [], List.map2 (in_pat_sc scopes) argscs args)
| NApp (NRef g,pl) ->
ensure_kind top loc g;
let (argscs1,argscs2) = find_remaining_scopes pl args g in
RCPatCstr (loc, g,
- List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl,
- List.map2 (in_pat_sc env) argscs2 args)
+ List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
+ List.map (in_pat false scopes) args, [])
| NList (x,_,iter,terminator,lassoc) ->
if not (List.is_empty args) then user_err_loc
(loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns.");
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (l,(scopt,subscopes)) = Id.Map.find x substlist in
- let termin = in_not top loc env fullsubst [] terminator in
+ let termin = in_not top loc scopes fullsubst [] terminator in
List.fold_right (fun a t ->
let nsubst = Id.Map.add x (a, (scopt, subscopes)) subst in
- let u = in_not false loc env (nsubst, substlist) [] iter in
+ let u = in_not false loc scopes (nsubst, substlist) [] iter in
subst_pat_iterator ldots_var t u)
(if lassoc then List.rev l else l) termin
with Not_found ->
@@ -1238,7 +1251,7 @@ let rec intern_pat genv aliases pat =
let aliases' = merge_aliases aliases id in
intern_pat genv aliases' p
| RCPatCstr (loc, head, expl_pl, pl) ->
- if !oldfashion_patterns then
+ if !asymmetric_patterns then
let len = if List.is_empty expl_pl then Some (List.length pl) else None in
let c,idslpl1 = find_constructor loc len head in
let with_letin =
@@ -1263,29 +1276,27 @@ let rec intern_pat genv aliases pat =
check_or_pat_variables loc ids (List.tl idsl);
(ids,List.flatten pl')
-let intern_cases_pattern genv env aliases pat =
+let intern_cases_pattern genv scopes aliases pat =
intern_pat genv aliases
- (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) env pat)
+ (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
-let intern_ind_pattern genv env pat =
+let intern_ind_pattern genv scopes pat =
let no_not =
try
- drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) env pat
+ drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type loc
- in
+ in
match no_not with
- | RCPatCstr (loc, head,expl_pl, pl) ->
- let c = (function IndRef ind -> ind
- |_ -> error_bad_inductive_type loc) head in
+ | RCPatCstr (loc, head, expl_pl, pl) ->
+ let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type loc) head in
let with_letin, pl2 = add_implicits_check_ind_length genv loc c
(List.length expl_pl) pl in
let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in
let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
(with_letin,
match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with
- |_,[_,pl] ->
- (c,chop_params_pattern loc c pl with_letin)
- |_ -> error_bad_inductive_type loc)
+ | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
+ | _ -> error_bad_inductive_type loc)
| x -> error_bad_inductive_type (raw_cases_pattern_expr_loc x)
(**********************************************************************)
@@ -1495,36 +1506,44 @@ let internalize globalenv env allow_patvar lvar c =
intern env app
end
| CCases (loc, sty, rtnpo, tms, eqns) ->
- let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
- Option.fold_left (fun x tt -> List.fold_right Id.Set.add (ids_of_cases_indtype tt) x)
- (Option.fold_left (fun x (_,y) -> match y with | Name y' -> Id.Set.add y' x |_ -> x) acc na)
- inb) 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 env' = Id.Set.fold
- (fun var bli -> push_name_env lvar (Variable,[],[],[]) bli (Loc.ghost,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 rec aux = function
- |[] -> []
- |(_,PatVar _) :: q -> aux q
- |l -> l
- in aux match_from_in in
+ 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 (_,y) -> name_fold Id.Set.add y acc) acc na)
+ inb) 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 env' = Id.Set.fold
+ (fun var bli -> push_name_env lvar (Variable,[],[],[]) bli (Loc.ghost,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 rec aux = function
+ | [] -> []
+ | (_,PatVar _) :: q -> aux q
+ | l -> l
+ in aux match_from_in in
let rtnpo = match stripped_match_from_in with
| [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *)
- | l -> let thevars,thepats=List.split l in
- Some (
- GCases(Loc.ghost,Term.RegularStyle,(* Some (GSort (Loc.ghost,GType None)) *)None, (* "return Type" *)
- List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *)
- [Loc.ghost,[],thepats, (* "|p1,..,pn" *)
- Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) rtnpo; (* "=> P" is there were a P "=> _" else *)
- Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
- GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None) (* "=> _" *)]))
+ | l ->
+ (* Build a return predicate by expansion of the patterns of the "in" clause *)
+ let thevars,thepats = List.split l in
+ let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in
+ let sub_tms = List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars (* "match v1,..,vn" *) in
+ let main_sub_eqn =
+ (Loc.ghost,[],thepats, (* "|p1,..,pn" *)
+ Option.cata (intern_type env')
+ (GHole(Loc.ghost,Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
+ rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
+ let catch_all_sub_eqn =
+ if List.for_all (irrefutable globalenv) thepats then [] else
+ [Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
+ GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None)] (* "=> _" *) in
+ Some (GCases(Loc.ghost,Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
in
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
GCases (loc, sty, rtnpo, tms, List.flatten eqns')
@@ -1591,8 +1610,7 @@ let internalize globalenv env allow_patvar lvar c =
(* Expands a multiple pattern into a disjunction of multiple patterns *)
and intern_multiple_pattern env n (loc,pl) =
- let idsl_pll =
- List.map (intern_cases_pattern globalenv {env with tmp_scope = None} empty_alias) pl in
+ let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in
check_number_of_pattern loc n pl;
product_of_cases_patterns [] idsl_pll
@@ -1618,7 +1636,7 @@ let internalize globalenv env allow_patvar lvar c =
(loc,eqn_ids,pl,rhs')) pll
and intern_case_item env forbidden_names_for_gen (tm,na,t) =
- (*the "match" part *)
+ (* the "match" part *)
let tm' = intern env tm in
(* the "as" part *)
let extra_id,na = match tm', na with
@@ -1629,9 +1647,7 @@ let internalize globalenv env allow_patvar lvar c =
(* the "in" part *)
let match_td,typ = match t with
| Some t ->
- let tids = ids_of_cases_indtype t in
- let tids = List.fold_right Id.Set.add tids Id.Set.empty in
- let with_letin,(ind,l) = intern_ind_pattern globalenv {env with ids = tids; tmp_scope = None} t in
+ let with_letin,(ind,l) = intern_ind_pattern globalenv (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")])
@@ -1643,15 +1659,15 @@ let internalize globalenv env allow_patvar lvar c =
let (match_to_do,nal) =
let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc =
let add_name l = function
- |_,Anonymous -> l
- |loc,(Name y as x) -> (y,PatVar(loc,x)) :: l in
+ | _,Anonymous -> l
+ | loc,(Name y as x) -> (y,PatVar(loc,x)) :: l in
match case_rel_ctxt,arg_pats with
(* LetIn in the rel_context *)
| LocalDef _ :: t, l when not with_letin ->
canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc)
- |[],[] ->
+ | [],[] ->
(add_name match_acc na, var_acc)
- |_::t,PatVar (loc,x)::tt ->
+ | _::t,PatVar (loc,x)::tt ->
canonize_args t tt forbidden_names
(add_name match_acc (loc,x)) ((loc,x)::var_acc)
| (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
@@ -1659,7 +1675,7 @@ let internalize globalenv env allow_patvar lvar c =
Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in
canonize_args t tt (fresh::forbidden_names)
((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
- |_ -> assert false in
+ | _ -> assert false in
let _,args_rel =
List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
canonize_args args_rel l (Id.Set.elements forbidden_names_for_gen) [] [] in
@@ -1749,7 +1765,7 @@ let extract_ids env =
Id.Set.empty
let scope_of_type_kind = function
- | IsType -> Some Notation.type_scope
+ | IsType -> Notation.current_type_scope_name ()
| OfType typ -> compute_type_scope typ
| WithoutTypeConstraint -> None
@@ -1773,9 +1789,7 @@ let intern_type env c = intern_gen IsType env c
let intern_pattern globalenv patt =
try
- intern_cases_pattern globalenv {ids = extract_ids globalenv; unb = false;
- tmp_scope = None; scopes = [];
- impls = empty_internalization_env} empty_alias patt
+ intern_cases_pattern globalenv (None,[]) empty_alias patt
with
InternalizationError (loc,e) ->
user_err_loc (loc,"internalize",explain_internalization_error e)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 44a62ef379..931fc1ca40 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -141,7 +141,7 @@ let interval loc =
let dump_ref loc filepath modpath ident ty =
match !glob_output with
| Feedback ->
- Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
+ Feedback.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
| NoGlob -> ()
| _ when not (Loc.is_ghost loc) ->
let bl,el = interval loc in
@@ -172,7 +172,7 @@ let cook_notation df sc =
(* - all single quotes in terminal tokens are doubled *)
(* - characters < 32 are represented by '^A, '^B, '^C, etc *)
(* The output is decoded in function Index.prepare_entry of coqdoc *)
- let ntn = String.make (String.length df * 3) '_' in
+ let ntn = String.make (String.length df * 5) '_' in
let j = ref 0 in
let l = String.length df - 1 in
let i = ref 0 in
@@ -240,7 +240,7 @@ let dump_binding loc id = ()
let dump_def ty loc secpath id =
if !glob_output = Feedback then
- Pp.feedback (Feedback.GlobDef (loc, id, secpath, ty))
+ Feedback.feedback (Feedback.GlobDef (loc, id, secpath, ty))
else
let bl,el = interval loc in
dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 751b03a4a8..567150a5d6 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -310,7 +310,7 @@ let implicits_of_glob_constr ?(with_products=true) l =
else
let () = match bk with
| Implicit ->
- msg_warning (strbrk "Ignoring implicit status of product binder " ++
+ Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++
pr_name na ++ strbrk " and following binders")
| _ -> ()
in []
diff --git a/interp/notation.ml b/interp/notation.ml
index 04918bf7dd..b19fd9e1fe 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -13,7 +13,6 @@ open Pp
open Bigint
open Names
open Term
-open Nametab
open Libnames
open Globnames
open Constrexpr
@@ -65,11 +64,9 @@ let empty_scope = {
}
let default_scope = "" (* empty name, not available from outside *)
-let type_scope = "type_scope" (* special scope used for interpreting types *)
let init_scope_map () =
- scope_map := String.Map.add default_scope empty_scope !scope_map;
- scope_map := String.Map.add type_scope empty_scope !scope_map
+ scope_map := String.Map.add default_scope empty_scope !scope_map
(**********************************************************************)
(* Operations on scopes *)
@@ -187,7 +184,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 ->
- msg_warning
+ Feedback.msg_warning
(str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
scope_map := String.Map.add scope newsc !scope_map
end;
@@ -195,7 +192,7 @@ let declare_delimiters scope key =
let oldscope = String.Map.find key !delimiters_map in
if String.equal oldscope scope then ()
else begin
- msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
+ Feedback.msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
delimiters_map := String.Map.add key scope !delimiters_map
end
with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map
@@ -204,7 +201,7 @@ let remove_delimiters scope =
let sc = find_scope scope in
let newsc = { sc with delimiters = None } in
match sc.delimiters with
- | None -> msg_warning (str "No bound key for scope " ++ str scope ++ str ".")
+ | None -> Feedback.msg_warning (str "No bound key for scope " ++ str scope ++ str ".")
| Some key ->
scope_map := String.Map.add scope newsc !scope_map;
try
@@ -314,7 +311,9 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
patl
let mkNumeral n = Numeral n
-let mkString s = String s
+let mkString = function
+| None -> None
+| Some s -> if Unicode.is_utf8 s then Some (String s) else None
let delay dir int loc x = (dir, (fun () -> int loc x))
@@ -326,7 +325,7 @@ let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
declare_prim_token_interpreter sc
(fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
- (patl, (fun r -> Option.map mkString (uninterp r)), inpat)
+ (patl, (fun r -> mkString (uninterp r)), inpat)
let check_required_module loc sc (sp,d) =
try let _ = Nametab.global_of_path sp in ()
@@ -389,7 +388,7 @@ let declare_notation_interpretation ntn scopt pat df =
let which_scope = match scopt with
| None -> mt ()
| Some _ -> str " in scope " ++ str scope in
- msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
+ Feedback.msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
in
let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in
let () = scope_map := String.Map.add scope sc !scope_map in
@@ -557,23 +556,16 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
(**********************************************************************)
(* Mapping classes to scopes *)
-type scope_class = ScopeRef of global_reference | ScopeSort
+open Classops
-let scope_class_compare sc1 sc2 = match sc1, sc2 with
-| ScopeRef gr1, ScopeRef gr2 -> RefOrdered.compare gr1 gr2
-| ScopeRef _, ScopeSort -> -1
-| ScopeSort, ScopeRef _ -> 1
-| ScopeSort, ScopeSort -> 0
+type scope_class = cl_typ
-let scope_class_of_reference x = ScopeRef x
+let scope_class_compare : scope_class -> scope_class -> int =
+ cl_typ_ord
let compute_scope_class t =
- let t', _ = decompose_appvect (Reductionops.whd_betaiotazeta Evd.empty t) in
- match kind_of_term t' with
- | Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t')
- | Proj (p, c) -> ScopeRef (ConstRef (Projection.constant p))
- | Sort _ -> ScopeSort
- | _ -> raise Not_found
+ let (cl,_,_) = find_class_type Evd.empty t in
+ cl
module ScopeClassOrd =
struct
@@ -584,7 +576,7 @@ end
module ScopeClassMap = Map.Make(ScopeClassOrd)
let initial_scope_class_map : scope_name ScopeClassMap.t =
- ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
+ ScopeClassMap.empty
let scope_class_map = ref initial_scope_class_map
@@ -618,8 +610,11 @@ let compute_arguments_scope t = fst (compute_arguments_scope_full t)
let compute_type_scope t =
find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None)
-let compute_scope_of_global ref =
- find_scope_class_opt (Some (ScopeRef ref))
+let current_type_scope_name () =
+ find_scope_class_opt (Some CL_SORT)
+
+let scope_class_of_class (x : cl_typ) : scope_class =
+ x
(** Updating a scope list, thanks to a list of argument classes
and the current Bind Scope base. When some current scope
@@ -651,12 +646,8 @@ let load_arguments_scope _ (_,(_,r,scl,cls)) =
let cache_arguments_scope o =
load_arguments_scope 1 o
-let subst_scope_class subst cs = match cs with
- | ScopeSort -> Some cs
- | ScopeRef t ->
- let (t',c) = subst_global subst t in
- if t == t' then Some cs
- else try Some (compute_scope_class c) with Not_found -> None
+let subst_scope_class subst cs =
+ try Some (subst_cl_typ subst cs) with Not_found -> None
let subst_arguments_scope (subst,(req,r,scl,cls)) =
let r' = fst (subst_global subst r) in
@@ -789,9 +780,7 @@ let pr_delimiters_info = function
let classes_of_scope sc =
ScopeClassMap.fold (fun cl sc' l -> if String.equal sc sc' then cl::l else l) !scope_class_map []
-let pr_scope_class = function
- | ScopeSort -> str "Sort"
- | ScopeRef t -> pr_global_env Id.Set.empty t
+let pr_scope_class = pr_class
let pr_scope_classes sc =
let l = classes_of_scope sc in
diff --git a/interp/notation.mli b/interp/notation.mli
index 7885814c75..480979ccc3 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -29,7 +29,6 @@ type scopes (** = [scope_name list] *)
type local_scopes = tmp_scope_name option * scope_name list
-val type_scope : scope_name
val declare_scope : scope_name -> unit
val current_scopes : unit -> scopes
@@ -153,7 +152,9 @@ val find_arguments_scope : global_reference -> scope_name option list
type scope_class
-val scope_class_of_reference : global_reference -> scope_class
+(** Comparison of scope_class *)
+val scope_class_compare : scope_class -> scope_class -> int
+
val subst_scope_class :
Mod_subst.substitution -> scope_class -> scope_class option
@@ -162,7 +163,11 @@ val declare_ref_arguments_scope : global_reference -> unit
val compute_arguments_scope : Term.types -> scope_name option list
val compute_type_scope : Term.types -> scope_name option
-val compute_scope_of_global : global_reference -> scope_name option
+
+(** Get the current scope bound to Sortclass, if it exists *)
+val current_type_scope_name : unit -> scope_name option
+
+val scope_class_of_class : Classops.cl_typ -> scope_class
(** Building notation key *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 6561000c47..b4cf6e9430 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -12,15 +12,103 @@ open Util
open Names
open Nameops
open Globnames
+open Decl_kinds
open Misctypes
open Glob_term
open Glob_ops
open Mod_subst
open Notation_term
-open Decl_kinds
(**********************************************************************)
-(* Re-interpret a notation as a glob_constr, taking care of binders *)
+(* Utilities *)
+
+let on_true_do b f c = if b then (f c; b) else b
+
+let compare_glob_constr f add t1 t2 = match t1,t2 with
+ | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2
+ | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
+ | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
+ | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
+ when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
+ on_true_do (f ty1 ty2 && f c1 c2) add na1
+ | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
+ when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
+ on_true_do (f ty1 ty2 && f c1 c2) add na1
+ | GHole _, GHole _ -> true
+ | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
+ | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 ->
+ on_true_do (f b1 b2 && f c1 c2) add na1
+ | (GCases _ | GRec _
+ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
+ | _,(GCases _ | GRec _
+ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _)
+ -> error "Unsupported construction in recursive notations."
+ | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _
+ | GHole _ | GSort _ | GLetIn _), _
+ -> false
+
+let rec eq_notation_constr t1 t2 = match t1, t2 with
+| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NVar id1, NVar id2 -> Id.equal id1 id2
+| NApp (t1, a1), NApp (t2, a2) ->
+ eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2
+| 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 t1 t2 &&
+ eq_notation_constr u1 u2 && b1 == b2
+| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
+ Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
+ Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
+ Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
+ eq_notation_constr u1 u2
+| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) ->
+ Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| 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 t1 t2
+ in
+ let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
+ let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
+ eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
+ in
+ Option.equal eq_notation_constr o1 o2 &&
+ List.equal eqf r1 r2 &&
+ List.equal eqpat p1 p2
+| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
+ List.equal Name.equal nas1 nas2 &&
+ Name.equal na1 na2 &&
+ Option.equal eq_notation_constr o1 o2 &&
+ eq_notation_constr t1 t2 &&
+ eq_notation_constr u1 u2
+| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
+ eq_notation_constr t1 t2 &&
+ Name.equal na1 na2 &&
+ Option.equal eq_notation_constr o1 o2 &&
+ eq_notation_constr u1 u2 &&
+ eq_notation_constr r1 r2
+| 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 o1 o2 &&
+ eq_notation_constr t1 t2
+ in
+ Array.equal Id.equal ids1 ids2 &&
+ Array.equal (List.equal eq) ts1 ts2 &&
+ Array.equal eq_notation_constr us1 us2 &&
+ Array.equal eq_notation_constr rs1 rs2
+| NSort s1, NSort s2 ->
+ Miscops.glob_sort_eq s1 s2
+| NCast (t1, c1), NCast (t2, c2) ->
+ eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2
+| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
+ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
+ | NRec _ | NSort _ | NCast _), _ -> false
+
+(**********************************************************************)
+(* Re-interpret a notation as a glob_constr, taking care of binders *)
let name_to_ident = function
| Anonymous -> Errors.error "This expression should be a simple identifier."
@@ -105,7 +193,6 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
| NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k)
| NSort x -> GSort (loc,x)
| NHole (x, naming, arg) -> GHole (loc, x, naming, arg)
- | NPatVar n -> GPatVar (loc,(false,n))
| NRef x -> GRef (loc,x,None)
let glob_constr_of_notation_constr loc x =
@@ -113,7 +200,7 @@ let glob_constr_of_notation_constr loc x =
glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x
in aux () x
-(****************************************************************************)
+(******************************************************************************)
(* Translating a glob_constr into a notation, interpreting recursive patterns *)
let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r)
@@ -143,96 +230,6 @@ let split_at_recursive_part c =
| GVar (_,v) when Id.equal v ldots_var -> (* Not enough context *) raise Not_found
| _ -> outer_iterator, c
-let on_true_do b f c = if b then (f c; b) else b
-
-let compare_glob_constr f add t1 t2 = match t1,t2 with
- | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2
- | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
- | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
- | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
- when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
- on_true_do (f ty1 ty2 && f c1 c2) add na1
- | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
- when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
- on_true_do (f ty1 ty2 && f c1 c2) add na1
- | GHole _, GHole _ -> true
- | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
- | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 ->
- on_true_do (f b1 b2 && f c1 c2) add na1
- | (GCases _ | GRec _
- | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
- | _,(GCases _ | GRec _
- | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _)
- -> error "Unsupported construction in recursive notations."
- | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _
- | GHole _ | GSort _ | GLetIn _), _
- -> false
-
-let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2
-
-let rec eq_notation_constr t1 t2 = match t1, t2 with
-| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
-| NVar id1, NVar id2 -> Id.equal id1 id2
-| NApp (t1, a1), NApp (t2, a2) ->
- eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2
-| 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 t1 t2 &&
- eq_notation_constr u1 u2 && b1 == b2
-| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
- Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
-| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
- Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
-| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
- Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
- eq_notation_constr u1 u2
-| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) ->
- Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
-| 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 t1 t2
- in
- let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
- let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
- eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
- in
- Option.equal eq_notation_constr o1 o2 &&
- List.equal eqf r1 r2 &&
- List.equal eqpat p1 p2
-| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
- List.equal Name.equal nas1 nas2 &&
- Name.equal na1 na2 &&
- Option.equal eq_notation_constr o1 o2 &&
- eq_notation_constr t1 t2 &&
- eq_notation_constr u1 u2
-| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
- eq_notation_constr t1 t2 &&
- Name.equal na1 na2 &&
- Option.equal eq_notation_constr o1 o2 &&
- eq_notation_constr u1 u2 &&
- eq_notation_constr r1 r2
-| 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 o1 o2 &&
- eq_notation_constr t1 t2
- in
- Array.equal Id.equal ids1 ids2 &&
- Array.equal (List.equal eq) ts1 ts2 &&
- Array.equal eq_notation_constr us1 us2 &&
- Array.equal eq_notation_constr rs1 rs2
-| NSort s1, NSort s2 ->
- Miscops.glob_sort_eq s1 s2
-| NPatVar p1, NPatVar p2 ->
- Id.equal p1 p2
-| NCast (t1, c1), NCast (t2, c2) ->
- eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2
-| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
- | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NPatVar _ | NCast _), _ -> false
-
-
let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1)
let check_is_hole id = function GHole _ -> () | t ->
@@ -352,8 +349,7 @@ let notation_constr_and_vars_of_glob_constr a =
| GSort (_,s) -> NSort s
| GHole (_,w,naming,arg) -> NHole (w, naming, arg)
| GRef (_,r,_) -> NRef r
- | GPatVar (_,(_,n)) -> NPatVar n
- | GEvar _ ->
+ | GEvar _ | GPatVar _ ->
error "Existential variables not allowed in notations."
in
@@ -413,6 +409,7 @@ let notation_constr_of_glob_constr nenv a =
let () = check_variables nenv found in
a
+(**********************************************************************)
(* Substitution of kernel names, avoiding a list of bound identifiers *)
let notation_constr_of_constr avoiding t =
@@ -526,7 +523,7 @@ let rec subst_notation_constr subst bound raw =
if dll' == dll && tl' == tl && bl' == bl then raw else
NRec (fk,idl,dll',tl',bl')
- | NPatVar _ | NSort _ -> raw
+ | NSort _ -> raw
| NHole (knd, naming, solve) ->
let nknd = match knd with
@@ -548,7 +545,8 @@ let subst_interpretation subst (metas,pat) =
let bound = List.map fst metas in
(metas,subst_notation_constr subst bound pat)
-(* Pattern-matching glob_constr and notation_constr *)
+(**********************************************************************)
+(* Pattern-matching a [glob_constr] against a [notation_constr] *)
let abstract_return_type_context pi mklam tml rtno =
Option.map (fun rtn ->
@@ -782,7 +780,6 @@ 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
- | GPatVar (_,(_,n1)), NPatVar n2 when Id.equal n1 n2 -> sigma
| GApp (loc,f1,l1), NApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
let f1,l1,f2,l2 =
@@ -854,15 +851,21 @@ let rec match_ inner u alp metas sigma a1 a2 =
otherwise how to ensure it corresponds to a well-typed eta-expansion;
we make an exception for types which are metavariables: this is useful e.g.
to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
- | b1, NLambda (Name id,(NHole _ | NVar _ as t2),b2) when inner ->
- let id' = Namegen.next_ident_away id (free_glob_vars b1) in
+ | b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
+ let avoid =
+ free_glob_vars b1 @ (* as in Namegen: *) glob_visible_short_qualid b1 in
+ let id' = Namegen.next_ident_away id avoid in
let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
let sigma = match t2 with
| NHole _ -> sigma
| NVar id2 -> bind_term_env alp sigma id2 t1
| _ -> assert false in
- match_in u alp metas (add_bindinglist_env sigma id [(Name id',Explicit,None,t1)])
- (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
+ let (alp,sigma) =
+ if is_bindinglist_meta id metas then
+ alp, add_bindinglist_env sigma id [(Name id',Explicit,None,t1)]
+ else
+ match_names metas (alp,sigma) (Name id') na in
+ match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
| (GRec _ | GEvar _), _
| _,_ -> raise No_match
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 280ccfd21f..576c5b943a 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -10,24 +10,28 @@ open Names
open Notation_term
open Glob_term
-(** Utilities about [notation_constr] *)
+(** {5 Utilities about [notation_constr]} *)
-(** Translate a [glob_constr] into a notation given the list of variables
- bound by the notation; also interpret recursive patterns *)
+val eq_notation_constr : notation_constr -> notation_constr -> bool
-val notation_constr_of_glob_constr : notation_interp_env ->
- glob_constr -> notation_constr
+(** Substitution of kernel names in interpretation data *)
+val subst_interpretation :
+ Mod_subst.substitution -> interpretation -> interpretation
+
(** Name of the special identifier used to encode recursive notations *)
+
val ldots_var : Id.t
-(** Equality of [glob_constr] (warning: only partially implemented) *)
-(** FIXME: nothing to do here *)
-val eq_glob_constr : glob_constr -> glob_constr -> bool
+(** {5 Translation back and forth between [glob_constr] and [notation_constr] *)
-val eq_notation_constr : notation_constr -> notation_constr -> bool
+(** Translate a [glob_constr] into a notation given the list of variables
+ bound by the notation; also interpret recursive patterns *)
+
+val notation_constr_of_glob_constr : notation_interp_env ->
+ glob_constr -> notation_constr
-(** Re-interpret a notation as a [glob_constr], taking care of binders *)
+(** Re-interpret a notation as a [glob_constr], taking care of binders *)
val glob_constr_of_notation_constr_with_binders : Loc.t ->
('a -> Name.t -> 'a * Name.t) ->
@@ -36,6 +40,8 @@ val glob_constr_of_notation_constr_with_binders : Loc.t ->
val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
+(** {5 Matching a notation pattern against a [glob_constr] *)
+
(** [match_notation_constr] matches a [glob_constr] against a notation
interpretation; raise [No_match] if the matching fails *)
@@ -55,9 +61,5 @@ val match_notation_constr_ind_pattern :
((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) *
(int * cases_pattern list)
-(** Substitution of kernel names in interpretation data *)
-
-val subst_interpretation :
- Mod_subst.substitution -> interpretation -> interpretation
+(** {5 Matching a notation pattern against a [glob_constr] *)
-val add_patterns_for_params : inductive -> cases_pattern list -> cases_pattern list
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 9c3ed94130..2a7d52e3af 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -7,24 +7,29 @@
(************************************************************************)
open Genarg
+open Geninterp
+
+let make0 ?dyn name =
+ let wit = Genarg.make0 name in
+ let () = register_val0 wit dyn in
+ wit
let wit_unit : unit uniform_genarg_type =
- make0 None "unit"
+ make0 "unit"
let wit_bool : bool uniform_genarg_type =
- make0 None "bool"
+ make0 "bool"
let wit_int : int uniform_genarg_type =
- make0 None "int"
+ make0 "int"
let wit_string : string uniform_genarg_type =
- make0 None "string"
+ make0 "string"
let wit_pre_ident : string uniform_genarg_type =
- make0 None "preident"
+ make0 ~dyn:(val_tag (topwit wit_string)) "preident"
+
+(** Aliases for compatibility *)
-let () = register_name0 wit_unit "Stdarg.wit_unit"
-let () = register_name0 wit_bool "Stdarg.wit_bool"
-let () = register_name0 wit_int "Stdarg.wit_int"
-let () = register_name0 wit_string "Stdarg.wit_string"
-let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident"
+let wit_integer = wit_int
+let wit_preident = wit_pre_ident
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index d8904dab87..e1f648d7fc 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -19,3 +19,8 @@ val wit_int : int uniform_genarg_type
val wit_string : string uniform_genarg_type
val wit_pre_ident : string uniform_genarg_type
+
+(** Aliases for compatibility *)
+
+val wit_integer : int uniform_genarg_type
+val wit_preident : string uniform_genarg_type
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index db548ec326..891b64fa11 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -93,7 +93,7 @@ let is_verbose_compat () =
let verbose_compat kn def = function
| Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
let act =
- if !verbose_compat_notations then msg_warning else errorlabstrm ""
+ if !verbose_compat_notations then Feedback.msg_warning else errorlabstrm ""
in
let pp_def = match def with
| [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 8293f7f88d..91099bbb19 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -19,14 +19,14 @@ open Constrexpr_ops
(*i*)
-let oldfashion_patterns = ref (false)
+let asymmetric_patterns = ref (false)
let _ = Goptions.declare_bool_option {
Goptions.optsync = true; Goptions.optdepr = false;
Goptions.optname =
"Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments";
Goptions.optkey = ["Asymmetric";"Patterns"];
- Goptions.optread = (fun () -> !oldfashion_patterns);
- Goptions.optwrite = (fun a -> oldfashion_patterns:=a);
+ Goptions.optread = (fun () -> !asymmetric_patterns);
+ Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
}
(**********************************************************************)
@@ -52,7 +52,7 @@ let rec cases_pattern_fold_names f a = function
List.fold_left (cases_pattern_fold_names f) a patl
| CPatCstr (_,_,patl1,patl2) ->
List.fold_left (cases_pattern_fold_names f)
- (List.fold_left (cases_pattern_fold_names f) a patl1) patl2
+ (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2
| CPatNotation (_,_,(patl,patll),patl') ->
List.fold_left (cases_pattern_fold_names f)
(List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
@@ -67,7 +67,7 @@ let ids_of_pattern_list =
Id.Set.empty
let ids_of_cases_indtype p =
- Id.Set.elements (cases_pattern_fold_names Id.Set.add Id.Set.empty p)
+ cases_pattern_fold_names Id.Set.add Id.Set.empty p
let ids_of_cases_tomatch tms =
List.fold_right
@@ -132,7 +132,7 @@ let fold_constr_expr_with_binders g f n acc = function
fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
| CCoFix (loc,_,_) ->
- msg_warning (strbrk "Capture check in multiple binders not done"); acc
+ Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
let free_vars_of_constr_expr c =
let rec aux bdvars l = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1e867c19c6..58edd4ddf8 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -12,7 +12,7 @@ open Constrexpr
(** Topconstr *)
-val oldfashion_patterns : bool ref
+val asymmetric_patterns : bool ref
(** Utilities on constr_expr *)
@@ -23,7 +23,7 @@ val free_vars_of_constr_expr : constr_expr -> Id.Set.t
val occur_var_constr_expr : Id.t -> constr_expr -> bool
(** Specific function for interning "in indtype" syntax of "match" *)
-val ids_of_cases_indtype : cases_pattern_expr -> Id.t list
+val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
val split_at_annot : local_binder list -> Id.t located option -> local_binder list * local_binder list
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 01:43:22 +0000