From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- interp/constrarg.ml | 72 ++-- interp/constrarg.mli | 43 +- interp/constrexpr_ops.ml | 106 +++-- interp/constrexpr_ops.mli | 5 + interp/constrextern.ml | 184 ++++----- interp/constrextern.mli | 3 +- interp/constrintern.ml | 845 +++++++++++++++++++++++++--------------- interp/constrintern.mli | 9 +- interp/coqlib.ml | 4 +- interp/dumpglob.ml | 17 +- interp/dumpglob.mli | 2 +- interp/genintern.ml | 14 +- interp/implicit_quantifiers.ml | 24 +- interp/implicit_quantifiers.mli | 4 +- interp/notation.ml | 199 +++++----- interp/notation.mli | 21 +- interp/notation_ops.ml | 745 +++++++++++++++++++++++++---------- interp/notation_ops.mli | 37 +- interp/reserve.ml | 2 +- interp/smartlocate.ml | 2 +- interp/stdarg.ml | 25 +- interp/stdarg.mli | 5 + interp/syntax_def.ml | 48 +-- interp/syntax_def.mli | 6 - interp/topconstr.ml | 35 +- interp/topconstr.mli | 4 +- 26 files changed, 1542 insertions(+), 919 deletions(-) (limited to 'interp') 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 -- cgit v1.2.3