diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 5 | ||||
| -rw-r--r-- | interp/constrextern.ml | 223 | ||||
| -rw-r--r-- | interp/constrextern.mli | 20 | ||||
| -rw-r--r-- | interp/constrintern.ml | 123 | ||||
| -rw-r--r-- | interp/constrintern.mli | 6 | ||||
| -rw-r--r-- | interp/notation.ml | 36 | ||||
| -rw-r--r-- | interp/notation.mli | 5 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 13 |
8 files changed, 307 insertions, 124 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 79e0e61646..396dde0465 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -45,8 +45,11 @@ let names_of_local_binders bl = (**********************************************************************) (* Functions on constr_expr *) +(* Note: redundant Numeral representations such as -0 and +0 (or different + numbers of leading zeros) are considered different here. *) + let prim_token_eq t1 t2 = match t1, t2 with -| Numeral i1, Numeral i2 -> Bigint.equal i1 i2 +| Numeral (n1,s1), Numeral (n2,s2) -> String.equal n1 n2 && s1 == s2 | String s1, String s2 -> String.equal s1 s2 | _ -> false diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f6da10c961..8a798bfb00 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -66,22 +66,138 @@ let print_universes = Detyping.print_universes (* This suppresses printing of primitive tokens (e.g. numeral) and notations *) let print_no_symbol = ref false -(* This tells which notations still not to used if print_no_symbol is true *) -let print_non_active_notations = ref ([] : interp_rule list) +(**********************************************************************) +(* Turning notations and scopes on and off for printing *) +module IRuleSet = Set.Make(struct + type t = interp_rule + let compare x y = Pervasives.compare x y + end) + +let inactive_notations_table = + Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty) +let inactive_scopes_table = + Summary.ref ~name:"inactive_scopes_table" CString.Set.empty + +let show_scope scopt = + match scopt with + | None -> str "" + | Some sc -> spc () ++ str "in scope" ++ spc () ++ str sc + +let _show_inactive_notations () = + begin + if CString.Set.is_empty !inactive_scopes_table + then + Feedback.msg_notice (str "No inactive notation scopes.") + else + let _ = Feedback.msg_notice (str "Inactive notation scopes:") in + CString.Set.iter (fun sc -> Feedback.msg_notice (str " " ++ str sc)) + !inactive_scopes_table + end; + if IRuleSet.is_empty !inactive_notations_table + then + Feedback.msg_notice (str "No individual inactive notations.") + else + let _ = Feedback.msg_notice (str "Inactive notations:") in + IRuleSet.iter + (function + | NotationRule (scopt, ntn) -> + Feedback.msg_notice (str ntn ++ show_scope scopt) + | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn))) + !inactive_notations_table + +let deactivate_notation nr = + match nr with + | SynDefRule kn -> + (* shouldn't we check wether it is well defined? *) + inactive_notations_table := IRuleSet.add nr !inactive_notations_table + | NotationRule (scopt, ntn) -> + match availability_of_notation (scopt, ntn) (scopt, []) with + | None -> user_err ~hdr:"Notation" + (str ntn ++ spc () ++ str "does not exist" + ++ (match scopt with + | None -> spc () ++ str "in the empty scope." + | Some _ -> show_scope scopt ++ str ".")) + | Some _ -> + if IRuleSet.mem nr !inactive_notations_table then + Feedback.msg_warning + (str "Notation" ++ spc () ++ str ntn ++ spc () + ++ str "is already inactive" ++ show_scope scopt ++ str ".") + else inactive_notations_table := IRuleSet.add nr !inactive_notations_table + +let reactivate_notation nr = + try + inactive_notations_table := + IRuleSet.remove nr !inactive_notations_table + with Not_found -> + match nr with + | NotationRule (scopt, ntn) -> + Feedback.msg_warning (str "Notation" ++ spc () ++ str ntn ++ spc () + ++ str "is already active" ++ show_scope scopt ++ + str ".") + | SynDefRule kn -> + Feedback.msg_warning + (str "Notation" ++ spc () ++ str (Names.KerName.to_string kn) + ++ spc () ++ str "is already active.") + + +let deactivate_scope sc = + ignore (find_scope sc); (* ensures that the scope exists *) + if CString.Set.mem sc !inactive_scopes_table + then + Feedback.msg_warning (str "Notation Scope" ++ spc () ++ str sc ++ spc () + ++ str "is already inactive.") + else + inactive_scopes_table := CString.Set.add sc !inactive_scopes_table + +let reactivate_scope sc = + try + inactive_scopes_table := CString.Set.remove sc !inactive_scopes_table + with Not_found -> + Feedback.msg_warning (str "Notation Scope" ++ spc () ++ str sc ++ spc () + ++ str "is already active.") + +let is_inactive_rule nr = + IRuleSet.mem nr !inactive_notations_table || + match nr with + | NotationRule (Some sc, ntn) -> CString.Set.mem sc !inactive_scopes_table + | NotationRule (None, ntn) -> false + | SynDefRule _ -> false + +(* args: notation, scope, activate/deactivate *) +let toggle_scope_printing ~scope ~activate = + if activate then + reactivate_scope scope + else + deactivate_scope scope + +let toggle_notation_printing ?scope ~notation ~activate = + if activate then + reactivate_notation (NotationRule (scope, notation)) + else + deactivate_notation (NotationRule (scope, notation)) (* This governs printing of projections using the dot notation symbols *) let print_projections = ref false let print_meta_as_hole = ref false -let with_arguments f = Flags.with_option print_arguments f -let with_implicits f = Flags.with_option print_implicits f -let with_coercions f = Flags.with_option print_coercions f let with_universes f = Flags.with_option print_universes f let with_meta_as_hole f = Flags.with_option print_meta_as_hole f let without_symbols f = Flags.with_option print_no_symbol f -let without_specific_symbols l f = - Flags.with_extra_values print_non_active_notations l f + +(* XXX: Where to put this in the library? Util maybe? *) +let protect_ref r nf f x = + let old_ref = !r in + r := nf !r; + try let res = f x in r := old_ref; res + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + r := old_ref; + Exninfo.iraise reraise + +let without_specific_symbols l = + protect_ref inactive_notations_table + (fun tbl -> IRuleSet.(union (of_list l) tbl)) (**********************************************************************) (* Control printing of records *) @@ -239,23 +355,31 @@ let expand_curly_brackets loc mknot ntn l = let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None +let is_number s = + let rec aux i = + Int.equal (String.length s) i || + match s.[i] with '0'..'9' -> aux (i+1) | _ -> false + in aux 0 + +let is_zero s = + let rec aux i = + Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1)) + in aux 0 + let make_notation_gen loc ntn mknot mkprim destprim l = if has_curly_brackets ntn then expand_curly_brackets loc mknot ntn l else match ntn,List.map destprim l with (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *) - | "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p -> + | "- _", [Some (Numeral (p,true))] when not (is_zero p) -> mknot (loc,ntn,([mknot (loc,"( _ )",l)])) | _ -> match decompose_notation_key ntn, l with - | [Terminal "-"; Terminal x], [] -> - (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x))) - with Failure _ -> mknot (loc,ntn,[])) - | [Terminal x], [] -> - (try mkprim (loc, Numeral (Bigint.of_string x)) - with Failure _ -> mknot (loc,ntn,[])) - | _ -> - mknot (loc,ntn,l) + | [Terminal "-"; Terminal x], [] when is_number x -> + mkprim (loc, Numeral (x,false)) + | [Terminal x], [] when is_number x -> + mkprim (loc, Numeral (x,true)) + | _ -> mknot (loc,ntn,l) let make_notation loc ntn (terms,termlists,binders as subst) = if not (List.is_empty termlists) || not (List.is_empty binders) then @@ -288,17 +412,8 @@ let pattern_printable_in_both_syntax (ind,_ as c) = (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = - (* pboutill: There are letins in pat which is incompatible with notations and - not explicit application. *) - match pat with - | { loc; v = PatCstr(cstrsp,args,na) } - 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 - CAst.make ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) - | _ -> try - if !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; let (na,sc,p) = uninterp_prim_token_cases_pattern pat in match availability_of_prim_token p sc scopes with | None -> raise No_match @@ -307,7 +422,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na with No_match -> try - if !Flags.raw_print || !print_no_symbol then raise No_match; + if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_pattern scopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> @@ -321,21 +436,19 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = if !Flags.raw_print then raise Exit; let projs = Recordops.lookup_projections (fst cstrsp) in let rec ip projs args acc = - match projs with - | [] -> acc - | None :: q -> ip q args acc - | Some c :: q -> - match args with - | [] -> raise No_match - - - - - - | { CAst.v = CPatAtom None } :: tail -> ip q tail acc - (* we don't want to have 'x = _' in our patterns *) - | head :: tail -> ip q tail - ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) + match projs, args with + | [], [] -> acc + | proj :: q, pat :: tail -> + let acc = + match proj, pat with + | _, { CAst.v = CPatAtom None } -> + (* we don't want to have 'x := _' in our patterns *) + acc + | Some c, _ -> + ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc) + | _ -> raise No_match in + ip q tail acc + | _ -> assert false in CPatRecord(List.rev (ip projs args [])) with @@ -401,7 +514,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try - if List.mem keyrule !print_non_active_notations then raise No_match; + if is_inactive_rule keyrule then raise No_match; let loc = t.loc in match t.v with | PatCstr (cstr,_,na) -> @@ -417,8 +530,8 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try - if List.mem keyrule !print_non_active_notations then raise No_match; - apply_notation_to_pattern (IndRef ind) + if is_inactive_rule keyrule then raise No_match; + apply_notation_to_pattern (IndRef ind) (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with No_match -> extern_notation_ind_pattern allscopes vars ind args rules @@ -663,9 +776,11 @@ let rec extern inctx scopes vars r = | GEvar (n,l) -> extern_evar n (List.map (on_snd (extern false scopes vars)) l) - | GPatVar (b,n) -> + | GPatVar kind -> if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else - if b then CPatVar n else CEvar (n,[]) + (match kind with + | Evar_kinds.SecondOrderPatVar n -> CPatVar n + | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) | GApp (f,args) -> (match f with @@ -698,7 +813,7 @@ let rec extern inctx scopes vars r = | None :: q -> raise No_match | Some c :: q -> match locs with - | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern]") + | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].") | (_, false) :: locs' -> (* we don't want to print locals *) ip q locs' args acc @@ -886,7 +1001,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function | (keyrule,pat,n as _rule)::rules -> let loc = Glob_ops.loc_of_glob_constr t in try - if List.mem keyrule !print_non_active_notations then raise No_match; + if is_inactive_rule keyrule then raise No_match; (* Adjusts to the number of arguments expected by the notation *) let (t,args,argsscopes,argsimpls) = match t.v ,n with | GApp (f,args), Some n @@ -1033,17 +1148,17 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with let id = try match lookup_name_of_rel n env with | Name id -> id | Anonymous -> - anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable") + anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.") with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar id | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) - | PMeta (Some n) -> GPatVar (false,n) + | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) | PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None), [glob_of_pat env sigma c]) | PApp (f,args) -> GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) | PSoApp (n,args) -> - GApp (CAst.make @@ GPatVar (true,n), + GApp (CAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n), List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) @@ -1064,7 +1179,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with | _, Some ind -> let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in simple_cases_matrix_of_branches ind bl' - | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive") + | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.") in let mat = if info.cip_extensible then mat @ [any_any_branch] else mat in @@ -1072,7 +1187,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with | PMeta None, _, _ -> (Anonymous,None),None | _, Some ind, Some nargs -> return_type_of_predicate ind nargs (glob_of_pat env sigma p) - | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive") + | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) | PFix f -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))).v (** FIXME bad env *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index ea627cff11..6c82168e48 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -59,16 +59,6 @@ val set_extern_reference : val get_extern_reference : unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -(** This governs printing of implicit arguments. If [with_implicits] is - on and not [with_arguments] then implicit args are printed prefixed - by "!"; if [with_implicits] and [with_arguments] are both on the - function and not the arguments is prefixed by "!" *) -val with_implicits : ('a -> 'b) -> 'a -> 'b -val with_arguments : ('a -> 'b) -> 'a -> 'b - -(** This forces printing of coercions *) -val with_coercions : ('a -> 'b) -> 'a -> 'b - (** This forces printing universe names of Type\{.\} *) val with_universes : ('a -> 'b) -> 'a -> 'b @@ -80,3 +70,13 @@ val without_specific_symbols : interp_rule list -> ('a -> 'b) -> 'a -> 'b (** This prints metas as anonymous holes *) val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b + +(** Fine-grained activation and deactivation of notation printing. + *) +val toggle_scope_printing : + scope:Notation_term.scope_name -> activate:bool -> unit + +val toggle_notation_printing : + ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit + + diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 190369e8fa..89827300c4 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -46,7 +46,7 @@ open Context.Rel.Declaration types and recursive definitions and of projection names in records *) type var_internalization_type = - | Inductive of Id.t list (* list of params *) + | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *) | Recursive | Method | Variable @@ -176,7 +176,7 @@ let parsing_explicit = ref false let empty_internalization_env = Id.Map.empty let compute_explicitable_implicit imps = function - | Inductive params -> + | Inductive (params,_) -> (* In inductive types, the parameters are fixed implicit arguments *) let sub_impl,_ = List.chop (List.length params) imps in let sub_impl' = List.filter is_status_implicit sub_impl in @@ -190,10 +190,10 @@ let compute_internalization_data env ty typ impl = let expls_impl = compute_explicitable_implicit impl ty in (ty, expls_impl, impl, compute_arguments_scope typ) -let compute_internalization_env env ty = +let compute_internalization_env env ?(impls=empty_internalization_env) ty = List.fold_left3 (fun map id typ impl -> Id.Map.add id (compute_internalization_data env ty typ impl) map) - empty_internalization_env + impls (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -358,16 +358,17 @@ let locate_if_hole ?loc na = function let reset_hidden_inductive_implicit_test env = { env with impls = Id.Map.map (function - | (Inductive _,b,c,d) -> (Inductive [],b,c,d) + | (Inductive (params,_),b,c,d) -> (Inductive (params,false),b,c,d) | x -> x) env.impls } -let check_hidden_implicit_parameters id impls = +let check_hidden_implicit_parameters ?loc id impls = if Id.Map.exists (fun _ -> function - | (Inductive indparams,_,_,_) -> Id.List.mem id indparams + | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams | _ -> false) impls then - user_err (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.") + user_err ?loc (pr_id id ++ strbrk " is already used as name of " ++ + strbrk "a parameter of the inductive type; bound variables in " ++ + strbrk "the type of a constructor shall use a different name.") let push_name_env ?(global_level=false) ntnvars implargs env = function @@ -376,7 +377,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env = user_err ?loc (str "Anonymous variables not allowed"); env | loc,Name id -> - check_hidden_implicit_parameters id env.impls ; + check_hidden_implicit_parameters ?loc id env.impls ; if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; set_var_scope ?loc id false env ntnvars; @@ -616,7 +617,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = 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 + 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 @@ -659,7 +660,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = termin bl in make_letins letins res with Not_found -> - anomaly (Pp.str "Inconsistent substitution of recursive notation")) + anomaly (Pp.str "Inconsistent substitution of recursive notation.")) | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt -> let a,letins = snd (Option.get binderopt) in let e = make_letins letins (aux subst' infos c') in @@ -785,7 +786,7 @@ let find_appl_head_data c = let scopes = find_arguments_scope ref in c, impls, scopes, [] | GApp ({ v = GRef (ref,_) },l) - when l != [] && Flags.version_strictly_greater Flags.V8_2 -> + when l != [] -> let n = List.length l in let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in @@ -962,6 +963,45 @@ let check_constructor_length env loc cstr len_pl pl0 = (error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr))) +open Term +open Declarations + +(* Similar to Cases.adjust_local_defs but on RCPat *) +let insert_local_defs_in_pattern (ind,j) l = + let (mib,mip) = Global.lookup_inductive ind in + if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then + (* Optimisation *) l + else + let typi = mip.mind_nf_lc.(j-1) in + let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in + let (decls,_) = decompose_prod_assum typi in + let rec aux decls args = + match decls, args with + | Context.Rel.Declaration.LocalDef _ :: decls, args -> (CAst.make @@ RCPatAtom None) :: aux decls args + | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *) + | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args + | _ -> assert false in + aux (List.rev decls) l + +let add_local_defs_and_check_length loc env g pl args = match g with + | ConstructRef cstr -> + (* We consider that no variables corresponding to local binders + have been given in the "explicit" arguments, which come from a + "@C args" notation or from a custom user notation *) + let pl' = insert_local_defs_in_pattern cstr pl in + let maxargs = Inductiveops.constructor_nalldecls cstr in + if List.length pl' + List.length args > maxargs then + error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr); + (* Two possibilities: either the args are given with explict + variables for local definitions, then we give the explicit args + extended with local defs, so that there is nothing more to be + added later on; or the args are not enough to have all arguments, + which a priori means local defs to add in the [args] part, so we + postpone the insertion of local defs in the explicit args *) + (* Note: further checks done later by check_constructor_length *) + if List.length pl' + List.length args = maxargs then pl' else pl + | _ -> pl + let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = let impl_list = if Int.equal len_pl1 0 then select_impargs_size (List.length pl2) impls_st @@ -1070,7 +1110,7 @@ let sort_fields ~complete loc fields completer = 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 + 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 *) @@ -1085,7 +1125,7 @@ let sort_fields ~complete loc fields completer = let field_glob_ref = ConstRef field_glob_id 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") + | [] -> 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 @@ -1179,6 +1219,11 @@ let alias_of als = match als.alias_ids with *) +let is_zero s = + let rec aux i = + Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1)) + in aux 0 + let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 let product_of_cases_patterns aliases idspl = @@ -1199,7 +1244,7 @@ let rec subst_pat_iterator y t = CAst.(map (function | RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a) | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl))) -let drop_notations_pattern looked_for = +let drop_notations_pattern looked_for genv = (* At toplevel, Constructors and Inductives are accepted, in recursive calls only constructor are allowed *) let ensure_kind top loc g = @@ -1218,7 +1263,7 @@ let drop_notations_pattern looked_for = | GHole (_,_,_) -> RCPatAtom (None) | GRef (g,_) -> RCPatCstr (g,[],[]) | GApp ({ v = GRef (g,_) }, l) -> RCPatCstr (g, List.map rcp_of_glob l,[]) - | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr "))) x + | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x in let rec drop_syndef top scopes re pats = let (loc,qid) = qualid_of_reference re in @@ -1291,9 +1336,9 @@ let drop_notations_pattern looked_for = (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) - | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral p) }],[]),[]) - when Bigint.is_strictly_pos p -> - let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in + | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral (p,true)) }],[]),[]) + when not (is_zero p) -> + let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in rcp_of_glob pat | CPatNotation ("( _ )",([a],[]),[]) -> in_pat top scopes a @@ -1345,7 +1390,7 @@ let drop_notations_pattern looked_for = in_pat top (scopt,subscopes@snd scopes) a with Not_found -> if Id.equal id ldots_var then CAst.make ?loc @@ RCPatAtom (Some id) else - anomaly (str "Unbound pattern notation variable: " ++ Id.print id) + anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".") end | NRef g -> ensure_kind top loc g; @@ -1354,9 +1399,9 @@ let drop_notations_pattern looked_for = | NApp (NRef g,pl) -> ensure_kind top loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in - CAst.make ?loc @@ RCPatCstr (g, - List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @ - List.map (in_pat false scopes) args, []) + let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in + let pl = add_local_defs_and_check_length loc genv g pl args in + CAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, []) | NList (x,y,iter,terminator,lassoc) -> if not (List.is_empty args) then user_err ?loc (strbrk "Application of arguments to a recursive notation not supported in patterns."); @@ -1370,7 +1415,7 @@ let drop_notations_pattern looked_for = subst_pat_iterator ldots_var t u) (if lassoc then List.rev l else l) termin with Not_found -> - anomaly (Pp.str "Inconsistent substitution of recursive notation")) + anomaly (Pp.str "Inconsistent substitution of recursive notation.")) | NHole _ -> let () = assert (List.is_empty args) in CAst.make ?loc @@ RCPatAtom None @@ -1417,7 +1462,7 @@ let rec intern_pat genv aliases pat = let intern_cases_pattern genv scopes aliases pat = intern_pat genv aliases - (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat) + (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat) let _ = intern_cases_pattern_fwd := @@ -1426,7 +1471,7 @@ let _ = let intern_ind_pattern genv scopes pat = let no_not = try - drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat + drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc in let loc = no_not.CAst.loc in @@ -1464,7 +1509,7 @@ let get_implicit_name n imps = let set_hole_implicit i b = function | {loc; v = GRef (r,_) } | { v = GApp ({loc; v = GRef (r,_)},_) } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) | {loc; v = GVar id } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) - | _ -> anomaly (Pp.str "Only refs have implicits") + | _ -> anomaly (Pp.str "Only refs have implicits.") let exists_implicit_name id = List.exists (fun imp -> is_status_implicit imp && Id.equal id (name_of_implicit imp)) @@ -1506,7 +1551,7 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) -let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = +let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let rec intern env = CAst.with_loc_val (fun ?loc -> function | CRef (ref,us) -> let (c,imp,subscopes,l),_ = @@ -1599,9 +1644,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = CAst.make ?loc @@ GLetIn (snd na, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) - | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[])) - when Bigint.is_strictly_pos p -> - intern env (CAst.make ?loc @@ CPrim (Numeral (Bigint.neg p))) + | CNotation ("- _",([{ CAst.v = CPrim (Numeral (p,true)) }],[],[])) + when not (is_zero p) -> + intern env (CAst.make ?loc @@ CPrim (Numeral (p,false))) | CNotation ("( _ )",([a],[],[])) -> intern env a | CNotation (ntn,args) -> intern_notation intern env ntnvars loc ntn args @@ -1749,12 +1794,12 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = CAst.make ?loc @@ GHole (k, naming, solve) (* Parsing pattern variables *) - | CPatVar n when allow_patvar -> + | CPatVar n when pattern_mode -> CAst.make ?loc @@ - GPatVar (true,n) - | CEvar (n, []) when allow_patvar -> + GPatVar (Evar_kinds.SecondOrderPatVar n) + | CEvar (n, []) when pattern_mode -> CAst.make ?loc @@ - GPatVar (false,n) + GPatVar (Evar_kinds.FirstOrderPatVar n) (* end *) (* Parsing existential variables *) | CEvar (n, l) -> @@ -1944,13 +1989,13 @@ let empty_ltac_sign = { } let intern_gen kind env - ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign) + ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) c = let tmp_scope = scope_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; impls = impls} - allow_patvar (ltacvars, Id.Map.empty) c + pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env c = intern_gen WithoutTypeConstraint env c @@ -2023,7 +2068,7 @@ let interp_type_evars env evdref ?(impls=empty_internalization_env) c = let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let c = intern_gen (if as_type then IsType else WithoutTypeConstraint) - ~allow_patvar:true ~ltacvars env c in + ~pattern_mode:true ~ltacvars env c in pattern_of_glob_constr c let interp_notation_constr ?(impls=empty_internalization_env) nenv a = diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 644f60d850..a92e94d97b 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -38,7 +38,7 @@ open Misctypes of [env] *) type var_internalization_type = - | Inductive of Id.t list (* list of params *) + | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *) | Recursive | Method | Variable @@ -61,7 +61,7 @@ val empty_internalization_env : internalization_env val compute_internalization_data : env -> var_internalization_type -> types -> Impargs.manual_explicitation list -> var_internalization_data -val compute_internalization_env : env -> var_internalization_type -> +val compute_internalization_env : env -> ?impls:internalization_env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env @@ -83,7 +83,7 @@ val intern_constr : env -> constr_expr -> glob_constr val intern_type : env -> constr_expr -> glob_constr val intern_gen : typing_constraint -> env -> - ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign -> constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> diff --git a/interp/notation.ml b/interp/notation.ml index d19654b10b..300f6b1dd0 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -10,7 +10,6 @@ open CErrors open Util open Pp -open Bigint open Names open Term open Libnames @@ -319,16 +318,34 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) = (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table) patl -let mkNumeral n = Numeral n +let mkNumeral n = + if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true) + else Numeral (Bigint.to_string (Bigint.neg n), false) + +let ofNumeral n s = + if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) + 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)) +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign + +let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) = + declare_prim_token_interpreter sc + (fun cont ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s) + | p -> cont ?loc p) + (patl, (fun r -> match uninterp r with + | None -> None + | Some (n,s) -> Some (Numeral (n,s))), inpat) + let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = + let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in declare_prim_token_interpreter sc - (fun cont ?loc -> function Numeral n-> delay dir interp ?loc n | p -> cont ?loc p) + (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s) + | p -> cont ?loc p) (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat) let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = @@ -381,7 +398,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function let declare_notation_level ntn level = if String.Map.mem ntn !notation_level_map then - anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level"); + anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level."); notation_level_map := String.Map.add ntn level !notation_level_map let level_of_notation ntn = @@ -440,8 +457,8 @@ let find_notation ntn sc = (n.not_interp, n.not_location) let notation_of_prim_token = function - | Numeral n when is_pos_or_zero n -> to_string n - | Numeral n -> "- "^(to_string (neg n)) + | Numeral (n,true) -> n + | Numeral (n,false) -> "- "^n | String _ -> raise Not_found let find_prim_token check_allowed ?loc p sc = @@ -466,7 +483,8 @@ let interp_prim_token_gen ?loc g p local_scopes = with Not_found -> user_err ?loc ~hdr:"interp_prim_token" ((match p with - | Numeral n -> str "No interpretation for numeral " ++ str (to_string n) + | Numeral _ -> + str "No interpretation for numeral " ++ str (notation_of_prim_token p) | String s -> str "No interpretation for string " ++ qs s) ++ str ".") let interp_prim_token ?loc = @@ -1004,13 +1022,13 @@ let declare_notation_rule ntn ~extra unpl gram = let find_notation_printing_rule ntn = try pi1 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No printing rule found for " ++ str ntn) + with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".") let find_notation_extra_printing_rules ntn = 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) + with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".") let get_defined_notations () = String.Set.elements @@ String.Map.domain !notation_rules diff --git a/interp/notation.mli b/interp/notation.mli index d271a88fe7..c739ec12fd 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -74,6 +74,11 @@ type 'a prim_token_interpreter = type 'a prim_token_uninterpreter = glob_constr list * (glob_constr -> 'a option) * cases_pattern_status +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign + +val declare_rawnumeral_interpreter : scope_name -> required_module -> + rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit + val declare_numeral_interpreter : scope_name -> required_module -> bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 8e876ec16d..33b93606ec 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -690,7 +690,7 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig | { CAst.v = 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") + | _ -> 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 *) @@ -830,7 +830,7 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v 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") + anomaly (str "There should be a binder list bindings this list of terms.") let match_fix_kind fk1 fk2 = match (fk1,fk2) with @@ -1154,10 +1154,6 @@ let match_notation_constr u c (metas,pat) = metas ([],[],[]) (* Matching cases pattern *) -let add_patterns_for_params ind l = - let mib,_ = Global.lookup_inductive ind in - let nparams = mib.Declarations.mind_nparams in - Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v = try @@ -1187,10 +1183,11 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 = | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[]) | PatVar Anonymous, NHole _ -> sigma,(0,[]) | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> - sigma,(0,add_patterns_for_params (fst r1) largs) + let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in + sigma,(0,l) | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) when eq_constructor r1 r2 -> - let l1 = add_patterns_for_params (fst r1) args1 in + let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in let le2 = List.length l2 in if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1 then |