aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml13
-rw-r--r--interp/constrintern.ml51
-rw-r--r--interp/constrintern.mli2
-rw-r--r--interp/notation.ml3
-rw-r--r--interp/notation.mli3
-rw-r--r--interp/notation_ops.ml40
-rw-r--r--interp/notation_ops.mli2
-rw-r--r--interp/syntax_def.ml20
-rw-r--r--interp/syntax_def.mli3
-rw-r--r--interp/topconstr.ml19
10 files changed, 97 insertions, 59 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e71daef999..dd8a48b85e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -149,17 +149,8 @@ let extern_evar loc n l = CEvar (loc,n,l)
For instance, in the debugger the tables of global references
may be inaccurate *)
-let safe_shortest_qualid_of_global vars r =
- try shortest_qualid_of_global vars r
- with Not_found ->
- match r with
- | VarRef v -> make_qualid DirPath.empty v
- | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c))
- | IndRef (i,_) | ConstructRef ((i,_),_) ->
- make_qualid DirPath.empty Names.(Label.to_id (mind_label i))
-
let default_extern_reference loc vars r =
- Qualid (loc,safe_shortest_qualid_of_global vars r)
+ Qualid (loc,shortest_qualid_of_global vars r)
let my_extern_reference = ref default_extern_reference
@@ -481,7 +472,7 @@ 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 &&
- (not (is_inferable_implicit inctx n imp) || !Flags.beautify_file) &&
+ (not (is_inferable_implicit inctx n imp) || !Flags.beautify) &&
is_significant_implicit (Lazy.force a))
in
if visible then
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4502aa7ace..c916fcd886 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1061,6 +1061,15 @@ let find_pattern_variable = function
| Ident (loc,id) -> id
| Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x))
+let check_duplicate loc fields =
+ let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in
+ let dups = List.duplicates eq fields in
+ match dups with
+ | [] -> ()
+ | (r, _) :: _ ->
+ user_err_loc (loc, "", str "This record defines several times the field " ++
+ pr_reference r ++ str ".")
+
(** [sort_fields ~complete loc fields completer] expects a list
[fields] of field assignments [f = e1; g = e2; ...], where [f, g]
are fields of a record and [e1] are "values" (either terms, when
@@ -1094,6 +1103,7 @@ let sort_fields ~complete loc fields completer =
try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id)
with Not_found ->
anomaly (str "Environment corruption for records") in
+ let () = check_duplicate loc fields in
let (end_index, (* one past the last field index *)
first_field_index, (* index of the first field of the record *)
proj_list) (* list of projections *)
@@ -1400,7 +1410,40 @@ let rec intern_pat genv aliases pat =
check_or_pat_variables loc ids (List.tl idsl);
(ids,List.flatten pl')
+(* [check_no_patcast p] raises an error if [p] contains a cast. This code is a
+ bit ad-hoc, and is due to current restrictions on casts in patterns. We
+ support them only in local binders and only at top level. In fact, they are
+ currently eliminated by the parser. The only reason why they are in the
+ [cases_pattern_expr] type is that the parser needs to factor the "(c : t)"
+ notation with user defined notations (such as the pair). In the long term, we
+ will try to support such casts everywhere, and use them to print the domains
+ of lambdas in the encoding of match in constr. We put this check here and not
+ in the parser because it would require to duplicate the levels of the
+ [pattern] rule. *)
+let rec check_no_patcast = function
+ | CPatCast (loc,_,_) ->
+ CErrors.user_err_loc (loc, "check_no_patcast",
+ Pp.strbrk "Casts are not supported here.")
+ | CPatDelimiters(_,_,p)
+ | CPatAlias(_,p,_) -> check_no_patcast p
+ | CPatCstr(_,_,opl,pl) ->
+ Option.iter (List.iter check_no_patcast) opl;
+ List.iter check_no_patcast pl
+ | CPatOr(_,pl) ->
+ List.iter check_no_patcast pl
+ | CPatNotation(_,_,subst,pl) ->
+ check_no_patcast_subst subst;
+ List.iter check_no_patcast pl
+ | CPatRecord(_,prl) ->
+ List.iter (fun (_,p) -> check_no_patcast p) prl
+ | CPatAtom _ | CPatPrim _ -> ()
+
+and check_no_patcast_subst (pl,pll) =
+ List.iter check_no_patcast pl;
+ List.iter (List.iter check_no_patcast) pll
+
let intern_cases_pattern genv scopes aliases pat =
+ check_no_patcast pat;
intern_pat genv aliases
(drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
@@ -1409,6 +1452,7 @@ let _ =
fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p
let intern_ind_pattern genv scopes pat =
+ check_no_patcast pat;
let no_not =
try
drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
@@ -1558,7 +1602,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let idl_tmp = Array.map
(fun ((loc,id),bl,ty,_) ->
let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
- let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbl in
+ let rbl = List.map (function BDRawDef a -> a | BDPattern _ ->
+ Loc.raise loc (Stream.Error "pattern with quote not allowed after cofix")) rbl in
(List.rev rbl,
intern_type env' ty,env')) dl in
let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') ->
@@ -2003,14 +2048,14 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
tmp_scope = None; scopes = []; impls = impls}
false (empty_ltac_sign, vl) a in
(* Translate and check that [c] has all its free variables bound in [vars] *)
- let a = notation_constr_of_glob_constr nenv c in
+ let a, reversible = notation_constr_of_glob_constr nenv c in
(* Splits variables into those that are binding, bound, or both *)
(* binding and bound *)
let out_scope = function None -> None,[] | Some (a,l) -> a,l in
let vars = Id.Map.map (fun (isonlybinding, sc, typ) ->
(!isonlybinding, out_scope !sc, typ)) vl in
(* Returns [a] and the ordered list of variables with their scopes *)
- vars, a
+ vars, a, reversible
(* Interpret binders and contexts *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index eea76aa310..61e7c6f5cb 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -186,7 +186,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
val interp_notation_constr : ?impls:internalization_env ->
notation_interp_env -> constr_expr ->
(bool * subscopes * notation_var_internalization_type) Id.Map.t *
- notation_constr
+ notation_constr * reversibility_flag
(** Globalization options *)
val parsing_explicit : bool ref
diff --git a/interp/notation.ml b/interp/notation.ml
index d301ed21db..389a1c9dff 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1009,6 +1009,9 @@ let find_notation_parsing_rules ntn =
try pi3 (String.Map.find ntn !notation_rules)
with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn)
+let get_defined_notations () =
+ String.Set.elements @@ String.Map.domain !notation_rules
+
let add_notation_extra_printing_rule ntn k v =
try
notation_rules :=
diff --git a/interp/notation.mli b/interp/notation.mli
index b47e1975e3..2e92a00a8c 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -203,6 +203,9 @@ val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
val find_notation_parsing_rules : notation -> notation_grammar
val add_notation_extra_printing_rule : notation -> string -> string -> unit
+(** Returns notations with defined parsing/printing rules *)
+val get_defined_notations : unit -> notation list
+
(** Rem: printing rules for primitive token are canonical *)
val with_notation_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index cc81a00919..0c5393cf41 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -248,6 +248,10 @@ let check_is_hole id = function GHole _ -> () | t ->
let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
+type recursive_pattern_kind =
+| RecursiveTerms of bool (* associativity *)
+| RecursiveBinders of glob_constr * glob_constr
+
let compare_recursive_parts found f f' (iterator,subc) =
let diff = ref None in
let terminator = ref None in
@@ -269,18 +273,16 @@ let compare_recursive_parts found f f' (iterator,subc) =
let x,y = if lassoc then y,x else x,y in
begin match !diff with
| None ->
- let () = diff := Some (x, y, Some lassoc) in
+ let () = diff := Some (x, y, RecursiveTerms lassoc) in
true
| Some _ -> false
end
| GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term)
| GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) ->
(* We found a binding position where it differs *)
- check_is_hole x t_x;
- check_is_hole y t_y;
begin match !diff with
| None ->
- let () = diff := Some (x, y, None) in
+ let () = diff := Some (x, y, RecursiveBinders (t_x,t_y)) in
aux c term
| Some _ -> false
end
@@ -294,7 +296,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
(* Here, we would need a loc made of several parts ... *)
user_err_loc (subtract_loc loc1 loc2,"",
str "Both ends of the recursive pattern are the same.")
- | Some (x,y,Some lassoc) ->
+ | Some (x,y,RecursiveTerms lassoc) ->
let newfound,x,y,lassoc =
if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) ||
List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found)
@@ -312,17 +314,20 @@ let compare_recursive_parts found f f' (iterator,subc) =
(* found have been collected by compare_constr *)
found := newfound;
NList (x,y,iterator,f (Option.get !terminator),lassoc)
- | Some (x,y,None) ->
+ | Some (x,y,RecursiveBinders (t_x,t_y)) ->
let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
let iterator = f' (subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in
(* found have been collected by compare_constr *)
found := newfound;
+ check_is_hole x t_x;
+ check_is_hole y t_y;
NBinderList (x,y,iterator,f (Option.get !terminator))
else
raise Not_found
let notation_constr_and_vars_of_glob_constr a =
let found = ref ([],[],[]) in
+ let has_ltac = ref false in
let rec aux c =
let keepfound = !found in
(* n^2 complexity but small and done only once per notation *)
@@ -368,7 +373,9 @@ let notation_constr_and_vars_of_glob_constr a =
NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
| GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
| GSort (_,s) -> NSort s
- | GHole (_,w,naming,arg) -> NHole (w, naming, arg)
+ | GHole (_,w,naming,arg) ->
+ if arg != None then has_ltac := true;
+ NHole (w, naming, arg)
| GRef (_,r,_) -> NRef r
| GEvar _ | GPatVar _ ->
error "Existential variables not allowed in notations."
@@ -376,9 +383,10 @@ let notation_constr_and_vars_of_glob_constr a =
in
let t = aux a in
(* Side effect *)
- t, !found
+ t, !found, !has_ltac
-let check_variables nenv (found,foundrec,foundrecbinding) =
+let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) =
+ let injective = ref true in
let recvars = nenv.ninterp_rec_vars in
let fold _ y accu = Id.Set.add y accu in
let useless_vars = Id.Map.fold fold recvars Id.Set.empty in
@@ -401,7 +409,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
error
(Id.to_string x ^
" should not be bound in a recursive pattern of the right-hand side.")
- else nenv.ninterp_only_parse <- true
+ else injective := false
in
let check_pair s x y where =
if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
@@ -421,12 +429,13 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
with Not_found -> check_bound x
end
| NtnInternTypeIdent -> check_bound x in
- Id.Map.iter check_type vars
+ Id.Map.iter check_type vars;
+ !injective
let notation_constr_of_glob_constr nenv a =
- let a, found = notation_constr_and_vars_of_glob_constr a in
- let () = check_variables nenv found in
- a
+ let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in
+ let injective = check_variables_and_reversibility nenv found in
+ a, not has_ltac && injective
(**********************************************************************)
(* Substitution of kernel names, avoiding a list of bound identifiers *)
@@ -436,7 +445,6 @@ let notation_constr_of_constr avoiding t =
let nenv = {
ninterp_var_type = Id.Map.empty;
ninterp_rec_vars = Id.Map.empty;
- ninterp_only_parse = false;
} in
notation_constr_of_glob_constr nenv t
@@ -454,7 +462,7 @@ let rec subst_notation_constr subst bound raw =
| NRef ref ->
let ref',t = subst_global subst ref in
if ref' == ref then raw else
- notation_constr_of_constr bound t
+ fst (notation_constr_of_constr bound t)
| NVar _ -> raw
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 4ebd3ddd80..c8fcbf7410 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -29,7 +29,7 @@ val ldots_var : Id.t
bound by the notation; also interpret recursive patterns *)
val notation_constr_of_glob_constr : notation_interp_env ->
- glob_constr -> notation_constr
+ glob_constr -> notation_constr * reversibility_flag
(** Re-interpret a notation as a [glob_constr], taking care of binders *)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index d2dcbd92aa..2523063e64 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -84,11 +84,6 @@ let declare_syntactic_definition local id onlyparse pat =
let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn)
-let verbose_compat_notations = ref true
-
-let is_verbose_compat () =
- !verbose_compat_notations
-
let pr_compat_warning (kn, def, v) =
let pp_def = match def with
| [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r
@@ -98,11 +93,11 @@ let pr_compat_warning (kn, def, v) =
pr_syndef kn ++ pp_def ++ since
let warn_compatibility_notation =
- CWarnings.create ~name:"compatibility-notation"
- ~category:"deprecated" pr_compat_warning
+ CWarnings.(create ~name:"compatibility-notation"
+ ~category:"deprecated" ~default:Disabled pr_compat_warning)
let verbose_compat kn def = function
- | Some v when is_verbose_compat () && Flags.version_strictly_greater v ->
+ | Some v when Flags.version_strictly_greater v ->
warn_compatibility_notation (kn, def, v)
| _ -> ()
@@ -113,12 +108,3 @@ let search_syntactic_definition kn =
def
open Goptions
-
-let set_verbose_compat_notations =
- declare_bool_option
- { optsync = true;
- optdepr = false;
- optname = "verbose compatibility notations";
- optkey = ["Verbose";"Compat";"Notations"];
- optread = (fun () -> !verbose_compat_notations);
- optwrite = ((:=) verbose_compat_notations) }
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index aa2c9c3c1b..55e2848e69 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -17,6 +17,3 @@ val declare_syntactic_definition : bool -> Id.t ->
Flags.compat_version option -> syndef_interpretation -> unit
val search_syntactic_definition : kernel_name -> syndef_interpretation
-
-(** Option concerning verbose display of compatibility notations *)
-val set_verbose_compat_notations : bool -> unit
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2b860173a6..a397ca82eb 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -22,8 +22,7 @@ open Constrexpr_ops
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.optname = "no parameters in constructors";
Goptions.optkey = ["Asymmetric";"Patterns"];
Goptions.optread = (fun () -> !asymmetric_patterns);
Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
@@ -61,6 +60,9 @@ let rec cases_pattern_fold_names f a = function
| CPatPrim _ | CPatAtom _ -> a
| CPatCast _ -> assert false
+let ids_of_pattern =
+ cases_pattern_fold_names Id.Set.add Id.Set.empty
+
let ids_of_pattern_list =
List.fold_left
(Loc.located_fold_left
@@ -93,8 +95,9 @@ let rec fold_local_binders g f n acc b = function
f n (fold_local_binders g f n' acc b l) t
| LocalRawDef ((_,na),t)::l ->
f n (fold_local_binders g f (name_fold g na n) acc b l) t
- | LocalPattern _::l ->
- assert false
+ | LocalPattern (_,pat,t)::l ->
+ let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
+ Option.fold_left (f n) acc t
| [] ->
f n acc b
@@ -173,7 +176,8 @@ let split_at_annot bl na =
(List.rev ans, LocalRawAssum (r, k, t) :: rest)
end
| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
- | LocalPattern _ :: rest -> assert false
+ | LocalPattern (loc,_,_) :: rest ->
+ Loc.raise loc (Stream.Error "pattern with quote not allowed after fix")
| [] ->
user_err_loc(loc,"",
str "No parameter named " ++ Nameops.pr_id id ++ str".")
@@ -196,8 +200,9 @@ let map_local_binders f g e bl =
(map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl)
| LocalRawDef((loc,na),ty) ->
(name_fold g na e, LocalRawDef((loc,na),f e ty)::bl)
- | LocalPattern _ ->
- assert false in
+ | LocalPattern (loc,pat,t) ->
+ let ids = ids_of_pattern pat in
+ (Id.Set.fold g ids e, LocalPattern (loc,pat,Option.map (f e) t)::bl) in
let (e,rbl) = List.fold_left h (e,[]) bl in
(e, List.rev rbl)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 05:27:20 +0000