summaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /interp
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'interp')
-rw-r--r--interp/constrarg.ml72
-rw-r--r--interp/constrarg.mli43
-rw-r--r--interp/constrexpr_ops.ml106
-rw-r--r--interp/constrexpr_ops.mli5
-rw-r--r--interp/constrextern.ml184
-rw-r--r--interp/constrextern.mli3
-rw-r--r--interp/constrintern.ml845
-rw-r--r--interp/constrintern.mli9
-rw-r--r--interp/coqlib.ml4
-rw-r--r--interp/dumpglob.ml17
-rw-r--r--interp/dumpglob.mli2
-rw-r--r--interp/genintern.ml14
-rw-r--r--interp/implicit_quantifiers.ml24
-rw-r--r--interp/implicit_quantifiers.mli4
-rw-r--r--interp/notation.ml199
-rw-r--r--interp/notation.mli21
-rw-r--r--interp/notation_ops.ml745
-rw-r--r--interp/notation_ops.mli37
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/smartlocate.ml2
-rw-r--r--interp/stdarg.ml25
-rw-r--r--interp/stdarg.mli5
-rw-r--r--interp/syntax_def.ml48
-rw-r--r--interp/syntax_def.mli6
-rw-r--r--interp/topconstr.ml35
-rw-r--r--interp/topconstr.mli4
26 files changed, 1542 insertions, 919 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index d9c60a18..ca828102 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. *)
@@ -19,56 +24,51 @@ let loc_of_or_by_notation f = function
| AN c -> f c
| ByNotation (loc,s,_) -> loc
-let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type =
- Obj.magic t
-
-let wit_int_or_var = unsafe_of_type IntOrVarArgType
+let wit_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"
-
-let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type =
- Genarg.make0 None "tactic"
+ make0 "intropattern"
-let wit_ident = unsafe_of_type IdentArgType
+let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
+ make0 "tactic"
-let wit_var = unsafe_of_type VarArgType
+let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
-let wit_ref = Genarg.make0 None "ref"
+let wit_ident =
+ make0 "ident"
-let wit_quant_hyp = unsafe_of_type QuantHypArgType
+let wit_var =
+ make0 ~dyn:(val_tag (topwit wit_ident)) "var"
-let wit_genarg = unsafe_of_type GenArgType
+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 = unsafe_of_type ConstrArgType
+let wit_constr =
+ make0 "constr"
-let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType
+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 = unsafe_of_type OpenConstrArgType
+let wit_constr_with_bindings = make0 "constr_with_bindings"
-let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
+let wit_bindings = make0 "bindings"
-let wit_bindings = unsafe_of_type BindingsArgType
-
-let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
- Genarg.make0 None "hyp_location_flag"
-
-let wit_red_expr = unsafe_of_type RedExprArgType
+let wit_red_expr = make0 "redexpr"
let wit_clause_dft_concl =
- Genarg.make0 None "clause_dft_concl"
+ make0 "clause_dft_concl"
+
+let wit_destruction_arg =
+ make0 "destruction_arg"
-(** Register location *)
+(** Aliases *)
-let () =
- register_name0 wit_ref "Constrarg.wit_ref";
- 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_uconstr "Constrarg.wit_uconstr";
- register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl";
+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 ebef1ada..6ccd944d 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -26,7 +26,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
(** {5 Additional generic arguments} *)
-val wit_int_or_var : int or_var uniform_genarg_type
+val wit_int_or_var : (int or_var, int or_var, int) genarg_type
val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
@@ -38,39 +38,50 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-val wit_genarg : (raw_generic_argument, glob_generic_argument, typed_generic_argument) 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 :
- (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type
+ (constr_expr, glob_constr_and_expr, constr) genarg_type
val wit_constr_with_bindings :
(constr_expr with_bindings,
glob_constr_and_expr with_bindings,
- constr with_bindings Evd.sigma) genarg_type
+ constr with_bindings delayed_open) genarg_type
val wit_bindings :
(constr_expr bindings,
glob_constr_and_expr bindings,
- constr bindings Evd.sigma) genarg_type
-
-val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type
+ constr bindings delayed_open) 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, glob_tactic_expr) 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
+
+val wit_destruction_arg :
+ (constr_expr with_bindings destruction_arg,
+ glob_constr_and_expr with_bindings destruction_arg,
+ delayed_open_constr_with_bindings destruction_arg) 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 16447002..04429851 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -40,7 +40,7 @@ let names_of_local_assums bl =
List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
let names_of_local_binders bl =
- List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
+ List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalPattern _ -> assert false) bl)
(**********************************************************************)
(* Functions on constr_expr *)
@@ -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
@@ -125,11 +125,10 @@ let rec constr_expr_eq e1 e2 =
Option.equal Int.equal proj1 proj2 &&
constr_expr_eq e1 e2 &&
List.equal args_eq al1 al2
- | CRecord (_, e1, l1), CRecord (_, e2, l2) ->
+ | CRecord (_, l1), CRecord (_, l2) ->
let field_eq (r1, e1) (r2, e2) =
eq_reference r1 r2 && constr_expr_eq e1 e2
in
- Option.equal constr_expr_eq e1 e2 &&
List.equal field_eq l1 l2
| CCases(_,_,r1,a1,brl1), CCases(_,_,r2,a2,brl2) ->
(** Don't care about the case_style *)
@@ -178,7 +177,7 @@ and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_located explicitation_eq) e1 e2 &&
constr_expr_eq a1 a2
-and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) =
+and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
constr_expr_eq e1 e2 &&
Option.equal (eq_located Name.equal) n1 n2 &&
Option.equal cases_pattern_expr_eq p1 p2
@@ -238,7 +237,7 @@ let constr_loc = function
| CLetIn (loc,_,_,_) -> loc
| CAppExpl (loc,_,_) -> loc
| CApp (loc,_,_) -> loc
- | CRecord (loc,_,_) -> loc
+ | CRecord (loc,_) -> loc
| CCases (loc,_,_,_,_) -> loc
| CLetTuple (loc,_,_,_,_) -> loc
| CIf (loc,_,_,_,_) -> loc
@@ -261,6 +260,7 @@ let cases_pattern_expr_loc = function
| CPatRecord (loc, _) -> loc
| CPatPrim (loc,_) -> loc
| CPatDelimiters (loc,_,_) -> loc
+ | CPatCast(loc,_,_) -> loc
let raw_cases_pattern_expr_loc = function
| RCPatAlias (loc,_,_) -> loc
@@ -272,6 +272,7 @@ let local_binder_loc = function
| LocalRawAssum ((loc,_)::_,_,t)
| LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
| LocalRawAssum ([],_,_) -> assert false
+ | LocalPattern (loc,_,_) -> loc
let local_binders_loc bll = match bll with
| [] -> Loc.ghost
@@ -293,23 +294,74 @@ let mkAppC (f,l) =
| CApp (_,g,l') -> CApp (Loc.ghost, g, l' @ l)
| _ -> CApp (Loc.ghost, (None, f), l)
-let rec mkCProdN loc bll c =
- match bll with
- | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
- CProdN (loc,[idl,bk,t],mkCProdN (Loc.merge loc1 loc) bll c)
- | LocalRawDef ((loc1,_) as id,b) :: bll ->
- CLetIn (loc,id,b,mkCProdN (Loc.merge loc1 loc) bll c)
- | [] -> c
- | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
-
-let rec mkCLambdaN loc bll c =
- match bll with
- | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
- CLambdaN (loc,[idl,bk,t],mkCLambdaN (Loc.merge loc1 loc) bll c)
- | LocalRawDef ((loc1,_) as id,b) :: bll ->
- CLetIn (loc,id,b,mkCLambdaN (Loc.merge loc1 loc) bll c)
- | [] -> c
- | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
+let add_name_in_env env n =
+ match snd n with
+ | Anonymous -> env
+ | Name id -> id :: env
+
+let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) ()
+
+let expand_pattern_binders mkC bl c =
+ let rec loop bl c =
+ match bl with
+ | [] -> ([], [], c)
+ | b :: bl ->
+ let (env, bl, c) = loop bl c in
+ match b with
+ | LocalRawDef (n, _) ->
+ let env = add_name_in_env env n in
+ (env, b :: bl, c)
+ | LocalRawAssum (nl, _, _) ->
+ let env = List.fold_left add_name_in_env env nl in
+ (env, b :: bl, c)
+ | LocalPattern (loc, p, ty) ->
+ let ni = Hook.get fresh_var env c in
+ let id = (loc, Name ni) in
+ let b =
+ LocalRawAssum
+ ([id], Default Explicit,
+ match ty with
+ | Some ty -> ty
+ | None -> CHole (loc, None, IntroAnonymous, None))
+ in
+ let e = CRef (Libnames.Ident (loc, ni), None) in
+ let c =
+ CCases
+ (loc, LetPatternStyle, None, [(e,None,None)],
+ [(loc, [(loc,[p])], mkC loc bl c)])
+ in
+ (ni :: env, [b], c)
+ in
+ let (_, bl, c) = loop bl c in
+ (bl, c)
+
+let mkCProdN loc bll c =
+ let rec loop loc bll c =
+ match bll with
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
+ | [] -> c
+ | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
+ | LocalPattern (loc,p,ty) :: bll -> assert false
+ in
+ let (bll, c) = expand_pattern_binders loop bll c in
+ loop loc bll c
+
+let mkCLambdaN loc bll c =
+ let rec loop loc bll c =
+ match bll with
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
+ | [] -> c
+ | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
+ | LocalPattern (loc,p,ty) :: bll -> assert false
+ in
+ let (bll, c) = expand_pattern_binders loop bll c in
+ loop loc bll c
let rec abstract_constr_expr c = function
| [] -> c
@@ -317,6 +369,7 @@ let rec abstract_constr_expr c = function
| LocalRawAssum (idl,bk,t)::bl ->
List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
(abstract_constr_expr c bl)
+ | LocalPattern _::_ -> assert false
let rec prod_constr_expr c = function
| [] -> c
@@ -324,22 +377,23 @@ let rec prod_constr_expr c = function
| LocalRawAssum (idl,bk,t)::bl ->
List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
(prod_constr_expr c bl)
+ | LocalPattern _::_ -> assert false
let coerce_reference_to_id = function
| Ident (_,id) -> id
| Qualid (loc,_) ->
- Errors.user_err_loc (loc, "coerce_reference_to_id",
+ CErrors.user_err_loc (loc, "coerce_reference_to_id",
str "This expression should be a simple identifier.")
let coerce_to_id = function
| CRef (Ident (loc,id),_) -> (loc,id)
- | a -> Errors.user_err_loc
+ | a -> CErrors.user_err_loc
(constr_loc a,"coerce_to_id",
str "This expression should be a simple identifier.")
let coerce_to_name = function
| CRef (Ident (loc,id),_) -> (loc,Name id)
| CHole (loc,_,_,_) -> (loc,Anonymous)
- | a -> Errors.user_err_loc
+ | a -> CErrors.user_err_loc
(constr_loc a,"coerce_to_name",
str "This expression should be a name.")
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 3f5be485..a92da035 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -58,6 +58,11 @@ val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr
val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr
(** Same as [prod_constr_expr], with location *)
+val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t
+val expand_pattern_binders :
+ (Loc.t -> local_binder list -> constr_expr -> constr_expr) ->
+ local_binder list -> constr_expr -> local_binder list * constr_expr
+
(** {6 Destructors}*)
val coerce_reference_to_id : reference -> Id.t
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9df8f9c2..dd8a48b8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -8,7 +8,7 @@
(*i*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -29,6 +29,8 @@ open Notation
open Detyping
open Misctypes
open Decl_kinds
+
+module NamedDecl = Context.Named.Declaration
(*i*)
(* Translation from glob_constr to front constr *)
@@ -147,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
@@ -173,6 +166,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
@@ -264,7 +261,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
@@ -284,7 +281,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;
@@ -297,7 +294,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
@@ -325,15 +322,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 =
@@ -356,7 +353,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
@@ -372,7 +369,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
@@ -380,7 +377,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
@@ -393,9 +390,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
@@ -403,7 +400,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
@@ -411,7 +408,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;
@@ -423,14 +420,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
@@ -462,15 +459,6 @@ let is_needed_for_correct_partial_application tail imp =
exception Expl
-let params_implicit n impl =
- let rec aux n impl =
- if n == 0 then true
- else match impl with
- | [] -> false
- | imp :: impl when is_status_implicit imp -> aux (pred n) impl
- | _ -> false
- in aux n impl
-
(* Implicit args indexes are in ascending order *)
(* inctx is useful only if there is a last argument to be deduced from ctxt *)
let explicitize loc inctx impl (cf,f) args =
@@ -484,15 +472,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) || !Flags.beautify) &&
+ 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
@@ -519,7 +507,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
@@ -541,19 +529,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)
@@ -629,7 +619,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))
@@ -650,8 +640,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;
@@ -686,12 +675,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, None, List.rev (ip projs locals args []))
+ 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
@@ -699,7 +690,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,
@@ -721,26 +712,27 @@ let rec extern inctx scopes vars r =
(cases_predicate_names tml) vars in
let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
let tml = List.map (fun (tm,(na,x)) ->
- let na' = match na,tm with
- | Anonymous, GVar (_, id) ->
- begin match rtntypopt with
- | None -> None
- | Some ntn ->
- if occur_glob_constr id ntn then
- Some (Loc.ghost, Anonymous)
- else None
- end
- | Anonymous, _ -> None
- | Name id, GVar (_,id') when Id.equal id id' -> None
- | Name _, _ -> Some (Loc.ghost,na) in
- (sub_extern false scopes vars tm,
- (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
- extern_ind_pattern_in_scope scopes vars ind fullargs
- ) x))) tml in
+ let na' = match na,tm with
+ | Anonymous, GVar (_, id) ->
+ begin match rtntypopt with
+ | None -> None
+ | Some ntn ->
+ if occur_glob_constr id ntn then
+ Some (Loc.ghost, Anonymous)
+ else None
+ end
+ | Anonymous, _ -> None
+ | Name id, GVar (_,id') when Id.equal id id' -> None
+ | Name _, _ -> Some (Loc.ghost,na) in
+ (sub_extern false scopes vars tm,
+ na',
+ Option.map (fun (loc,ind,nal) ->
+ let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
+ let fullargs = add_cpatt_for_params ind args in
+ extern_ind_pattern_in_scope scopes vars ind fullargs
+ ) x))
+ tml
+ in
let eqns = List.map (extern_eqn inctx scopes vars) eqns in
CCases (loc,sty,rtntypopt',tml,eqns)
@@ -764,6 +756,7 @@ let rec extern inctx scopes vars r =
let listdecl =
Array.mapi (fun i fi ->
let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
+ let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) bl in
let (assums,ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
@@ -780,7 +773,8 @@ let rec extern inctx scopes vars r =
| GCoFix n ->
let listdecl =
Array.mapi (fun i fi ->
- let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in
+ let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) blv.(i) in
+ let (_,ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
((Loc.ghost, fi),bl,extern_typ scopes vars0 tyv.(i),
@@ -797,7 +791,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)
@@ -823,13 +817,13 @@ and factorize_lambda inctx scopes vars na bk aty c =
and extern_local_binder scopes vars = function
[] -> ([],[],[])
- | (na,bk,Some bd,ty)::l ->
+ | (Inl na,bk,Some bd,ty)::l ->
let (assums,ids,l) =
extern_local_binder scopes (name_fold Id.Set.add na vars) l in
(assums,na::ids,
LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l)
- | (na,bk,None,ty)::l ->
+ | (Inl na,bk,None,ty)::l ->
let ty = extern_typ scopes vars ty in
(match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
(assums,ids,LocalRawAssum(nal,k,ty')::l)
@@ -842,11 +836,20 @@ and extern_local_binder scopes vars = function
(na::assums,na::ids,
LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l))
+ | (Inr p,bk,Some bd,ty)::l -> assert false
+
+ | (Inr p,bk,None,ty)::l ->
+ let ty =
+ if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
+ let p = extern_cases_pattern vars p in
+ let (assums,ids,l) = extern_local_binder scopes vars l in
+ (assums,ids, LocalPattern(Loc.ghost,p,ty) :: l)
+
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
@@ -918,10 +921,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
@@ -986,9 +990,12 @@ let rec glob_of_pat env sigma = function
| PRef ref -> GRef (loc,ref,None)
| PVar id -> GVar (loc,id)
| PEvar (evk,l) ->
- let test (id,_,_) = function PVar id' -> Id.equal id id' | _ -> false in
+ let test decl = function PVar id' -> Id.equal (NamedDecl.get_id decl) id' | _ -> false in
let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
- let id = Evd.evar_ident evk sigma in
+ let id = match Evd.evar_ident evk sigma with
+ | None -> Id.of_string "__"
+ | Some id -> id
+ in
GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l)
| PRel n ->
let id = try match lookup_name_of_rel n env with
@@ -1045,4 +1052,5 @@ let extern_constr_pattern env sigma pat =
let extern_rel_context where env sigma sign =
let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
let vars = vars_of_env env in
+ let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in
pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index bf1f529c..f617faa3 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Termops
open Environ
open Libnames
@@ -42,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
val extern_sort : Evd.evar_map -> sorts -> glob_sort
val extern_rel_context : constr option -> env -> Evd.evar_map ->
- rel_context -> local_binder list
+ Context.Rel.t -> local_binder list
(** Printing options *)
val print_implicits : bool ref
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a7b1bb41..e6340646 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -29,13 +29,14 @@ open Nametab
open Notation
open Inductiveops
open Decl_kinds
+open Context.Rel.Declaration
(** constr_expr -> glob_constr translation:
- it adds holes for implicit arguments
- - it remplaces notations by their value (scopes stuff are here)
+ - it replaces notations by their value (scopes stuff are here)
- it recognizes global vars from local ones
- - it prepares pattern maching problems (a pattern becomes a tree where nodes
- are constructor/variable pairs and leafs are variables)
+ - it prepares pattern matching problems (a pattern becomes a tree
+ where nodes are constructor/variable pairs and leafs are variables)
All that at once, fasten your seatbelt!
*)
@@ -101,7 +102,7 @@ let global_reference id =
let construct_reference ctx id =
try
- Term.mkVar (let _ = Context.lookup_named id ctx in id)
+ Term.mkVar (let _ = Context.Named.lookup id ctx in id)
with Not_found ->
global_reference id
@@ -274,7 +275,8 @@ let error_expect_binder_notation_type loc id =
let set_var_scope loc id istermvar env ntnvars =
try
- let idscopes,typ = Id.Map.find id ntnvars in
+ let isonlybinding,idscopes,typ = Id.Map.find id ntnvars in
+ if istermvar then isonlybinding := false;
let () = if istermvar then
(* scopes have no effect on the interpretation of identifiers *)
begin match !idscopes with
@@ -298,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}
@@ -367,7 +369,7 @@ let check_hidden_implicit_parameters id impls =
errorlabstrm "" (strbrk "A parameter of an inductive type " ++
pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
-let push_name_env ?(global_level=false) lvar implargs env =
+let push_name_env ?(global_level=false) ntnvars implargs env =
function
| loc,Anonymous ->
if global_level then
@@ -375,7 +377,6 @@ let push_name_env ?(global_level=false) lvar implargs env =
env
| loc,Name id ->
check_hidden_implicit_parameters id env.impls ;
- let (_,ntnvars) = lvar in
if Id.Map.is_empty ntnvars && Id.equal id ldots_var
then error_ldots_var loc;
set_var_scope loc id false env ntnvars;
@@ -431,14 +432,72 @@ let intern_assumption intern lvar env nal bk ty =
let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
env, b
+let rec free_vars_of_pat il =
+ function
+ | CPatCstr (loc, c, l1, l2) ->
+ let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in
+ List.fold_left free_vars_of_pat il l2
+ | CPatAtom (loc, ro) ->
+ begin match ro with
+ | Some (Ident (loc, i)) -> (loc, i) :: il
+ | Some _ | None -> il
+ end
+ | CPatNotation (loc, n, l1, l2) ->
+ let il = List.fold_left free_vars_of_pat il (fst l1) in
+ List.fold_left (List.fold_left free_vars_of_pat) il (snd l1)
+ | _ -> anomaly (str "free_vars_of_pat")
+
+let intern_local_pattern intern lvar env p =
+ List.fold_left
+ (fun env (loc, i) ->
+ let bk = Default Implicit in
+ let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in
+ let n = Name i in
+ let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in
+ env)
+ env (free_vars_of_pat [] p)
+
+type binder_data =
+ | BDRawDef of (Loc.t * glob_binder)
+ | BDPattern of
+ (Loc.t * (cases_pattern * Id.t list) *
+ (bool ref *
+ (Notation_term.tmp_scope_name option *
+ Notation_term.tmp_scope_name list)
+ option ref * Notation_term.notation_var_internalization_type)
+ Names.Id.Map.t *
+ intern_env * constr_expr)
+
+let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
+
let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function
| LocalRawAssum(nal,bk,ty) ->
let env, bl' = intern_assumption intern lvar env nal bk ty in
+ let bl' = List.map (fun a -> BDRawDef a) bl' in
env, bl' @ bl
| LocalRawDef((loc,na as locna),def) ->
- let indef = intern env def in
+ let indef = intern env def in
+ let term, ty =
+ match indef with
+ | GCast (loc, b, Misctypes.CastConv t) -> b, t
+ | _ -> indef, GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)
+ in
(push_name_env lvar (impls_term_list indef) env locna,
- (loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))::bl)
+ (BDRawDef ((loc,(na,Explicit,Some(term),ty))))::bl)
+ | LocalPattern (loc,p,ty) ->
+ let tyc =
+ match ty with
+ | Some ty -> ty
+ | None -> CHole(loc,None,Misctypes.IntroAnonymous,None)
+ in
+ let env = intern_local_pattern intern lvar env p in
+ let cp =
+ match !intern_cases_pattern_fwd (None,env.scopes) p with
+ | (_, [(_, cp)]) -> cp
+ | _ -> assert false
+ in
+ let il = List.map snd (free_vars_of_pat [] p) in
+ (env, BDPattern(loc,(cp,il),lvar,env,tyc) :: bl)
let intern_generalization intern env lvar loc bk ak c =
let c = intern {env with unb = true} c in
@@ -449,12 +508,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 ->
@@ -504,44 +566,85 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
in
(renaming',env), Name id'
-let make_letins = List.fold_right (fun (loc,(na,b,t)) c -> GLetIn (loc,na,b,c))
-
-let rec subordinate_letins letins = function
+type letin_param =
+ | LPLetIn of Loc.t * (Name.t * glob_constr)
+ | LPCases of Loc.t * (cases_pattern * Id.t list) * Id.t
+
+let make_letins =
+ List.fold_right
+ (fun a c ->
+ match a with
+ | LPLetIn (loc,(na,b)) ->
+ GLetIn(loc,na,b,c)
+ | LPCases (loc,(cp,il),id) ->
+ let tt = (GVar(loc,id),(Name id,None)) in
+ GCases(loc,Misctypes.LetPatternStyle,None,[tt],[(loc,il,[cp],c)]))
+
+let rec subordinate_letins intern letins = function
(* binders come in reverse order; the non-let are returned in reverse order together *)
(* with the subordinated let-in in writing order *)
- | (loc,(na,_,Some b,t))::l ->
- subordinate_letins ((loc,(na,b,t))::letins) l
- | (loc,(na,bk,None,t))::l ->
- let letins',rest = subordinate_letins [] l in
+ | BDRawDef (loc,(na,_,Some b,t))::l ->
+ subordinate_letins intern (LPLetIn (loc,(na,b))::letins) l
+ | BDRawDef (loc,(na,bk,None,t))::l ->
+ let letins',rest = subordinate_letins intern [] l in
letins',((loc,(na,bk,t)),letins)::rest
+ | BDPattern (loc,u,lvar,env,tyc) :: l ->
+ let ienv = Id.Set.elements env.ids in
+ let id = Namegen.next_ident_away (Id.of_string "pat") ienv in
+ let na = (loc, Name id) in
+ let bk = Default Explicit in
+ let _, bl' = intern_assumption intern lvar env [na] bk tyc in
+ let bl' = List.map (fun a -> BDRawDef a) bl' in
+ subordinate_letins intern (LPCases (loc,u,id)::letins) (bl'@ l)
| [] ->
letins,[]
-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 terms_of_binders bl =
+ let rec term_of_pat = function
+ | PatVar (loc,Name id) -> CRef (Ident (loc,id), None)
+ | PatVar (loc,Anonymous) -> error "Cannot turn \"_\" into a term."
+ | PatCstr (loc,c,l,_) ->
+ let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
+ let hole = CHole (loc,None,Misctypes.IntroAnonymous,None) in
+ let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
+ CAppExpl (loc,(None,r,None),params @ List.map term_of_pat l) in
+ let rec extract_variables = function
+ | BDRawDef (loc,(Name id,_,None,_))::l -> CRef (Ident (loc,id), None) :: extract_variables l
+ | BDRawDef (loc,(Name id,_,Some _,_))::l -> extract_variables l
+ | BDRawDef (loc,(Anonymous,_,_,_))::l -> error "Cannot turn \"_\" into a term."
+ | BDPattern (loc,(u,_),lvar,env,tyc) :: l -> term_of_pat u :: extract_variables l
+ | [] -> [] in
+ extract_variables bl
+
+let instantiate_notation_constr loc intern ntnvars 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) *)
let avoid = Id.Map.domain ntnvars in
- let rec aux (terms,binderopt as subst') (renaming,env) c =
+ let rec aux (terms,binderopt,terminopt as subst') (renaming,env) c =
let subinfos = renaming,{env with tmp_scope = None} in
match c with
+ | NVar id when Id.equal id ldots_var -> Option.get terminopt
| NVar id -> subst_var subst' (renaming, env) id
- | NList (x,_,iter,terminator,lassoc) ->
- (try
+ | NList (x,y,iter,terminator,lassoc) ->
+ let l,(scopt,subscopes) =
(* All elements of the list are in scopes (scopt,subscopes) *)
- let (l,(scopt,subscopes)) = Id.Map.find x termlists in
- let termin = aux subst' subinfos terminator in
- let fold a t =
- let nterms = Id.Map.add x (a, (scopt, subscopes)) terms in
- subst_iterator ldots_var t (aux (nterms, binderopt) subinfos iter)
- in
- List.fold_right fold (if lassoc then List.rev l else l) termin
- with Not_found ->
- anomaly (Pp.str "Inconsistent substitution of recursive notation"))
+ try
+ let l,scopes = Id.Map.find x termlists in
+ (if lassoc then List.rev l else l),scopes
+ with Not_found ->
+ try
+ let (bl,(scopt,subscopes)) = Id.Map.find x binders in
+ let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
+ terms_of_binders (if lassoc then bl' else List.rev bl'),(None,[])
+ with Not_found ->
+ anomaly (Pp.str "Inconsistent substitution of recursive notation") in
+ let termin = aux (terms,None,None) subinfos terminator in
+ let fold a t =
+ let nterms = Id.Map.add y (a, (scopt, subscopes)) terms in
+ aux (nterms,None,Some t) subinfos iter
+ in
+ List.fold_right fold l termin
| NHole (knd, naming, arg) ->
let knd = match knd with
| Evar_kinds.BinderType (Name id as na) ->
@@ -576,26 +679,28 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c =
Some arg
in
GHole (loc, knd, naming, arg)
- | NBinderList (x,_,iter,terminator) ->
+ | NBinderList (x,y,iter,terminator) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (bl,(scopt,subscopes)) = Id.Map.find x binders in
- let env,bl = List.fold_left (intern_local_binder_aux intern lvar) (env,[]) bl in
- let letins,bl = subordinate_letins [] bl in
- let termin = aux subst' (renaming,env) terminator in
+ let env,bl = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in
+ let letins,bl = subordinate_letins intern [] bl in
+ let termin = aux (terms,None,None) (renaming,env) terminator in
let res = List.fold_left (fun t binder ->
- subst_iterator ldots_var t
- (aux (terms,Some(x,binder)) subinfos iter))
+ aux (terms,Some(y,binder),Some t) subinfos iter)
termin bl in
make_letins letins res
with Not_found ->
anomaly (Pp.str "Inconsistent substitution of recursive notation"))
| NProd (Name id, NHole _, c') when option_mem_assoc id binderopt ->
- let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in
- GProd (loc,na,bk,t,make_letins letins (aux subst' infos c'))
+ let a,letins = snd (Option.get binderopt) in
+ let e = make_letins letins (aux subst' infos c') in
+ let (loc,(na,bk,t)) = a in
+ GProd (loc,na,bk,t,e)
| NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
- let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in
- GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c'))
+ let a,letins = snd (Option.get binderopt) in
+ let (loc,(na,bk,t)) = a in
+ GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c'))
(* Two special cases to keep binder name synchronous with BinderType *)
| NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
when Name.equal na na' ->
@@ -610,7 +715,7 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c =
| t ->
glob_constr_of_notation_constr_with_binders loc
(traverse_binder subst avoid) (aux subst') subinfos t
- and subst_var (terms, binderopt) (renaming, env) id =
+ and subst_var (terms, _binderopt, _terminopt) (renaming, env) id =
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
try
@@ -623,12 +728,12 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c =
with Not_found ->
(* Happens for local notation joint with inductive/fixpoint defs *)
GVar (loc,id)
- in aux (terms,None) infos c
+ in aux (terms,None,None) infos c
let split_by_type ids =
List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) ->
match typ with
- | NtnTypeConstr -> ((x,scl)::l1,l2,l3)
+ | NtnTypeConstr | NtnTypeOnlyBinder -> ((x,scl)::l1,l2,l3)
| NtnTypeConstrList -> (l1,(x,scl)::l2,l3)
| NtnTypeBinderList -> (l1,l2,(x,scl)::l3)) ids ([],[],[])
@@ -644,7 +749,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
(**********************************************************************)
@@ -656,7 +761,13 @@ let string_of_ty = function
| Method -> "meth"
| Variable -> "var"
-let intern_var genv (ltacvars,ntnvars) namedctx loc id =
+let gvar (loc, id) us = match us with
+| None -> GVar (loc, id)
+| Some _ ->
+ user_err_loc (loc, "", str "Variable " ++ pr_id id ++
+ str " cannot have a universe instance")
+
+let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
(* Is [id] an inductive type potentially with implicit *)
try
let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
@@ -664,28 +775,28 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
(fun id -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
let tys = string_of_ty ty in
Dumpglob.dump_reference loc "<>" (Id.to_string id) tys;
- GVar (loc,id), make_implicits_list impls, argsc, expl_impls
+ gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
with Not_found ->
(* Is [id] bound in current term or is an ltac var bound to constr *)
if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars
then
- GVar (loc,id), [], [], []
+ gvar (loc,id) us, [], [], []
(* Is [id] a notation variable *)
else if Id.Map.mem id ntnvars
then
- (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], [])
+ (set_var_scope loc id true genv ntnvars; gvar (loc,id) us, [], [], [])
(* Is [id] the special variable for recursive notations *)
else if Id.equal id ldots_var
then if Id.Map.is_empty ntnvars
then error_ldots_var loc
- else GVar (loc,id), [], [], []
+ else gvar (loc,id) us, [], [], []
else if Id.Set.mem id ltacvars.ltac_bound then
(* Is [id] bound to a free name in ltac (this is an ltac error message) *)
user_err_loc (loc,"intern_var",
str "variable " ++ pr_id id ++ str " should be bound to a term.")
else
(* Is [id] a goal or section variable *)
- let _ = Context.lookup_named id namedctx in
+ let _ = Context.Named.lookup id namedctx in
try
(* [id] a section variable *)
(* Redundant: could be done in intern_qualid *)
@@ -693,23 +804,10 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
- GRef (loc, ref, None), impls, scopes, []
- with e when Errors.noncritical e ->
+ GRef (loc, ref, us), impls, scopes, []
+ with e when CErrors.noncritical e ->
(* [id] a goal variable *)
- GVar (loc,id), [], [], []
-
-let proj_impls r impls =
- let env = Global.env () in
- let f (x, l) = x, projection_implicits env r l in
- List.map f impls
-
-let proj_scopes n scopes =
- List.skipn_at_least n scopes
-
-let proj_impls_scopes p impls scopes =
- match p with
- | Some (r, n) -> proj_impls r impls, proj_scopes n scopes
- | None -> impls, scopes
+ gvar (loc,id) us, [], [], []
let find_appl_head_data c =
match c with
@@ -767,7 +865,18 @@ 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 _, GApp (loc, GRef (loc', ref, None), arg) ->
+ GApp (loc, GRef (loc', ref, us), arg)
+ | Some _, _ ->
+ user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++
+ str " cannot have a universe instance, its expanded head
+ does not start with a reference")
+ 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 =
@@ -775,26 +884,26 @@ let intern_non_secvar_qualid loc qid intern env lvar us args =
| GRef (_, VarRef _, _),_,_ -> raise Not_found
| r -> r
-let intern_applied_reference intern env namedctx lvar us args = function
+let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function
| Qualid (loc, qid) ->
let r,projapp,args2 =
- try intern_qualid loc qid intern env lvar us args
+ try intern_qualid loc qid intern env ntnvars us args
with Not_found -> error_global_not_found_loc loc qid
in
let x, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), args2
| Ident (loc, id) ->
- try intern_var env lvar namedctx loc id, args
+ try intern_var env lvar namedctx loc id us, args
with Not_found ->
let qid = qualid_of_ident id in
try
- let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env lvar us args in
+ let r, projapp, args2 = intern_non_secvar_qualid loc qid intern env ntnvars us args in
let x, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), args2
with Not_found ->
(* Extra allowance for non globalizing functions *)
if !interning_grammar || env.unb then
- (GVar (loc,id), [], [], []), args
+ (gvar (loc,id) us, [], [], []), args
else error_global_not_found_loc loc qid
let interp_reference vars r =
@@ -929,7 +1038,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
@@ -938,109 +1047,136 @@ 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
| Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x))
-let sort_fields mode loc l completer =
-(*mode=false if pattern and true if constructor*)
- match l with
+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
+ interning a record construction, or patterns, when intering record
+ pattern-matching). It will sort the fields according to the record
+ declaration order (which is important when type-checking them in
+ presence of dependencies between fields). If the parameter
+ [complete] is true, we require the assignment to be complete: all
+ the fields of the record must be present in the
+ assignment. Otherwise the record assignment may be partial
+ (in a pattern, we may match on some fields only), and we call the
+ function [completer] to fill the missing fields; the returned
+ field assignment list is always complete. *)
+let sort_fields ~complete loc fields completer =
+ match fields with
| [] -> None
- | (refer, value)::rem ->
- let (nparams, (* the number of parameters *)
- base_constructor, (* the reference constructor of the record *)
- (max, (* number of params *)
- (first_index, (* index of the first field of the record *)
- list_proj))) (* list of projections *)
- =
- let record =
- try Recordops.find_projection
- (global_reference_of_reference refer)
- with Not_found ->
- user_err_loc (loc_of_reference refer, "intern", pr_reference refer ++ str": Not a projection")
- in
- (* elimination of the first field from the projections *)
- let rec build_patt l m i acc =
- match l with
- | [] -> (i, acc)
- | (Some name) :: b->
- (match m with
- | [] -> anomaly (Pp.str "Number of projections mismatch")
- | (_, regular)::tm ->
- let boolean = not regular in
- begin match global_reference_of_reference refer with
- | ConstRef name' when eq_constant name name' ->
- if boolean && mode then
- user_err_loc (loc, "", str"No local fields allowed in a record construction.")
- else build_patt b tm (i + 1) (i, snd acc) (* we found it *)
- | _ ->
- build_patt b tm (if boolean&&mode then i else i + 1)
- (if boolean && mode then acc
- else fst acc, (i, ConstRef name) :: snd acc)
- end)
- | None :: b-> (* we don't want anonymous fields *)
- if mode then
- user_err_loc (loc, "", str "This record contains anonymous fields.")
- else build_patt b m (i+1) acc
- (* anonymous arguments don't appear in m *)
- in
- let ind = record.Recordops.s_CONST in
- try (* insertion of Constextern.reference_global *)
- (record.Recordops.s_EXPECTEDPARAM,
- Qualid (loc, shortest_qualid_of_global Id.Set.empty (ConstructRef ind)),
- build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[]))
- with Not_found -> anomaly (Pp.str "Environment corruption for records.")
- in
- (* now we want to have all fields of the pattern indexed by their place in
- the constructor *)
- let rec sf patts accpatt =
- match patts with
- | [] -> accpatt
- | p::q->
- let refer, patt = p in
- let glob_refer = try global_reference_of_reference refer
- with |Not_found ->
- user_err_loc (loc_of_reference refer, "intern",
- str "The field \"" ++ pr_reference refer ++ str "\" does not exist.") in
- let rec add_patt l acc =
- match l with
- | [] ->
- user_err_loc
- (loc, "",
- str "This record contains fields of different records.")
- | (i, a) :: b->
- if eq_gr glob_refer a
- then (i,List.rev_append acc l)
- else add_patt b ((i,a)::acc)
- in
- let (index, projs) = add_patt (snd accpatt) [] in
- sf q ((index, patt)::fst accpatt, projs) in
- let (unsorted_indexed_pattern, remainings) =
- sf rem ([first_index, value], list_proj) in
- (* we sort them *)
- let sorted_indexed_pattern =
- List.sort (fun (i, _) (j, _) -> compare i j) unsorted_indexed_pattern in
- (* a function to complete with wildcards *)
- let rec complete_list n l =
- if n <= 1 then l else complete_list (n-1) (completer n l) in
- (* a function to remove indice *)
- let rec clean_list l i acc =
- match l with
- | [] -> complete_list (max - i) acc
- | (k, p)::q-> clean_list q k (p::(complete_list (k - i) acc))
- in
- Some (nparams, base_constructor,
- List.rev (clean_list sorted_indexed_pattern 0 []))
+ | (first_field_ref, first_field_value):: other_fields ->
+ let (first_field_glob_ref, record) =
+ try
+ let gr = global_reference_of_reference first_field_ref in
+ (gr, Recordops.find_projection gr)
+ with Not_found ->
+ user_err_loc (loc_of_reference first_field_ref, "intern",
+ pr_reference first_field_ref ++ str": Not a projection")
+ in
+ (* the number of parameters *)
+ let nparams = record.Recordops.s_EXPECTEDPARAM in
+ (* the reference constructor of the record *)
+ let base_constructor =
+ let global_record_id = ConstructRef record.Recordops.s_CONST in
+ 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 *)
+ =
+ (* elimitate the first field from the projections,
+ but keep its index *)
+ let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc =
+ match projs with
+ | [] -> (idx, acc_first_idx, acc)
+ | (Some name) :: projs ->
+ let field_glob_ref = ConstRef name in
+ let first_field = eq_gr field_glob_ref first_field_glob_ref in
+ begin match proj_kinds with
+ | [] -> anomaly (Pp.str "Number of projections mismatch")
+ | (_, regular) :: proj_kinds ->
+ (* "regular" is false when the field is defined
+ by a let-in in the record declaration
+ (its value is fixed from other fields). *)
+ if first_field && not regular && complete then
+ user_err_loc (loc, "", str "No local fields allowed in a record construction.")
+ else if first_field then
+ build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc
+ else if not regular && complete then
+ (* skip non-regular fields *)
+ build_proj_list projs proj_kinds idx ~acc_first_idx acc
+ else
+ build_proj_list projs proj_kinds (idx+1) ~acc_first_idx
+ ((idx, field_glob_ref) :: acc)
+ end
+ | None :: projs ->
+ if complete then
+ (* we don't want anonymous fields *)
+ user_err_loc (loc, "", str "This record contains anonymous fields.")
+ else
+ (* anonymous arguments don't appear in proj_kinds *)
+ build_proj_list projs proj_kinds (idx+1) ~acc_first_idx acc
+ in
+ build_proj_list record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 ~acc_first_idx:0 []
+ in
+ (* now we want to have all fields assignments indexed by their place in
+ the constructor *)
+ let rec index_fields fields remaining_projs acc =
+ match fields with
+ | (field_ref, field_value) :: fields ->
+ let field_glob_ref = try global_reference_of_reference field_ref
+ with Not_found ->
+ user_err_loc (loc_of_reference field_ref, "intern",
+ str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
+ let remaining_projs, (field_index, _) =
+ let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in
+ try CList.extract_first the_proj remaining_projs
+ with Not_found ->
+ user_err_loc
+ (loc, "",
+ str "This record contains fields of different records.")
+ in
+ index_fields fields remaining_projs ((field_index, field_value) :: acc)
+ | [] ->
+ (* the order does not matter as we sort them next,
+ List.rev_* is just for efficiency *)
+ let remaining_fields =
+ let complete_field (idx, _field_ref) = (idx, completer idx) in
+ List.rev_map complete_field remaining_projs in
+ List.rev_append remaining_fields acc
+ in
+ let unsorted_indexed_fields =
+ index_fields other_fields proj_list
+ [(first_field_index, first_field_value)] in
+ let sorted_indexed_fields =
+ let cmp_by_index (i, _) (j, _) = Int.compare i j in
+ List.sort cmp_by_index unsorted_indexed_fields in
+ let sorted_fields = List.map snd sorted_indexed_fields in
+ Some (nparams, base_constructor, sorted_fields)
(** {6 Manage multiple aliases} *)
@@ -1068,10 +1204,6 @@ let alias_of als = match als.alias_ids with
| [] -> Anonymous
| id :: _ -> Name id
-let message_redundant_alias id1 id2 =
- msg_warning
- (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2)
-
(** {6 Expanding notations }
@returns a raw_case_pattern_expr :
@@ -1102,98 +1234,103 @@ 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
+ sort_fields ~complete:false loc l (fun _idx -> (CPatAtom (loc, None))) in
begin match sorted_fields with
| 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)
+ | CPatCast _ ->
+ assert false
+ 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
@@ -1201,8 +1338,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)
@@ -1210,23 +1346,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)
- | NList (x,_,iter,terminator,lassoc) ->
+ List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
+ List.map (in_pat false scopes) args, [])
+ | NList (x,y,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 nsubst = Id.Map.add y (a, (scopt, subscopes)) subst 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 ->
@@ -1249,7 +1385,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 =
@@ -1274,29 +1410,65 @@ 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 =
+(* [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) env pat)
+ (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
-let intern_ind_pattern genv env pat =
+let _ =
+ intern_cases_pattern_fwd :=
+ 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) 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)
(**********************************************************************)
@@ -1362,7 +1534,7 @@ let extract_explicit_arg imps args =
(**********************************************************************)
(* Main loop *)
-let internalize globalenv env allow_patvar lvar c =
+let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let rec intern env = function
| CRef (ref,us) as x ->
let (c,imp,subscopes,l),_ =
@@ -1383,10 +1555,11 @@ let internalize globalenv env allow_patvar lvar c =
(fun (id,(n,order),bl,ty,_) ->
let intern_ro_arg f =
let before, after = split_at_annot bl n in
- let (env',rbefore) =
- List.fold_left intern_local_binder (env,[]) before in
+ let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
+ let rbefore = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbefore in
let ro = f (intern env') in
- let n' = Option.map (fun _ -> List.length (List.filter (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore)) n in
+ let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in
+ let rbefore = List.map (fun a -> BDRawDef a) rbefore in
n', ro, List.fold_left intern_local_binder (env',rbefore) after
in
let n, ro, (env',rbl) =
@@ -1398,12 +1571,18 @@ let internalize globalenv env allow_patvar lvar c =
| CMeasureRec (m,r) ->
intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
in
- ((n, ro), List.rev rbl, intern_type env' ty, env')) dl in
+ let bl =
+ List.rev_map
+ (function
+ | BDRawDef a -> a
+ | BDPattern (loc,_,_,_,_) ->
+ Loc.raise loc (Stream.Error "pattern with quote not allowed after fix")) rbl in
+ ((n, ro), bl, intern_type env' ty, env')) dl in
let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
let env'' = List.fold_left_i (fun i en name ->
let (_,bli,tyi,_) = idl_temp.(i) in
let fix_args = (List.map (fun (_,(na, bk, _, _)) -> (build_impls bk na)) bli) in
- push_name_env lvar (impls_type_list ~args:fix_args tyi)
+ push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
en (Loc.ghost, Name name)) 0 env' lf in
(a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
GRec (loc,GFix
@@ -1422,15 +1601,15 @@ let internalize globalenv env allow_patvar lvar c =
in
let idl_tmp = Array.map
(fun ((loc,id),bl,ty,_) ->
- let (env',rbl) =
- List.fold_left intern_local_binder (env,[]) bl in
+ 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
(List.rev rbl,
intern_type env' ty,env')) dl in
let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') ->
let env'' = List.fold_left_i (fun i en name ->
let (bli,tyi,_) = idl_tmp.(i) in
let cofix_args = List.map (fun (_, (na, bk, _, _)) -> (build_impls bk na)) bli in
- push_name_env lvar (impls_type_list ~args:cofix_args tyi)
+ push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
en (Loc.ghost, Name name)) 0 env' lf in
(b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
GRec (loc,GCoFix n,
@@ -1449,15 +1628,15 @@ let internalize globalenv env allow_patvar lvar c =
| CLetIn (loc,na,c1,c2) ->
let inc1 = intern (reset_tmp_scope env) c1 in
GLetIn (loc, snd na, inc1,
- intern (push_name_env lvar (impls_term_list inc1) env na) c2)
+ intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
| CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[]))
when Bigint.is_strictly_pos p ->
intern env (CPrim (loc,Numeral (Bigint.neg p)))
| CNotation (_,"( _ )",([a],[],[])) -> intern env a
| CNotation (loc,ntn,args) ->
- intern_notation intern env lvar loc ntn args
+ intern_notation intern env ntnvars loc ntn args
| CGeneralization (loc,b,a,c) ->
- intern_generalization intern env lvar loc b a c
+ intern_generalization intern env ntnvars loc b a c
| CPrim (loc, p) ->
fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes))
| CDelimiters (loc, key, e) ->
@@ -1485,20 +1664,22 @@ let internalize globalenv env allow_patvar lvar c =
intern_applied_reference intern env
(Environ.named_context globalenv) lvar us args ref
| CNotation (loc,ntn,([],[],[])) ->
- let c = intern_notation intern env lvar loc ntn ([],[],[]) in
+ let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in
let x, impl, scopes, l = find_appl_head_data c in
(x,impl,scopes,l), args
| x -> (intern env f,[],[],[]), args in
apply_impargs c env impargs args_scopes
(merge_impargs l args) loc
- | CRecord (loc, _, fs) ->
- let cargs =
- sort_fields true loc fs
- (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l)
- in
- begin
- match cargs with
+ | CRecord (loc, fs) ->
+ let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
+ let fields =
+ sort_fields ~complete:true loc fs
+ (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark st),
+ Misctypes.IntroAnonymous, None))
+ in
+ begin
+ match fields with
| None -> user_err_loc (loc, "intern", str"No constructor inference.")
| Some (n, constrname, args) ->
let pars = List.make n (CHole (loc, None, Misctypes.IntroAnonymous, None)) in
@@ -1506,60 +1687,70 @@ 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 ntnvars (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')
| CLetTuple (loc, nal, (na,po), b, c) ->
let env' = reset_tmp_scope env in
(* "in" is None so no match to add *)
- let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,(na,None)) in
+ let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
let p' = Option.map (fun u ->
- let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
+ let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
(Loc.ghost,na') in
intern_type env'' u) po in
GLetTuple (loc, List.map snd nal, (na', p'), b',
- intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
+ intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
| CIf (loc, c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
- let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,(na,None)) in (* no "in" no match to ad too *)
+ let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
let p' = Option.map (fun p ->
- let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
+ let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
(Loc.ghost,na') in
intern_type env'' p) po in
GIf (loc, c', (na', p'), intern env b1, intern env b2)
| CHole (loc, k, naming, solve) ->
let k = match k with
- | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true)
+ | None ->
+ let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
+ Evar_kinds.QuestionMark st
| Some k -> k
in
let solve = match solve with
@@ -1598,12 +1789,11 @@ let internalize globalenv env allow_patvar lvar c =
and intern_type env = intern (set_type_scope env)
and intern_local_binder env bind =
- intern_local_binder_aux intern lvar env bind
+ intern_local_binder_aux intern ntnvars env bind
(* 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
@@ -1624,12 +1814,11 @@ let internalize globalenv env allow_patvar lvar c =
let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in
List.map (fun (asubst,pl) ->
let rhs = replace_vars_constr_expr asubst rhs in
- Id.Map.iter message_redundant_alias asubst;
let rhs' = intern {env with ids = env_ids} rhs in
(loc,eqn_ids,pl,rhs')) pll
- and intern_case_item env forbidden_names_for_gen (tm,(na,t)) =
- (*the "match" part *)
+ and intern_case_item env forbidden_names_for_gen (tm,na,t) =
+ (* the "match" part *)
let tm' = intern env tm in
(* the "as" part *)
let extra_id,na = match tm', na with
@@ -1640,9 +1829,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")])
@@ -1654,23 +1841,23 @@ 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 *)
- |(_,Some _,_)::t, l when not with_letin ->
+ | 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)
- |(cano_name,_,ty)::t,c::tt ->
+ | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
let fresh =
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
@@ -1680,11 +1867,11 @@ let internalize globalenv env allow_patvar lvar c =
(tm',(snd na,typ)), extra_id, match_td
and iterate_prod loc2 env bk ty body nal =
- let env, bl = intern_assumption intern lvar env nal bk ty in
+ let env, bl = intern_assumption intern ntnvars env nal bk ty in
it_mkGProd loc2 bl (intern_type env body)
and iterate_lam loc2 env bk ty body nal =
- let env, bl = intern_assumption intern lvar env nal bk ty in
+ let env, bl = intern_assumption intern ntnvars env nal bk ty in
it_mkGLambda loc2 bl (intern env body)
and intern_impargs c env l subscopes args =
@@ -1726,7 +1913,7 @@ let internalize globalenv env allow_patvar lvar c =
in aux 1 l subscopes eargs rargs
and apply_impargs c env imp subscopes l loc =
- let imp = select_impargs_size (List.length l) imp in
+ let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in
let l = intern_impargs c env imp subscopes l in
smart_gapp c loc l
@@ -1760,7 +1947,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
@@ -1784,9 +1971,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)
@@ -1857,18 +2042,19 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
let env = Global.env () in
(* [vl] is intended to remember the scope of the free variables of [a] *)
- let vl = Id.Map.map (fun typ -> (ref None, typ)) nenv.ninterp_var_type in
+ let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in
let c = internalize (Global.env()) {ids = extract_ids env; unb = false;
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 (sc, typ) -> (out_scope !sc, typ)) vl 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 *)
@@ -1891,7 +2077,16 @@ let intern_context global_level env impl_env binders =
try
let lvar = (empty_ltac_sign, Id.Map.empty) in
let lenv, bl = List.fold_left
- (intern_local_binder_aux ~global_level (my_intern_constr env lvar) lvar)
+ (fun (lenv, bl) b ->
+ let bl = List.map (fun a -> BDRawDef a) bl in
+ let (env, bl) = intern_local_binder_aux ~global_level (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
+ let bl =
+ List.map
+ (function
+ | BDRawDef a -> a
+ | BDPattern (loc,_,_,_,_) ->
+ Loc.raise loc (Stream.Error "pattern with quote not allowed here")) bl in
+ (env, bl))
({ids = extract_ids env; unb = false;
tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
(lenv.impls, List.map snd bl)
@@ -1902,12 +2097,14 @@ let interp_rawcontext_evars env evdref k bl =
let (env, par, _, impls) =
List.fold_left
(fun (env,params,n,impls) (na, k, b, t) ->
+ let t' =
+ if Option.is_empty b then locate_if_hole (loc_of_glob_constr t) na t
+ else t
+ in
+ let t = understand_tcc_evars env evdref ~expected_type:IsType t' in
match b with
None ->
- let t' = locate_if_hole (loc_of_glob_constr t) na t in
- let t =
- understand_tcc_evars env evdref ~expected_type:IsType t' in
- let d = (na,None,t) in
+ let d = LocalAssum (na,t) in
let impls =
if k == Implicit then
let na = match na with Name n -> Some n | Anonymous -> None in
@@ -1916,8 +2113,8 @@ let interp_rawcontext_evars env evdref k bl =
in
(push_rel d env, d::params, succ n, impls)
| Some b ->
- let c = understand_judgment_tcc env evdref b in
- let d = (na, Some c.uj_val, c.uj_type) in
+ let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in
+ let d = LocalDef (na, c, t) in
(push_rel d env, d::params, n, impls))
(env,[],k+1,[]) (List.rev bl)
in (env, par), impls
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 22cf910b..61e7c6f5 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Evd
open Environ
open Libnames
@@ -161,7 +160,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
val interp_context_evars :
?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
env -> evar_map ref -> local_binder list ->
- internalization_env * ((env * rel_context) * Impargs.manual_implicits)
+ internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits)
(* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
(* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
@@ -178,7 +177,7 @@ val interp_context_evars :
val locate_reference : Libnames.qualid -> Globnames.global_reference
val is_global : Id.t -> bool
-val construct_reference : named_context -> Id.t -> constr
+val construct_reference : Context.Named.t -> Id.t -> constr
val global_reference : Id.t -> constr
val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
@@ -186,8 +185,8 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr
guaranteed to have the same domain as the input one. *)
val interp_notation_constr : ?impls:internalization_env ->
notation_interp_env -> constr_expr ->
- (subscopes * notation_var_internalization_type) Id.Map.t *
- notation_constr
+ (bool * subscopes * notation_var_internalization_type) Id.Map.t *
+ notation_constr * reversibility_flag
(** Globalization options *)
val parsing_explicit : bool ref
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 9e517381..588637b7 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Names
@@ -87,7 +87,7 @@ let check_required_library d =
*)
(* or failing ...*)
errorlabstrm "Coqlib.check_required_library"
- (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.")
+ (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
(************************************************************************)
(* Specific Coq objects *)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 0d9d021c..b020f894 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -45,10 +45,10 @@ let dump_string s =
if dump () && !glob_output != Feedback then
Pervasives.output_string !glob_file s
-let start_dump_glob vfile =
+let start_dump_glob ~vfile ~vofile =
match !glob_output with
| MultFiles ->
- open_glob_file (Filename.chop_extension vfile ^ ".glob");
+ open_glob_file (Filename.chop_extension vofile ^ ".glob");
output_string !glob_file "DIGEST ";
output_string !glob_file (Digest.to_hex (Digest.file vfile));
output_char !glob_file '\n'
@@ -127,9 +127,10 @@ let type_of_global_ref gr =
| Globnames.ConstructRef _ -> "constr"
let remove_sections dir =
- if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
+ let cwd = Lib.cwd_except_section () in
+ if Libnames.is_dirpath_prefix_of cwd dir then
(* Not yet (fully) discharged *)
- Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
+ cwd
else
(* Theorem/Lemma outside its outer section of definition *)
dir
@@ -141,7 +142,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 +173,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 +241,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)
@@ -248,7 +249,7 @@ let dump_def ty loc secpath id =
let dump_definition (loc, id) sec s =
dump_def s loc (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
-let dump_constraint ((loc, n), _, _) sec ty =
+let dump_constraint (((loc, n),_), _, _) sec ty =
match n with
| Names.Name id -> dump_definition (loc, id) sec ty
| Names.Anonymous -> ()
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index a7c79911..e84a6405 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -9,7 +9,7 @@
val open_glob_file : string -> unit
val close_glob_file : unit -> unit
-val start_dump_glob : string -> unit
+val start_dump_glob : vfile:string -> vofile:string -> unit
val end_dump_glob : unit -> unit
val dump : unit -> bool
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 47b71735..d6bfd347 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -37,20 +37,16 @@ module Subst = Register (SubstObj)
let intern = Intern.obj
let register_intern0 = Intern.register0
-let generic_intern ist v =
- let unpacker wit v =
- let (ist, v) = intern wit ist (raw v) in
- (ist, in_gen (glbwit wit) v)
- in
- unpack { unpacker; } v
+let generic_intern ist (GenArg (Rawwit wit, v)) =
+ let (ist, v) = intern wit ist v in
+ (ist, in_gen (glbwit wit) v)
(** Substitution functions *)
let substitute = Subst.obj
let register_subst0 = Subst.register0
-let generic_substitute subs v =
- let unpacker wit v = in_gen (glbwit wit) (substitute wit subs (glb v)) in
- unpack { unpacker; } v
+let generic_substitute subs (GenArg (Glbwit wit, v)) =
+ in_gen (glbwit wit) (substitute wit subs v)
let () = Hook.set Detyping.subst_genarg_hook generic_substitute
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 391c600e..10cfbe58 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -9,7 +9,7 @@
(*i*)
open Names
open Decl_kinds
-open Errors
+open CErrors
open Util
open Glob_term
open Constrexpr
@@ -20,6 +20,7 @@ open Pp
open Libobject
open Nameops
open Misctypes
+open Context.Rel.Declaration
(*i*)
let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"
@@ -111,6 +112,7 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) =
let l' = free_vars_of_constr_expr c ~bound:bdvars l in
aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
+ | LocalPattern _ :: tl -> assert false
| [] -> bdvars, l
in aux bound l binders
@@ -196,7 +198,7 @@ let combine_params avoid fn applied needed =
List.partition
(function
(t, Some (loc, ExplByName id)) ->
- let is_id (_, (na, _, _)) = match na with
+ let is_id (_, decl) = match get_name decl with
| Name id' -> Id.equal id id'
| Anonymous -> false
in
@@ -209,22 +211,22 @@ let combine_params avoid fn applied needed =
(fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false)
named
in
- let is_unset (_, (_, b, _)) = match b with
- | None -> true
- | Some _ -> false
+ let is_unset (_, decl) = match decl with
+ | LocalAssum _ -> true
+ | LocalDef _ -> false
in
let needed = List.filter is_unset needed in
let rec aux ids avoid app need =
match app, need with
[], [] -> List.rev ids, avoid
- | app, (_, (Name id, _, _)) :: need when Id.List.mem_assoc id named ->
+ | app, (_, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need when Id.List.mem_assoc id named ->
aux (Id.List.assoc id named :: ids) avoid app need
- | (x, None) :: app, (None, (Name id, _, _)) :: need ->
+ | (x, None) :: app, (None, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need ->
aux (x :: ids) avoid app need
- | _, (Some cl, (_, _, _) as d) :: need ->
+ | _, (Some cl, _ as d) :: need ->
let t', avoid' = fn avoid d in
aux (t' :: ids) avoid' app need
@@ -239,8 +241,8 @@ let combine_params avoid fn applied needed =
in aux [] avoid applied needed
let combine_params_freevar =
- fun avoid (_, (na, _, _)) ->
- let id' = next_name_away_from na avoid in
+ fun avoid (_, decl) ->
+ let id' = next_name_away_from (get_name decl) avoid in
(CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid)
let destClassApp cl =
@@ -309,7 +311,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/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index b226bfa0..d0327e50 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -38,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
val combine_params_freevar :
- Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) ->
+ Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t ->
Constrexpr.constr_expr * Id.Set.t
val implicit_application : Id.Set.t -> ?allow_partial:bool ->
- (Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) ->
+ (Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t ->
Constrexpr.constr_expr * Id.Set.t) ->
constr_expr -> constr_expr * Id.Set.t
diff --git a/interp/notation.ml b/interp/notation.ml
index 5c10e0af..389a1c9d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -7,13 +7,12 @@
(************************************************************************)
(*i*)
-open Errors
+open CErrors
open Util
open Pp
open Bigint
open Names
open Term
-open Nametab
open Libnames
open Globnames
open Constrexpr
@@ -45,8 +44,14 @@ type level = precedence * tolerability list
type delimiters = string
type notation_location = (DirPath.t * DirPath.t) * string
+type notation_data = {
+ not_interp : interpretation;
+ not_location : notation_location;
+ not_onlyprinting : bool;
+}
+
type scope = {
- notations: (interpretation * notation_location) String.Map.t;
+ notations: notation_data String.Map.t;
delimiters: delimiters option
}
@@ -65,11 +70,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 +190,8 @@ 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
+ (** 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
end;
@@ -195,7 +199,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);
+ Flags.if_verbose Feedback.msg_info (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 +208,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 -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
| Some key ->
scope_map := String.Map.add scope newsc !scope_map;
try
@@ -314,7 +318,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 +332,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 ()
@@ -381,17 +387,28 @@ let level_of_notation ntn =
(* The mapping between notations and their interpretation *)
-let declare_notation_interpretation ntn scopt pat df =
+let warn_notation_overridden =
+ CWarnings.create ~name:"notation-overridden" ~category:"parsing"
+ (fun (ntn,which_scope) ->
+ str "Notation" ++ spc () ++ str ntn ++ spc ()
+ ++ strbrk "was already used" ++ which_scope)
+
+let declare_notation_interpretation ntn scopt pat df ~onlyprint =
let scope = match scopt with Some s -> s | None -> default_scope in
let sc = find_scope scope in
let () =
if String.Map.mem ntn sc.notations then
let which_scope = match scopt with
| None -> mt ()
- | Some _ -> str " in scope " ++ str scope in
- msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
+ | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in
+ warn_notation_overridden (ntn,which_scope)
in
- let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in
+ let notdata = {
+ not_interp = pat;
+ not_location = df;
+ not_onlyprinting = onlyprint;
+ } in
+ let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in
let () = scope_map := String.Map.add scope sc !scope_map in
begin match scopt with
| None -> scope_stack := SingleNotation ntn :: !scope_stack
@@ -416,7 +433,9 @@ let rec find_interpretation ntn find = function
find_interpretation ntn find scopes
let find_notation ntn sc =
- String.Map.find ntn (find_scope sc).notations
+ let n = String.Map.find ntn (find_scope sc).notations in
+ let () = if n.not_onlyprinting then raise Not_found in
+ (n.not_interp, n.not_location)
let notation_of_prim_token = function
| Numeral n when is_pos_or_zero n -> to_string n
@@ -529,26 +548,25 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
let ntpe_eq t1 t2 = match t1, t2 with
| NtnTypeConstr, NtnTypeConstr -> true
+| NtnTypeOnlyBinder, NtnTypeOnlyBinder -> true
| NtnTypeConstrList, NtnTypeConstrList -> true
| NtnTypeBinderList, NtnTypeBinderList -> true
-| (NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList), _ -> false
+| (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false
-
-let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) =
- Id.equal id1 id2 &&
+let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) =
pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
ntpe_eq tp1 tp2
let interpretation_eq (vars1, t1) (vars2, t2) =
- List.equal vars_eq vars1 vars2 &&
- Notation_ops.eq_notation_constr t1 t2
+ List.equal var_attributes_eq vars1 vars2 &&
+ Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
let exists_notation_in_scope scopt ntn r =
let scope = match scopt with Some s -> s | None -> default_scope in
try
let sc = String.Map.find scope !scope_map in
- let (r',_) = String.Map.find ntn sc.notations in
- interpretation_eq r' r
+ let n = String.Map.find ntn sc.notations in
+ interpretation_eq n.not_interp r
with Not_found -> false
let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
@@ -556,23 +574,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
@@ -583,7 +594,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
@@ -617,8 +628,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
@@ -642,7 +656,7 @@ type arguments_scope_discharge_request =
| ArgsScopeManual
| ArgsScopeNoDischarge
-let load_arguments_scope _ (_,(_,r,scl,cls)) =
+let load_arguments_scope _ (_,(_,r,n,scl,cls)) =
List.iter (Option.iter check_scope) scl;
let initial_stamp = ScopeClassMap.empty in
arguments_scope := Refmap.add r (scl,cls,initial_stamp) !arguments_scope
@@ -650,14 +664,10 @@ 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 subst_arguments_scope (subst,(req,r,n,scl,cls)) =
let r' = fst (subst_global subst r) in
let subst_cl ocl = match ocl with
| None -> ocl
@@ -666,34 +676,42 @@ let subst_arguments_scope (subst,(req,r,scl,cls)) =
| Some cl' as ocl' when cl' != cl -> ocl'
| _ -> ocl in
let cls' = List.smartmap subst_cl cls in
- (ArgsScopeNoDischarge,r',scl,cls')
+ (ArgsScopeNoDischarge,r',n,scl,cls')
-let discharge_arguments_scope (_,(req,r,l,_)) =
+let discharge_arguments_scope (_,(req,r,n,l,_)) =
if req == ArgsScopeNoDischarge || (isVarRef r && Lib.is_in_section r) then None
- else Some (req,Lib.discharge_global r,l,[])
+ else
+ let n =
+ try
+ let vars = Lib.variable_section_segment_of_reference r in
+ List.length (List.filter (fun (_,_,b,_) -> b = None) vars)
+ with
+ Not_found (* Not a ref defined in this section *) -> 0 in
+ Some (req,Lib.discharge_global r,n,l,[])
-let classify_arguments_scope (req,_,_,_ as obj) =
+let classify_arguments_scope (req,_,_,_,_ as obj) =
if req == ArgsScopeNoDischarge then Dispose else Substitute obj
-let rebuild_arguments_scope (req,r,l,_) =
+let rebuild_arguments_scope (req,r,n,l,_) =
match req with
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
let scs,cls = compute_arguments_scope_full (fst(Universes.type_of_global r)(*FIXME?*)) in
- (req,r,scs,cls)
+ (req,r,List.length scs,scs,cls)
| ArgsScopeManual ->
(* Add to the manually given scopes the one found automatically
for the extra parameters of the section. Discard the classes
of the manually given scopes to avoid further re-computations. *)
- let l',cls = compute_arguments_scope_full (Global.type_of_global_unsafe r) in
- let nparams = List.length l' - List.length l in
- let l1 = List.firstn nparams l' in
- let cls1 = List.firstn nparams cls in
- (req,r,l1@l,cls1)
+ let l',cls = compute_arguments_scope_full (Global.type_of_global_unsafe r) in
+ let l1 = List.firstn n l' in
+ let cls1 = List.firstn n cls in
+ (req,r,0,l1@l,cls1)
type arguments_scope_obj =
arguments_scope_discharge_request * global_reference *
- scope_name option list * scope_class option list
+ (* Used to communicate information from discharge to rebuild *)
+ (* set to 0 otherwise *) int *
+ scope_name option list * scope_class option list
let inArgumentsScope : arguments_scope_obj -> obj =
declare_object {(default_object "ARGUMENTS-SCOPE") with
@@ -706,16 +724,15 @@ let inArgumentsScope : arguments_scope_obj -> obj =
let is_local local ref = local || isVarRef ref && Lib.is_in_section ref
-let declare_arguments_scope_gen req r (scl,cls) =
- Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl,cls))
+let declare_arguments_scope_gen req r n (scl,cls) =
+ Lib.add_anonymous_leaf (inArgumentsScope (req,r,n,scl,cls))
let declare_arguments_scope local r scl =
- let req = if is_local local r then ArgsScopeNoDischarge else ArgsScopeManual
- in
- (* We empty the list of argument classes to disable futher scope
+ let req = if is_local local r then ArgsScopeNoDischarge else ArgsScopeManual in
+ (* We empty the list of argument classes to disable further scope
re-computations and keep these manually given scopes. *)
- declare_arguments_scope_gen req r (scl,[])
-
+ declare_arguments_scope_gen req r 0 (scl,[])
+
let find_arguments_scope r =
try
let (scl,cls,stamp) = Refmap.find r !arguments_scope in
@@ -730,7 +747,8 @@ let find_arguments_scope r =
let declare_ref_arguments_scope ref =
let t = Global.type_of_global_unsafe ref in
- declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope_full t)
+ let (scs,cls as o) = compute_arguments_scope_full t in
+ declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
(********************************)
@@ -788,9 +806,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
@@ -815,7 +831,7 @@ let pr_named_scope prglob scope sc =
++ fnl ()
++ pr_scope_classes scope
++ String.Map.fold
- (fun ntn ((_,r),(_,df)) strm ->
+ (fun ntn { not_interp = (_, r); not_location = (_, df) } strm ->
pr_notation_info prglob df r ++ fnl () ++ strm)
sc.notations (mt ())
@@ -859,7 +875,7 @@ let browse_notation strict ntn map =
let l =
String.Map.fold
(fun scope_name sc ->
- String.Map.fold (fun ntn ((_,r),df) l ->
+ String.Map.fold (fun ntn { not_interp = (_, r); not_location = df } l ->
if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
map [] in
List.sort (fun x y -> String.compare (fst x) (fst y)) l
@@ -925,7 +941,7 @@ let locate_notation prglob ntn scope =
let collect_notation_in_scope scope sc known =
assert (not (String.equal scope default_scope));
String.Map.fold
- (fun ntn ((_,r),(_,df)) (l,known as acc) ->
+ (fun ntn { not_interp = (_, r); not_location = (_, df) } (l,known as acc) ->
if String.List.mem ntn known then acc else ((df,r)::l,ntn::known))
sc.notations ([],known)
@@ -941,7 +957,7 @@ let collect_notations stack =
| SingleNotation ntn ->
if String.List.mem ntn knownntn then (all,knownntn)
else
- let ((_,r),(_,df)) =
+ let { not_interp = (_, r); not_location = (_, df) } =
String.Map.find ntn (find_scope default_scope).notations in
let all' = match all with
| (s,lonelyntn)::rest when String.equal s default_scope ->
@@ -977,23 +993,30 @@ let pr_visibility prglob = function
type unparsing_rule = unparsing list * precedence
type extra_unparsing_rules = (string * string) list
(* Concrete syntax for symbolic-extension table *)
-let printing_rules =
- ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules) String.Map.t)
+let notation_rules =
+ ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
-let declare_notation_printing_rule ntn ~extra unpl =
- printing_rules := String.Map.add ntn (unpl,extra) !printing_rules
+let declare_notation_rule ntn ~extra unpl gram =
+ notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
let find_notation_printing_rule ntn =
- try fst (String.Map.find ntn !printing_rules)
+ try pi1 (String.Map.find ntn !notation_rules)
with Not_found -> anomaly (str "No printing rule found for " ++ str ntn)
let find_notation_extra_printing_rules ntn =
- try snd (String.Map.find ntn !printing_rules)
+ try pi2 (String.Map.find ntn !notation_rules)
with Not_found -> []
+let find_notation_parsing_rules ntn =
+ try pi3 (String.Map.find ntn !notation_rules)
+ with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn)
+
+let get_defined_notations () =
+ String.Set.elements @@ String.Map.domain !notation_rules
+
let add_notation_extra_printing_rule ntn k v =
try
- printing_rules :=
- let p, pp = String.Map.find ntn !printing_rules in
- String.Map.add ntn (p, (k,v) :: pp) !printing_rules
+ notation_rules :=
+ let p, pp, gr = String.Map.find ntn !notation_rules in
+ String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
with Not_found ->
user_err_loc (Loc.ghost,"add_notation_extra_printing_rule",
str "No such Notation.")
@@ -1003,7 +1026,7 @@ let add_notation_extra_printing_rule ntn k v =
let freeze _ =
(!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
- !delimiters_map, !notations_key_table, !printing_rules,
+ !delimiters_map, !notations_key_table, !notation_rules,
!scope_class_map)
let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
@@ -1013,7 +1036,7 @@ let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
delimiters_map := dlm;
arguments_scope := asc;
notations_key_table := fkm;
- printing_rules := pprules;
+ notation_rules := pprules;
scope_class_map := clsc
let init () =
@@ -1021,7 +1044,7 @@ let init () =
notation_level_map := String.Map.empty;
delimiters_map := String.Map.empty;
notations_key_table := KeyMap.empty;
- printing_rules := String.Map.empty;
+ notation_rules := String.Map.empty;
scope_class_map := initial_scope_class_map
let _ =
@@ -1034,6 +1057,6 @@ let with_notation_protection f x =
let fs = freeze false in
try let a = f x in unfreeze fs; a
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = unfreeze fs in
iraise reraise
diff --git a/interp/notation.mli b/interp/notation.mli
index 7885814c..2e92a00a 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
@@ -110,7 +109,7 @@ type interp_rule =
| SynDefRule of kernel_name
val declare_notation_interpretation : notation -> scope_name option ->
- interpretation -> notation_location -> unit
+ interpretation -> notation_location -> onlyprint:bool -> unit
val declare_uninterpretation : interp_rule -> interpretation -> unit
@@ -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 *)
@@ -191,12 +196,16 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd
(** Declare and look for the printing rule for symbolic notations *)
type unparsing_rule = unparsing list * precedence
type extra_unparsing_rules = (string * string) list
-val declare_notation_printing_rule :
- notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
+val declare_notation_rule :
+ notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
val find_notation_printing_rule : notation -> unparsing_rule
val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
+val find_notation_parsing_rules : notation -> notation_grammar
val add_notation_extra_printing_rule : notation -> string -> string -> unit
+(** Returns notations with defined parsing/printing rules *)
+val get_defined_notations : unit -> notation list
+
(** Rem: printing rules for primitive token are canonical *)
val with_notation_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 51dfadac..0c5393cf 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -7,23 +7,111 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
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 (vars1,vars2 as vars) t1 t2 = match t1, t2 with
+| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2)
+| NApp (t1, a1), NApp (t2, a2) ->
+ (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) 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 vars) t1 t2 &&
+ (eq_notation_constr vars) u1 u2 && b1 == b2
+| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
+ Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
+| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
+ Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
+| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
+ Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
+ (eq_notation_constr vars) u1 u2
+| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) ->
+ Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) 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 vars) 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 vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
+ in
+ Option.equal (eq_notation_constr vars) 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 vars) o1 o2 &&
+ (eq_notation_constr vars) t1 t2 &&
+ (eq_notation_constr vars) u1 u2
+| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
+ (eq_notation_constr vars) t1 t2 &&
+ Name.equal na1 na2 &&
+ 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? *)
+ let eq (na1, o1, t1) (na2, o2, t2) =
+ Name.equal na1 na2 &&
+ Option.equal (eq_notation_constr vars) o1 o2 &&
+ (eq_notation_constr vars) t1 t2
+ in
+ Array.equal Id.equal ids1 ids2 &&
+ Array.equal (List.equal eq) ts1 ts2 &&
+ Array.equal (eq_notation_constr vars) us1 us2 &&
+ Array.equal (eq_notation_constr vars) rs1 rs2
+| NSort s1, NSort s2 ->
+ Miscops.glob_sort_eq s1 s2
+| NCast (t1, c1), NCast (t2, c2) ->
+ (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) 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."
+ | Anonymous -> CErrors.error "This expression should be a simple identifier."
| Name id -> id
let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
@@ -36,6 +124,14 @@ let rec cases_pattern_fold_map loc g e = function
let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in
e', PatCstr (loc,cstr,patl',na')
+let subst_binder_type_vars l = function
+ | Evar_kinds.BinderType (Name id) ->
+ let id =
+ try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
+ with Not_found -> id in
+ Evar_kinds.BinderType (Name id)
+ | e -> e
+
let rec subst_glob_vars l = function
| GVar (_,id) as r -> (try Id.List.assoc id l with Not_found -> r)
| GProd (loc,Name id,bk,t,c) ->
@@ -48,6 +144,7 @@ let rec subst_glob_vars l = function
try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
with Not_found -> id in
GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
+ | GHole (loc,x,naming,arg) -> GHole (loc,subst_binder_type_vars l x,naming,arg)
| r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *)
let ldots_var = Id.of_string ".."
@@ -105,7 +202,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 +209,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 +239,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 ->
@@ -240,7 +246,13 @@ let check_is_hole id = function GHole _ -> () | t ->
strbrk "In recursive notation with binders, " ++ pr_id id ++
strbrk " is expected to come without type.")
-let compare_recursive_parts found f (iterator,subc) =
+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
let rec aux c1 c2 = match c1,c2 with
@@ -261,18 +273,16 @@ let compare_recursive_parts found 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
@@ -286,29 +296,42 @@ let compare_recursive_parts found 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) ->
- let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in
+ | 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)
+ then
+ !found,x,y,lassoc
+ else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) ||
+ List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found)
+ then
+ !found,y,x,not lassoc
+ else
+ (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in
let iterator =
- f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator
- else iterator) in
+ f' (if lassoc then iterator
+ else subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in
(* 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 iterator 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 *)
- try compare_recursive_parts found aux' (split_at_recursive_part c)
+ try compare_recursive_parts found aux aux' (split_at_recursive_part c)
with Not_found ->
found := keepfound;
match c with
@@ -350,20 +373,20 @@ 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
- | GPatVar (_,(_,n)) -> NPatVar n
- | GEvar _ ->
+ | GEvar _ | GPatVar _ ->
error "Existential variables not allowed in notations."
in
let t = aux a in
(* Side effect *)
- t, !found
+ t, !found, !has_ltac
-let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
-
-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
@@ -386,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
@@ -406,13 +429,15 @@ 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 *)
let notation_constr_of_constr avoiding t =
@@ -420,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
@@ -438,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
@@ -526,7 +550,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 +572,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 ->
@@ -567,6 +592,18 @@ let abstract_return_type_context_notation_constr =
abstract_return_type_context snd
(fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c))
+let is_term_meta id metas =
+ try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
+ with Not_found -> false
+
+let is_onlybinding_meta id metas =
+ try match Id.List.assoc id metas with _,NtnTypeOnlyBinder -> true | _ -> false
+ with Not_found -> false
+
+let is_bindinglist_meta id metas =
+ try match Id.List.assoc id metas with _,NtnTypeBinderList -> true | _ -> false
+ with Not_found -> false
+
exception No_match
let rec alpha_var id1 id2 = function
@@ -575,26 +612,231 @@ let rec alpha_var id1 id2 = function
| _::idl -> alpha_var id1 id2 idl
| [] -> Id.equal id1 id2
-let add_env alp (sigma,sigmalist,sigmabinders) var v =
+let alpha_rename alpmetas v =
+ if alpmetas == [] then v
+ else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match
+
+let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v =
(* Check that no capture of binding variables occur *)
- if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match;
+ (* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..."
+ with an actual term "fun z => ... z ..." when "x" is not bound in the
+ notation, as in "Notation "'twice_upto' y" := (fun x => x + x + y)". Then
+ we keep (z,x) in alp, and we have to check that what the [v] which is bound
+ to [var] does not contain z *)
+ if not (Id.equal ldots_var var) &&
+ List.exists (fun (id,_) -> occur_glob_constr id v) alp then raise No_match;
+ (* [alpmetas] is used when matching a pattern "fun x => ... x ... ?var ... x ..."
+ with an actual term "fun z => ... z ..." when "x" is bound in the
+ notation and the name "x" cannot be changed to "z", e.g. because
+ used at another occurrence, as in "Notation "'lam' y , P & Q" :=
+ ((fun y => P),(fun y => Q))". Then, we keep (z,y) in alpmetas, and we
+ have to check that "fun z => ... z ..." denotes the same term as
+ "fun x => ... x ... ?var ... x" up to alpha-conversion when [var]
+ is instantiated by [v];
+ Currently, we fail, but, eventually, [x] in [v] could be replaced by [x],
+ and, in match_, when finding "x" in subterm, failing because of a capture,
+ and, in match_, when finding "z" in subterm, replacing it with "x",
+ and, in an even further step, being even more robust, independent of the order, so
+ that e.g. the notation for ex2 works on "x y |- ex2 (fun x => y=x) (fun y => x=y)"
+ by giving, say, "exists2 x0, y=x0 & x=x0", but this would typically require the
+ glob_constr_eq in bind_term_env to be postponed in match_notation_constr, and the
+ choice of exact variable be done there; but again, this would be a non-trivial
+ refinement *)
+ let v = alpha_rename alpmetas v in
(* TODO: handle the case of multiple occs in different scopes *)
- ((var,v)::sigma,sigmalist,sigmabinders)
+ ((var,v)::terms,onlybinders,termlists,binderlists)
+
+let add_termlist_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var vl =
+ if List.exists (fun (id,_) -> List.exists (occur_glob_constr id) vl) alp then raise No_match;
+ let vl = List.map (alpha_rename alpmetas) vl in
+ (terms,onlybinders,(var,vl)::termlists,binderlists)
+
+let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v =
+ (* TODO: handle the case of multiple occs in different scopes *)
+ (terms,(var,v)::onlybinders,termlists,binderlists)
+
+let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl =
+ (terms,onlybinders,termlists,(x,bl)::binderlists)
+
+let rec pat_binder_of_term = function
+ | GVar (loc, id) -> PatVar (loc, Name id)
+ | GApp (loc, GRef (_,ConstructRef cstr,_), l) ->
+ let nparams = Inductiveops.inductive_nparams (fst cstr) in
+ let _,l = List.chop nparams l in
+ PatCstr (loc, cstr, List.map pat_binder_of_term l, Anonymous)
+ | _ -> raise No_match
-let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v =
+let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
try
- let v' = Id.List.assoc var sigma in
+ let v' = Id.List.assoc var terms in
match v, v' with
- | GHole _, _ -> fullsigma
+ | GHole _, _ -> sigma
| _, GHole _ ->
- add_env alp (Id.List.remove_assoc var sigma,sigmalist,sigmabinders) var v
+ let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in
+ add_env alp sigma var v
| _, _ ->
- if glob_constr_eq v v' then fullsigma
+ if glob_constr_eq (alpha_rename (snd alp) v) v' then sigma
else raise No_match
- with Not_found -> add_env alp fullsigma var v
+ with Not_found -> add_env alp sigma var v
-let bind_binder (sigma,sigmalist,sigmabinders) x bl =
- (sigma,sigmalist,(x,List.rev bl)::sigmabinders)
+let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var vl =
+ try
+ let vl' = Id.List.assoc var termlists in
+ let unify_term v v' =
+ match v, v' with
+ | GHole _, _ -> v'
+ | _, GHole _ -> v
+ | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in
+ let rec unify vl vl' =
+ match vl, vl' with
+ | [], [] -> []
+ | v :: vl, v' :: vl' -> unify_term v v' :: unify vl vl'
+ | _ -> raise No_match in
+ let vl = unify vl vl' in
+ let sigma = (terms,onlybinders,Id.List.remove_assoc var termlists,binderlists) in
+ add_termlist_env alp sigma var vl
+ with Not_found -> add_termlist_env alp sigma var vl
+
+let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
+ try
+ match Id.List.assoc var terms with
+ | GVar (_,id') ->
+ (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
+ sigma
+ | _ -> anomaly (str "A term which can be a binder has to be a variable")
+ with Not_found ->
+ (* The matching against a term allowing to find the instance has not been found yet *)
+ (* If it will be a different name, we shall unfortunately fail *)
+ (* TODO: look at the consequences for alp *)
+ alp, add_env alp sigma var (GVar (Loc.ghost,id))
+
+let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
+ try
+ let v' = Id.List.assoc var onlybinders in
+ match v' with
+ | Anonymous ->
+ (* Should not occur, since the term has to be bound upwards *)
+ let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+ add_binding_env alp sigma var (Name id)
+ | Name id' ->
+ if Id.equal (rename_var (snd alp) id) id' then sigma else raise No_match
+ with Not_found -> add_binding_env alp sigma var (Name id)
+
+let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
+ try
+ let v' = Id.List.assoc var onlybinders in
+ match v, v' with
+ | Anonymous, _ -> alp, sigma
+ | _, Anonymous ->
+ let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+ alp, add_binding_env alp sigma var v
+ | Name id1, Name id2 ->
+ if Id.equal id1 id2 then alp,sigma
+ else (fst alp,(id1,id2)::snd alp),sigma
+ with Not_found -> alp, add_binding_env alp sigma var v
+
+let rec map_cases_pattern_name_left f = function
+ | PatVar (loc,na) -> PatVar (loc,f na)
+ | PatCstr (loc,c,l,na) -> PatCstr (loc,c,List.map_left (map_cases_pattern_name_left f) l,f na)
+
+let rec fold_cases_pattern_eq f x p p' = match p, p' with
+ | PatVar (loc,na), PatVar (_,na') -> let x,na = f x na na' in x, PatVar (loc,na)
+ | PatCstr (loc,c,l,na), PatCstr (_,c',l',na') when eq_constructor c c' ->
+ let x,l = fold_cases_pattern_list_eq f x l l' in
+ let x,na = f x na na' in
+ x, PatCstr (loc,c,l,na)
+ | _ -> failwith "Not equal"
+
+and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
+ | [], [] -> x, []
+ | p::pl, p'::pl' ->
+ let x, p = fold_cases_pattern_eq f x p p' in
+ let x, pl = fold_cases_pattern_list_eq f x pl pl' in
+ x, p :: pl
+ | _ -> assert false
+
+let rec cases_pattern_eq p1 p2 = match p1, p2 with
+| PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2
+| PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) ->
+ eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
+ Name.equal na1 na2
+| _ -> false
+
+let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) var bl =
+ let bl = List.rev bl in
+ try
+ let bl' = Id.List.assoc var binderlists in
+ let unify_name alp na na' =
+ match na, na' with
+ | Anonymous, na' -> alp, na'
+ | na, Anonymous -> alp, na
+ | Name id, Name id' ->
+ if Id.equal id id' then alp, na'
+ else (fst alp,(id,id')::snd alp), na' in
+ let unify_pat alp p p' =
+ try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in
+ let unify_term alp v v' =
+ match v, v' with
+ | GHole _, _ -> v'
+ | _, GHole _ -> v
+ | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
+ let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
+ let unify_binder alp b b' =
+ match b, b' with
+ | (Inl na, bk, None, t), (Inl na', bk', None, t') (* assum *) ->
+ let alp, na = unify_name alp na na' in
+ alp, (Inl na, unify_binding_kind bk bk', None, unify_term alp t t')
+ | (Inl na, bk, Some c, t), (Inl na', bk', Some c', t') (* let *) ->
+ let alp, na = unify_name alp na na' in
+ alp, (Inl na, unify_binding_kind bk bk', Some (unify_term alp c c'), unify_term alp t t')
+ | (Inr p, bk, None, t), (Inr p', bk', None, t') (* pattern *) ->
+ let alp, p = unify_pat alp p p' in
+ alp, (Inr p, unify_binding_kind bk bk', None, unify_term alp t t')
+ | _ -> raise No_match in
+ let rec unify alp bl bl' =
+ match bl, bl' with
+ | [], [] -> alp, []
+ | b :: bl, b' :: bl' ->
+ let alp,b = unify_binder alp b b' in
+ let alp,bl = unify alp bl bl' in
+ alp, b :: bl
+ | _ -> raise No_match in
+ let alp, bl = unify alp bl bl' in
+ let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+ alp, add_bindinglist_env sigma var bl
+ with Not_found ->
+ alp, add_bindinglist_env sigma var bl
+
+let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) var cl =
+ try
+ let bl' = Id.List.assoc var binderlists in
+ let unify_id id na' =
+ match na' with
+ | Anonymous -> Name (rename_var (snd alp) id)
+ | Name id' ->
+ if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match in
+ let unify_pat p p' =
+ if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p'
+ else raise No_match in
+ let unify_term_binder c b' =
+ match c, b' with
+ | GVar (_, id), (Inl na', bk', None, t') (* assum *) ->
+ (Inl (unify_id id na'), bk', None, t')
+ | c, (Inr p', bk', None, t') (* pattern *) ->
+ let p = pat_binder_of_term c in
+ (Inr (unify_pat p p'), bk', None, t')
+ | _ -> raise No_match in
+ let rec unify cl bl' =
+ match cl, bl' with
+ | [], [] -> []
+ | c :: cl, (Inl _, _, Some _,t) :: bl' -> unify cl bl'
+ | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl'
+ | _ -> raise No_match in
+ let bl = unify cl bl' in
+ let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
+ add_bindinglist_env sigma var bl
+ with Not_found ->
+ anomaly (str "There should be a binder list bindings this list of terms")
let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
@@ -615,12 +857,16 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
| _ -> raise No_match
let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
- | (_,Name id2) when Id.List.mem id2 (fst metas) ->
- let rhs = match na1 with
- | Name id1 -> GVar (Loc.ghost,id1)
- | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
- alp, bind_env alp sigma id2 rhs
- | (Name id1,Name id2) -> (id1,id2)::alp,sigma
+ | (na1,Name id2) when is_onlybinding_meta id2 metas ->
+ bind_binding_env alp sigma id2 na1
+ | (Name id1,Name id2) when is_term_meta id2 metas ->
+ (* We let the non-binding occurrence define the rhs and hence reason up to *)
+ (* alpha-conversion for the given occurrence of the name (see #4592)) *)
+ bind_term_as_binding_env alp sigma id2 id1
+ | (Anonymous,Name id2) when is_term_meta id2 metas ->
+ (* We let the non-binding occurrence define the rhs *)
+ alp, sigma
+ | (Name id1,Name id2) -> ((id1,id2)::fst alp, snd alp),sigma
| (Anonymous,Anonymous) -> alp,sigma
| _ -> raise No_match
@@ -636,45 +882,69 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
let glue_letin_with_decls = true
let rec match_iterated_binders islambda decls = function
+ | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+ when islambda && Id.equal p e ->
+ match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
| GLambda (_,na,bk,t,b) when islambda ->
- match_iterated_binders islambda ((na,bk,None,t)::decls) b
+ match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
+ | GProd (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b)]))
+ when not islambda && Id.equal p e ->
+ match_iterated_binders islambda ((Inr cp,bk,None,t)::decls) b
| GProd (_,(Name _ as na),bk,t,b) when not islambda ->
- match_iterated_binders islambda ((na,bk,None,t)::decls) b
+ match_iterated_binders islambda ((Inl na,bk,None,t)::decls) b
| GLetIn (loc,na,c,b) when glue_letin_with_decls ->
match_iterated_binders islambda
- ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b
+ ((Inl na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b
| b -> (decls,b)
-let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
- (Id.List.remove_assoc x sigmavar,sigmalist,sigmabinders)
+let remove_sigma x (terms,onlybinders,termlists,binderlists) =
+ (Id.List.remove_assoc x terms,onlybinders,termlists,binderlists)
-let match_abinderlist_with_app match_fun metas sigma rest x iter termin =
- let rec aux sigma acc rest =
+let remove_bindinglist_sigma x (terms,onlybinders,termlists,binderlists) =
+ (terms,onlybinders,termlists,Id.List.remove_assoc x binderlists)
+
+let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
+
+let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas
+
+let match_binderlist_with_app match_fun alp metas sigma rest x y iter termin =
+ let rec aux sigma bl rest =
try
- let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
- let rest = Id.List.assoc ldots_var (pi1 sigma) in
+ let metas = add_ldots_var (add_meta_bindinglist y metas) in
+ let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in
+ let rest = Id.List.assoc ldots_var terms in
let b =
- match Id.List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false
+ match Id.List.assoc y binderlists with [b] -> b | _ ->assert false
in
- let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
- aux sigma (b::acc) rest
- with No_match when not (List.is_empty acc) ->
- acc, match_fun metas sigma rest termin in
- let bl,sigma = aux sigma [] rest in
- bind_binder sigma x bl
+ let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in
+ aux sigma (b::bl) rest
+ with No_match when not (List.is_empty bl) ->
+ bl, rest, sigma in
+ let bl,rest,sigma = aux sigma [] rest in
+ let alp,sigma = bind_bindinglist_env alp sigma x bl in
+ match_fun alp metas sigma rest termin
+
+let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas
-let match_alist match_fun metas sigma rest x iter termin lassoc =
+let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
let rec aux sigma acc rest =
try
- let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in
- let rest = Id.List.assoc ldots_var (pi1 sigma) in
- let t = Id.List.assoc x (pi1 sigma) in
- let sigma = remove_sigma x (remove_sigma ldots_var sigma) in
+ let metas = add_ldots_var (add_meta_term y metas) in
+ let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in
+ let rest = Id.List.assoc ldots_var terms in
+ let t = Id.List.assoc y terms in
+ let sigma = remove_sigma y (remove_sigma ldots_var sigma) in
aux sigma (t::acc) rest
with No_match when not (List.is_empty acc) ->
acc, match_fun metas sigma rest termin in
- let l,sigma = aux sigma [] rest in
- (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma)
+ let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
+ let l = if lassoc then l else List.rev l in
+ if is_bindinglist_meta x metas then
+ (* This is a recursive pattern for both bindings and terms; it is *)
+ (* registered for binders *)
+ bind_bindinglist_as_term_env alp sigma x l
+ else
+ bind_termlist_env alp sigma x l
let does_not_come_from_already_eta_expanded_var =
(* This is hack to avoid looping on a rule with rhs of the form *)
@@ -688,41 +958,67 @@ let does_not_come_from_already_eta_expanded_var =
(* checked). *)
function GVar _ -> false | _ -> true
-let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
+let rec match_ inner u alp metas sigma a1 a2 =
match (a1,a2) with
(* Matching notation variable *)
- | r1, NVar id2 when Id.List.mem id2 tmetas -> bind_env alp sigma id2 r1
+ | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 r1
+ | GVar (_,id1), NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1
+ | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 r1
(* Matching recursive notations for terms *)
- | r1, NList (x,_,iter,termin,lassoc) ->
- match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc
+ | r1, NList (x,y,iter,termin,lassoc) ->
+ match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc
+
+ (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
+ | GLambda (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+ NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e ->
+ let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
+ let alp,sigma = bind_bindinglist_env alp sigma x decls in
+ match_in u alp metas sigma b termin
(* Matching recursive notations for binders: ad hoc cases supporting let-in *)
- | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)->
- let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in
+ | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
+ let (decls,b) = match_iterated_binders true [(Inl na1,bk,None,t1)] b1 in
(* TODO: address the possibility that termin is a Lambda itself *)
- match_in u alp metas (bind_binder sigma x decls) b termin
- | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin)
+ let alp,sigma = bind_bindinglist_env alp sigma x decls in
+ match_in u alp metas sigma b termin
+
+ (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
+ | GProd (_,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+ NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e ->
+ let (decls,b) = match_iterated_binders true [(Inr cp,bk,None,t1)] b1 in
+ let alp,sigma = bind_bindinglist_env alp sigma x decls in
+ match_in u alp metas sigma b termin
+
+ | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
when na1 != Anonymous ->
- let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in
+ let (decls,b) = match_iterated_binders false [(Inl na1,bk,None,t1)] b1 in
(* TODO: address the possibility that termin is a Prod itself *)
- match_in u alp metas (bind_binder sigma x decls) b termin
+ let alp,sigma = bind_bindinglist_env alp sigma x decls in
+ match_in u alp metas sigma b termin
(* Matching recursive notations for binders: general case *)
- | r, NBinderList (x,_,iter,termin) ->
- match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin
+ | r, NBinderList (x,y,iter,termin) ->
+ match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin
(* Matching individual binders as part of a recursive pattern *)
- | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when Id.List.mem id blmetas ->
- match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
+ | GLambda (_,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,_,[cp],b1)])),
+ NLambda (Name id,_,b2)
+ when is_bindinglist_meta id metas ->
+ let alp,sigma = bind_bindinglist_env alp sigma id [(Inr cp,bk,None,t)] in
+ match_in u alp metas sigma b1 b2
+ | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2)
+ when is_bindinglist_meta id metas ->
+ let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in
+ match_in u alp metas sigma b1 b2
| GProd (_,na,bk,t,b1), NProd (Name id,_,b2)
- when Id.List.mem id blmetas && na != Anonymous ->
- match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
+ when is_bindinglist_meta id metas && na != Anonymous ->
+ let alp,sigma = bind_bindinglist_env alp sigma id [(Inl na,bk,None,t)] in
+ match_in u alp metas sigma b1 b2
(* Matching compositionally *)
- | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma
+ | 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 =
@@ -794,15 +1090,21 @@ let rec match_ inner u alp (tmetas,blmetas as 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_env alp sigma id2 t1
+ | NVar id2 -> bind_term_env alp sigma id2 t1
| _ -> assert false in
- match_in u alp metas (bind_binder 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
+ bind_bindinglist_env alp sigma id [(Inl (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
@@ -823,14 +1125,20 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
(alp,sigma) patl1 patl2 in
match_in u alp metas sigma rhs1 rhs2
+let term_of_binder = function
+ | Name id -> GVar (Loc.ghost,id)
+ | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
+
+type glob_decl2 =
+ (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
+ glob_constr option * glob_constr
+
let match_notation_constr u c (metas,pat) =
- let test (_, (_, x)) = match x with NtnTypeBinderList -> false | _ -> true in
- let vars = List.partition test metas in
- let vars = (List.map fst (fst vars), List.map fst (snd vars)) in
- let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in
+ let terms,binders,termlists,binderlists =
+ match_ false u ([],[]) metas ([],[],[],[]) c pat in
(* Reorder canonically the substitution *)
- let find x =
- try Id.List.assoc x terms
+ let find_binder x =
+ try term_of_binder (Id.List.assoc x binders)
with Not_found ->
(* Happens for binders bound to Anonymous *)
(* Find a better way to propagate Anonymous... *)
@@ -838,11 +1146,15 @@ let match_notation_constr u c (metas,pat) =
List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
match typ with
| NtnTypeConstr ->
- ((find x, scl)::terms',termlists',binders')
+ let term = try Id.List.assoc x terms with Not_found -> raise No_match in
+ ((term, scl)::terms',termlists',binders')
+ | NtnTypeOnlyBinder ->
+ ((find_binder x, scl)::terms',termlists',binders')
| NtnTypeConstrList ->
(terms',(Id.List.assoc x termlists,scl)::termlists',binders')
| NtnTypeBinderList ->
- (terms',termlists',(Id.List.assoc x binders,scl)::binders'))
+ let bl = try Id.List.assoc x binderlists with Not_found -> raise No_match in
+ (terms',termlists',(bl, scl)::binders'))
metas ([],[],[])
(* Matching cases pattern *)
@@ -851,17 +1163,31 @@ let add_patterns_for_params ind l =
let nparams = mib.Declarations.mind_nparams in
Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l
-let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
+let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v =
try
- let vvar = Id.List.assoc var sigma in
- if cases_pattern_eq v vvar then fullsigma else raise No_match
+ let vvar = Id.List.assoc var terms in
+ if cases_pattern_eq v vvar then sigma else raise No_match
with Not_found ->
(* TODO: handle the case of multiple occs in different scopes *)
- (var,v)::sigma,sigmalist,x
+ (var,v)::terms,x,termlists,y
+
+let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
+ let rec aux sigma acc rest =
+ try
+ let metas = add_ldots_var (add_meta_term y metas) in
+ let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in
+ let rest = Id.List.assoc ldots_var terms in
+ let t = Id.List.assoc y terms in
+ let sigma = remove_sigma y (remove_sigma ldots_var sigma) in
+ aux sigma (t::acc) rest
+ with No_match when not (List.is_empty acc) ->
+ acc, match_fun metas sigma rest termin in
+ let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
+ (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists)
-let rec match_cases_pattern metas sigma a1 a2 =
+let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
match (a1,a2) with
- | r1, NVar id2 when Id.List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
+ | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
| PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
| PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
sigma,(0,add_patterns_for_params (fst r1) largs)
@@ -875,15 +1201,15 @@ let rec match_cases_pattern metas sigma a1 a2 =
else
let l1',more_args = Util.List.chop le2 l1 in
(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
- | r1, NList (x,_,iter,termin,lassoc) ->
- (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas)
- (metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),(0,[])
+ | r1, NList (x,y,iter,termin,lassoc) ->
+ (match_cases_pattern_list (match_cases_pattern_no_more_args)
+ metas (terms,(),termlists,()) r1 x y iter termin lassoc),(0,[])
| _ -> raise No_match
and match_cases_pattern_no_more_args metas sigma a1 a2 =
match match_cases_pattern metas sigma a1 a2 with
- |out,(_,[]) -> out
- |_ -> raise No_match
+ | out,(_,[]) -> out
+ | _ -> raise No_match
let match_ind_pattern metas sigma ind pats a2 =
match a2 with
@@ -904,16 +1230,15 @@ let reorder_canonically_substitution terms termlists metas =
List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
match typ with
| NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists')
+ | NtnTypeOnlyBinder -> assert false
| NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists')
| NtnTypeBinderList -> assert false)
metas ([],[])
let match_notation_constr_cases_pattern c (metas,pat) =
- let vars = List.map fst metas in
- let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in
+ let (terms,(),termlists,()),more_args = match_cases_pattern metas ([],(),[],()) c pat in
reorder_canonically_substitution terms termlists metas, more_args
let match_notation_constr_ind_pattern ind args (metas,pat) =
- let vars = List.map fst metas in
- let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in
+ let (terms,(),termlists,()),more_args = match_ind_pattern metas ([],(),[],()) ind args pat in
reorder_canonically_substitution terms termlists metas, more_args
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 280ccfd2..c8fcbf74 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 : Id.t list * Id.t list -> 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]} *)
+
+(** 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 * reversibility_flag
-(** 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,14 +40,19 @@ 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 *)
exception No_match
+type glob_decl2 =
+ (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
+ glob_constr option * glob_constr
val match_notation_constr : bool -> glob_constr -> interpretation ->
(glob_constr * subscopes) list * (glob_constr list * subscopes) list *
- (glob_decl list * subscopes) list
+ (glob_decl2 list * subscopes) list
val match_notation_constr_cases_pattern :
cases_pattern -> interpretation ->
@@ -55,9 +64,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/reserve.ml b/interp/reserve.ml
index 7e42c1a2..388ca080 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -8,7 +8,7 @@
(* Reserved names *)
-open Errors
+open CErrors
open Util
open Pp
open Names
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 1f28ba65..47877421 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -13,7 +13,7 @@
(* *)
open Pp
-open Errors
+open CErrors
open Libnames
open Globnames
open Misctypes
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 9c3ed941..2a7d52e3 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 d8904dab..e1f648d7 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 db548ec3..2523063e 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Names
@@ -43,7 +43,7 @@ let is_alias_of_already_visible_name sp = function
false
let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
- if not (is_alias_of_already_visible_name sp pat) then begin
+ if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin
Nametab.push_syndef (Nametab.Exactly i) sp kn;
match onlyparse with
| None ->
@@ -84,23 +84,21 @@ let declare_syntactic_definition local id onlyparse pat =
let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn)
-let allow_compat_notations = ref true
-let verbose_compat_notations = ref false
+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
+ | _ -> strbrk " is a compatibility notation"
+ in
+ let since = strbrk " since Coq > " ++ str (Flags.pr_version v) ++ str "." in
+ pr_syndef kn ++ pp_def ++ since
-let is_verbose_compat () =
- !verbose_compat_notations || not !allow_compat_notations
+let warn_compatibility_notation =
+ 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 ->
- let act =
- if !verbose_compat_notations then msg_warning else errorlabstrm ""
- in
- let pp_def = match def with
- | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r
- | _ -> str " is a compatibility notation"
- in
- let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in
- act (pr_syndef kn ++ pp_def ++ since)
+ | Some v when Flags.version_strictly_greater v ->
+ warn_compatibility_notation (kn, def, v)
| _ -> ()
let search_syntactic_definition kn =
@@ -110,21 +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) }
-
-let set_compat_notations =
- declare_bool_option
- { optsync = true;
- optdepr = false;
- optname = "accept compatibility notations";
- optkey = ["Compat"; "Notations"];
- optread = (fun () -> !allow_compat_notations);
- optwrite = ((:=) allow_compat_notations) }
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 7a1c9c5c..55e2848e 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -17,9 +17,3 @@ val declare_syntactic_definition : bool -> Id.t ->
Flags.compat_version option -> syndef_interpretation -> unit
val search_syntactic_definition : kernel_name -> syndef_interpretation
-
-(** Options concerning verbose display of compatibility notations
- or their deactivation *)
-
-val set_verbose_compat_notations : bool -> unit
-val set_compat_notations : bool -> unit
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cc8e697e..79eeacf3 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -8,7 +8,7 @@
(*i*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -19,14 +19,13 @@ 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.optname = "no parameters in constructors";
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,13 +51,14 @@ 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'
| CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat
| CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a
| CPatPrim _ | CPatAtom _ -> a
+ | CPatCast _ -> assert false
let ids_of_pattern_list =
List.fold_left
@@ -67,11 +67,11 @@ 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
- (fun (_,(ona,indnal)) l ->
+ (fun (_, ona, indnal) l ->
Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
indnal
(Option.fold_right (Loc.down_located (name_fold Id.Set.add)) ona l))
@@ -92,6 +92,8 @@ 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
| [] ->
f n acc b
@@ -111,11 +113,11 @@ let fold_constr_expr_with_binders g f n acc = function
| CDelimiters (loc,_,a) -> f n acc a
| CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
acc
- | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
+ | CRecord (loc,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
| CCases (loc,sty,rtnpo,al,bl) ->
let ids = ids_of_cases_tomatch al in
let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
- let acc = List.fold_left (f n) acc (List.map fst al) in
+ let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
List.fold_right (fun (loc,patl,rhs) acc ->
let ids = ids_of_pattern_list patl in
f (Id.Set.fold g ids n) acc rhs) bl acc
@@ -132,7 +134,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
@@ -170,6 +172,7 @@ 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
| [] ->
user_err_loc(loc,"",
str "No parameter named " ++ Nameops.pr_id id ++ str".")
@@ -191,7 +194,9 @@ let map_local_binders f g e bl =
LocalRawAssum(nal,k,ty) ->
(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) in
+ (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl)
+ | LocalPattern _ ->
+ assert false in
let (e,rbl) = List.fold_left h (e,[]) bl in
(e, List.rev rbl)
@@ -213,14 +218,14 @@ let map_constr_expr_with_binders g f e = function
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
| CPrim _ | CRef _ as x -> x
- | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l)
+ | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l)
| CCases (loc,sty,rtnpo,a,bl) ->
let bl = List.map (fun (loc,patl,rhs) ->
let ids = ids_of_pattern_list patl in
(loc,patl,f (Id.Set.fold g ids e) rhs)) bl in
let ids = ids_of_cases_tomatch a in
let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
- CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
+ CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
| CLetTuple (loc,nal,(ona,po),b,c) ->
let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in
let e'' = Option.fold_right (Loc.down_located (name_fold g)) ona e in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1e867c19..58edd4dd 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.39.1) at 2024-05-01 20:41:08 +0000