diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 179 | ||||
| -rw-r--r-- | interp/constrextern.mli | 20 | ||||
| -rw-r--r-- | interp/constrintern.ml | 51 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 9 |
4 files changed, 200 insertions, 59 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 19ca8d50b5..f0ee1d58a6 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 *) @@ -288,17 +404,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 +414,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 +428,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 +506,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 +522,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 @@ -888,7 +993,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 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 6f17324a19..3d484a02da 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -963,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 @@ -1200,7 +1239,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 = @@ -1355,9 +1394,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."); @@ -1418,7 +1457,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 := @@ -1427,7 +1466,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 diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 08b9fbe8ec..33b93606ec 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -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 |