Skip to content

Local rewrite rules #21920

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
yannl35133 wants to merge 7 commits into
base: master
Choose a base branch
from
Open

Local rewrite rules #21920

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
cf765f0
Add freeze functions to QState
yannl35133 Jul 25, 2024
34d9044
New representation for patterns (no parsing)
yannl35133 Apr 13, 2026
42546fd
Typechecker for rewrite rules
yannl35133 Apr 13, 2026
bfbaf32
Documentation
yannl35133 Jul 26, 2024
008c029
overlay
yannl35133 Apr 30, 2026
8079fe5
Add pattern term to rewrite rule record
yannl35133 Apr 14, 2026
2abd8ed
Allow subtyping for rewrite rules
yannl35133 May 19, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
106 changes: 7 additions & 99 deletions checker/mod_checking.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,108 +122,16 @@ let check_constant_declaration env opac kn cb opacify =
in
env, opac

let check_quality_mask env qmask lincheck =
let open Sorts.Quality in
match qmask with
| PQConstant QSProp -> if Environ.sprop_allowed env then lincheck else Type_errors.error_not_allowed_sprop env
| PQConstant (QProp | QType) | PQGlobal _ -> lincheck
| PQVar qio -> Partial_subst.maybe_add_quality qio () lincheck

let check_instance_mask env udecl umask lincheck =
match udecl, umask with
| Monomorphic, ([||], [||]) -> lincheck
| Polymorphic uctx, (qmask, umask) ->
let lincheck = Array.fold_left_i (fun i lincheck mask -> check_quality_mask env mask lincheck) lincheck qmask in
let lincheck = Array.fold_left_i (fun i lincheck mask -> Partial_subst.maybe_add_univ mask () lincheck) lincheck umask in
if (Array.length qmask, Array.length umask) <> UVars.AbstractContext.size uctx then CErrors.anomaly Pp.(str "Bad univ mask length.");
lincheck
| _ -> CErrors.anomaly Pp.(str "Bad univ mask length.")

let rec get_holes_profiles env nargs ndecls lincheck el =
List.fold_left (get_holes_profiles_elim env nargs ndecls) lincheck el

and get_holes_profiles_elim env nargs ndecls lincheck = function
| PEApp args -> Array.fold_left (get_holes_profiles_parg env nargs ndecls) lincheck args
| PECase (ind, ret, brs) ->
let mib, mip = Inductive.lookup_mind_specif env ind in
let lincheck = get_holes_profiles_parg env (nargs + mip.mind_nrealargs + 1) (ndecls + mip.mind_nrealdecls + 1) lincheck ret in
Array.fold_left3 (fun lincheck nargs_b ndecls_b -> get_holes_profiles_parg env (nargs + nargs_b) (ndecls + ndecls_b) lincheck) lincheck mip.mind_consnrealargs mip.mind_consnrealdecls brs
| PEProj proj ->
let () = lookup_projection (Projection.make proj false) env |> ignore in
lincheck

and get_holes_profiles_headelim env nargs ndecls lincheck (h, el) =
let lincheck = get_holes_profiles_head env nargs ndecls lincheck h in
get_holes_profiles env nargs ndecls lincheck el

and get_holes_profiles_parg env nargs ndecls lincheck = function
| EHoleIgnored -> lincheck
| EHole i -> Partial_subst.add_term i nargs lincheck
| ERigid hel ->
get_holes_profiles_headelim env nargs ndecls lincheck hel

and get_holes_profiles_head env nargs ndecls lincheck = function
| PHRel n -> if n <= ndecls then lincheck else Type_errors.error_unbound_rel env n
| PHSymbol (c, u) ->
let cb = lookup_constant c env in
check_instance_mask env cb.const_universes u lincheck
| PHConstr (c, u) ->
let (mib, _) = Inductive.lookup_mind_specif env (inductive_of_constructor c) in
check_instance_mask env mib.mind_universes u lincheck
| PHInd (ind, u) ->
let (mib, _) = Inductive.lookup_mind_specif env ind in
check_instance_mask env mib.mind_universes u lincheck
| PHInt _ | PHFloat _ | PHString _ -> lincheck
| PHSort PSSProp -> if Environ.sprop_allowed env then lincheck else Type_errors.error_not_allowed_sprop env
| PHSort PSGlobal (_, io)
| PHSort PSType io -> Partial_subst.maybe_add_univ io () lincheck
| PHSort PSQSort (qio, uio) ->
lincheck
|> Partial_subst.maybe_add_quality qio ()
|> Partial_subst.maybe_add_univ uio ()
| PHSort _ -> lincheck
| PHLambda (tys, bod) ->
let lincheck = Array.fold_left_i (fun i -> get_holes_profiles_parg env (nargs + i) (ndecls + i)) lincheck tys in
let lincheck = get_holes_profiles_headelim env (nargs + Array.length tys) (ndecls + Array.length tys) lincheck bod in
lincheck
| PHProd (tys, bod) ->
let lincheck = Array.fold_left_i (fun i -> get_holes_profiles_parg env (nargs + i) (ndecls + i)) lincheck tys in
let lincheck = get_holes_profiles_parg env (nargs + Array.length tys) (ndecls + Array.length tys) lincheck bod in
lincheck

let check_rhs env holes_profile rhs =
let rec check i c = match Constr.kind c with
| App (f, args) when Constr.isRel f ->
let n = Constr.destRel f in
if n <= i then () else
if n - i > Array.length holes_profile then CErrors.anomaly Pp.(str "Malformed right-hand-side substitution site");
let d = holes_profile.(n-i-1) in
if Array.length args >= d then () else CErrors.anomaly Pp.(str "Malformed right-hand-side substitution site")
| Rel n when n > i ->
if n - i > Array.length holes_profile then CErrors.anomaly Pp.(str "Malformed right-hand-side substitution site");
let d = holes_profile.(n-i-1) in
if d = 0 then () else CErrors.anomaly Pp.(str "Malformed right-hand-side substitution site")
| _ -> Constr.iter_with_binders succ check i c
in
check 0 rhs

let check_rewrite_rule env lab i (symb, rule) =
Flags.if_verbose Feedback.msg_notice (str " checking rule:" ++ Id.print lab ++ str"#" ++ Pp.int i);
let { nvars; lhs_pat; rhs } = rule in
let symb_cb = Environ.lookup_constant symb env in
let () =
match symb_cb.const_body with Symbol _ -> ()
| _ -> ignore @@ invalid_arg "Rule defined on non-symbol"
in
let lincheck = Partial_subst.make nvars in
let lincheck = check_instance_mask env symb_cb.const_universes (fst lhs_pat) lincheck in
let lincheck = get_holes_profiles env 0 0 lincheck (snd lhs_pat) in
let holes_profile, _, _ = Partial_subst.to_arrays lincheck in
let () = check_rhs env holes_profile rhs in
let check_rewrite_rule env lab i rule =
let () = CErrors.user_err Pp.(str "Checker cannot verify code using rewrite rules.") in
(* TODO: Implementation *)

()

let check_rewrite_rules_body env lab rrb =
List.iteri (check_rewrite_rule env lab) rrb.rewrules_rules
Flags.if_verbose Feedback.msg_notice (str " checking rules:" ++ Id.print lab);
List.iter2 (check_rewrite_rule env lab) rrb.rewrules_rules rrb.rewrules_machine

(** {6 Checking modules } *)

Expand Down Expand Up @@ -340,7 +248,7 @@ and check_structure_field env opac mp lab res opacify = function
add_modtype mp mty env, opac
| SFBrules rrb ->
check_rewrite_rules_body env lab rrb;
Environ.add_rewrite_rules rrb.rewrules_rules env, opac
Environ.add_rewrite_rules rrb.rewrules_machine env, opac

and check_signature env opac sign mp_mse res opacify = match sign with
| MoreFunctor (arg_id, mtb, body) ->
Expand Down
91 changes: 70 additions & 21 deletions checker/values.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -217,7 +217,8 @@ let v_cstrs =
let v_variance = v_enum "variance" 3

let v_instance = v_annot_c ("instance", v_pair (v_array v_quality) (v_array v_level))
let v_abs_context = v_tuple "abstract_universe_context" [|v_pair (v_array v_name) (v_array v_name); v_cstrs|]
let v_bound_names = v_pair (v_array v_name) (v_array v_name)
let v_abs_context = v_tuple "abstract_universe_context" [|v_bound_names; v_cstrs|]
let v_univ_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_univ_cstrs|]

(** kernel/term *)
Expand Down Expand Up @@ -245,6 +246,15 @@ let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
let v_uint63 =
if Sys.word_size == 64 then v_int else v_int64

let v_evar = v_int

let v_slist v_arg = fix (fun v_slist ->
v_sum "slist" 1
[|[|v_arg; v_slist|];
[|v_int; v_slist|]|])

let v_evar_existential v_constr = v_pair v_evar (v_slist v_constr)

let v_constr =
fix (fun v_constr ->
let v_prec =
Expand All @@ -260,7 +270,7 @@ let v_case_return = v_tuple_c ("case_return", [|v_tuple_c ("case_return'", [|v_a
[|v_int|]; (* Rel *)
[|v_id|]; (* Var *)
[|v_fail "Meta"|]; (* Meta *)
[|v_fail "Evar"|]; (* Evar *)
[|v_evar_existential v_constr|]; (* Evar *)
[|v_sort|]; (* Sort *)
[|v_constr;v_cast;v_constr|]; (* Cast *)
[|v_binder_annot v_name;v_constr;v_constr|]; (* Prod *)
Expand Down Expand Up @@ -494,37 +504,72 @@ let v_retro_action =
let v_retroknowledge =
v_list v_retro_action

let v_puniv = v_opt v_int

let v_pqvar = v_opt v_int
let v_quality_pattern = v_sum "quality_pattern" 0 [|
let v_quality_pattern v_pqvar = v_sum "quality_pattern" 0 [|
[|v_pqvar|];
[|v_constant_quality|];
[|v_qglobal|];
|]

let v_instance_mask = v_pair (v_array v_quality_pattern) (v_array v_puniv)
let v_instance_mask v_pqvar v_puniv = v_pair (v_array (v_quality_pattern v_pqvar)) (v_array v_puniv)

let v_sort_pattern = v_sum_c ("sort_pattern", 3,
let v_sort_pattern v_pqvar v_puniv = v_sum_c ("sort_pattern", 3,
[|[|v_puniv|]; (* PSType *)
[|v_qglobal; v_puniv|]; (* PSGlobal *)
[|v_pqvar; v_puniv|]; (* PSQSort *)
|])

let v_pattern =
fix (fun v_pattern ->

let v_argpat = v_sum_c ("arg_pattern", 0,
[|[|v_int|]; (* PVar *)
[|v_pattern|]; (* Pat *)
|])
in
let v_annotated_argpat = v_tuple_c ("*", [|v_array v_name; v_argpat|]) in

v_sum_c ("pattern", 0,
[|[|v_int|]; (* PRel *)
[|v_sort_pattern v_int v_int|]; (* PSort *)
[|v_cst; v_instance_mask v_int v_int|]; (* PSymbol *)
[|v_ind; v_instance_mask v_int v_int|]; (* PInd *)
[|v_cons; v_instance_mask v_int v_int|]; (* PConstr *)
[|v_uint63|]; (* PInt *)
[|v_float64|]; (* PFloat *)
[|v_string|]; (* PString *)
[|v_name; v_argpat; v_pattern|]; (* PLambda *)
[|v_name; v_argpat; v_argpat|]; (* PProd *)
[|v_pattern; v_argpat |]; (* PApp *)
[|v_pattern; v_ind; v_annotated_argpat; v_array v_annotated_argpat |]; (* PCase *)
[|v_pattern; v_proj|]; (* PProj *)
|]))

let v_rewrule = v_tuple "rewrite_rule"
[|v_bound_names;(* rr_uctx *)
v_array v_name; (* rr_evars *)
v_map v_evar v_int; (* esubst *)
v_pattern; (* pattern *)
v_constr; (* pat_term *)
v_constr|] (* replacement *)

let v_puniv = v_opt v_int

let v_pqvar = v_opt v_int

let [_v_hpattern;v_elimination;_v_head_elim;_v_patarg] : _ Vector.t =
mfix [();();();()] (fun [v_hpattern;v_elimination;v_head_elim;v_patarg] ->
let v_hpattern =
v_sum_c ("head_pattern", 0,
[|[|v_int|]; (* PHRel *)
[|v_sort_pattern|]; (* PHSort *)
[|v_cst; v_instance_mask|]; (* PHSymbol *)
[|v_ind; v_instance_mask|]; (* PHInd *)
[|v_cons; v_instance_mask|]; (* PHConstr *)
[|v_uint63|]; (* PHInt *)
[|v_float64|]; (* PHFloat *)
[|v_string|]; (* PHString *)
[|v_array v_patarg; v_head_elim|]; (* PHLambda *)
[|v_array v_patarg; v_patarg|]; (* PHProd *)
[|[|v_int|]; (* PHRel *)
[|v_sort_pattern v_pqvar v_puniv|]; (* PHSort *)
[|v_cst; v_instance_mask v_pqvar v_puniv|]; (* PHSymbol *)
[|v_ind; v_instance_mask v_pqvar v_puniv|]; (* PHInd *)
[|v_cons; v_instance_mask v_pqvar v_puniv|]; (* PHConstr *)
[|v_uint63|]; (* PHInt *)
[|v_float64|]; (* PHFloat *)
[|v_string|]; (* PHString *)
[|v_array v_patarg; v_head_elim|]; (* PHLambda *)
[|v_array v_patarg; v_patarg|]; (* PHProd *)
|])

and v_elimination =
Expand All @@ -544,10 +589,14 @@ let [_v_hpattern;v_elimination;_v_head_elim;_v_patarg] : _ Vector.t =
in
[v_hpattern;v_elimination;v_head_elim;v_patarg])

let v_rewrule = v_tuple "rewrite_rule"
[| v_tuple "nvars" [| v_int; v_int; v_int |]; v_pair v_instance_mask (v_list v_elimination); v_constr |]
let v_machine_rewrule = v_tuple "rewrite_rule"
[|v_tuple "nvars" [| v_int; v_int; v_int |];
v_pair (v_instance_mask v_pqvar v_puniv) (v_list v_elimination);
v_constr |]

let v_rrb = v_tuple "rewrite_rules_body"
[| v_list (v_pair v_cst v_rewrule) |]
[|v_list v_rewrule;
v_list (v_pair v_cst v_machine_rewrule) |]

let v_module_with_decl = v_sum "with_declaration" 0 [|
[|v_list v_id; v_mp|];
Expand Down
5 changes: 5 additions & 0 deletions clib/cArray.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -419,6 +419,11 @@ let fold_left2_map_i f e v1 v2 =
let v' = map2_i (fun idx x1 x2 -> let (e,y) = f idx !e' x1 x2 in e' := e; y) v1 v2 in
(!e',v')

let init_fold n f e =
let e' = ref e in
let v' = init n (fun idx -> let (e, v) = f idx !e' in e' := e; v) in
!e', v'

let distinct v =
let visited = Hashtbl.create 23 in
try
Expand Down
3 changes: 3 additions & 0 deletions clib/cArray.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,6 +124,9 @@ val fold_left2_map_i :
val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
(** Same with two arrays, folding on the right *)

val init_fold : int -> (int -> 'acc -> 'acc * 'elt) -> 'acc -> 'acc * 'elt array
(** Initialize an array folding an accumulator *)

val distinct : 'a array -> bool
(** Return [true] if every element of the array is unique (for default
equality). *)
Expand Down
1 change: 1 addition & 0 deletions dev/ci/user-overlays/19290-Yann-Leray-rewrite-rules.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
overlay rocq_lsp https://github.com/Yann-Leray/rocq-lsp rewrite-rules 19290
55 changes: 29 additions & 26 deletions doc/sphinx/addendum/rewrite-rules.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ User-defined rewrite rules
This section describes the extension of Rocq's reduction mechanisms with user-defined rewrite rules,
as a means to extend definitional equality. It should not be confused with the :ref:`rewrite tactic <rewritingexpressions>`
or :ref:`setoid rewriting <generalizedrewriting>` which operate on propositional equality and other relations which are defined in Rocq.
This extension is described in :cite:`Rew24`, following the theory developed in :cite:`TotR21`.

Rewrite rules need to be enabled by passing the option ``-allow-rewrite-rules``
to the Rocq program.
Expand Down Expand Up @@ -49,7 +50,7 @@ Rewrite rules
.. insertprodn rewrite_rule rewrite_rule

.. prodn::
rewrite_rule ::= {? @univ_decl %|- } @rw_pattern => @term
rewrite_rule ::= @rw_pattern => @term

Declares a named block of rewrite rules. The name is declared in the same namespace as constants and inductives.

Expand Down Expand Up @@ -89,7 +90,7 @@ and eliminations (non-base-case constructions for :n:`@rw_pattern`):
| match @rw_pattern {? as @name } {? in @pattern } {? return @rw_pattern_arg } with {? | } {*| @pattern => @rw_pattern_arg } end
rw_head_pattern ::= @ident
| @qualid {? @univ_annot }
| fun {+ ({+ @name } {? : @rw_pattern_arg}) } => @rw_pattern_arg
| fun {+ ({+ @name } {? : @rw_pattern_arg}) } => @rw_pattern
| forall {+ ({+ @name } {? : @rw_pattern_arg}) }, @rw_pattern_arg
rw_pattern_arg ::= ?@name
| _
Expand All @@ -112,7 +113,7 @@ Note that if in the replacement, the context was extended with a variable bearin
this explicit substitution is inferred automatically (like for existential variable instantiations).


.. rocqtop:: all warn
.. rocqtop:: reset all warn

Symbol raise : forall (A : Type), A.
Rewrite Rule raise_nat :=
Expand All @@ -128,45 +129,47 @@ Universe polymorphic rules
--------------------------

Rewrite rules support universe and sort quality polymorphism.
Universe levels and sort quality variables must be declared with the notation :n:`@{q1 q2;u1 u2+|+}`
(the same notation as universe instance declarations);
each variable must appear exactly once in the pattern.
If any universe level isn't bound in the rule,
as is often the case with the level of a pattern variable when it is a type,
you need to make the universe instance extensible (with the final +).
Universe level constraints, as inferred from the pattern, must imply those given,
which in turn must imply the constraints needed for the replacement.
You can make the declared constraints extensible
so all inferred constraints from the left-hand side are used for the replacement.
As with pattern variables, universe levels and sort quality variables
must appear linearly (not more than once each) in the pattern.
Sort qualities and universe levels that appear in the replacement term
must all be either global, or bound in the pattern already.
Currently, unbound qualities and levels are replaced with a default value (Type and Set),
but this leads to subject reduction failures, so use at your own risk.

.. rocqtop:: reset all warn

#[universes(polymorphic)] Symbol raise@{q;u} : forall (A : Type@{q;u}), A.
#[universes(polymorphic)] Symbol raise@{s;l} : forall (A : Type@{s;l}), A.
Rewrite Rule raise_nat :=
@{q;u+|+} |- raise@{q;u} (forall (x : ?A), ?P) => fun (x : ?A) => raise@{q;u} ?P.
raise@{s;l} (forall (x : ?A), ?P) => fun (x : ?A) => raise@{s;l} ?P.

Rewrite rules, type preservation, confluence and termination
------------------------------------------------------------

Currently, rewrite rules do not ensure that types must be preserved.
There is a superficial check that the replacement needs to be typed
against the type inferred for the pattern (for an unclear definition of type of a pattern),
but it is known to be incomplete and only emits a warning if failed.
This then means that reductions using rewrite rules have no reason to preserve well-typedness at all.
The responsibility of ensuring type preservation falls on the user entirely.
The rewrite rules are typechecked so that all substituted replacements
have the type that the term being rewritten has (as described in :cite:`Rew24`).
This means that the check is more stringent than ensuring the two sides have a shared type.
This also means that the pattern is typechecked differently from regular terms,
with an especially more restricted and incomplete unification engine,
which leads to the typechecker refusing some rules that do respect the criterion.
For this reason, the typechecker only emits warnings when it fails to verify the rule,
letting the user take responsibility over the correctness of the rule.

Similarly, neither confluence nor termination are checked by the compiler.
Rocq currently doesn't check for confluence of the rewrite rules,
even though it is required for the invariants that the typechecker uses.
There are plans to add a check using the triangle criterion described in :cite:`TotR21`.

There are future plans to add a check on confluence using the triangle criterion :cite:`TotR21`
and a more complete check on type preservation.
Rocq doesn't check for termination of the rewrite rules either.
Indeed, non-terminating rules are generally fine except for one thing:
the typechecker itself might not always terminate anymore.
Unlike the previous two properties, non-termination cannot cause crashes or anomalies.

Compatibility with the eta laws
-------------------------------

Currently, pattern matching against rewrite rules pattern cannot do eta-expansion or contraction,
which means that it cannot properly match against terms of functional types or primitive records.
As with type preservation, a check is done to test whether this may happen,
but it is not complete (false positives) and thus only emits a warning if failed.
Rocq checks whether this may happen, but the check is imperfect (it reports false positives).
Therefore, the check fails by only emitting a warning, similar to the check for type preservation.

Level of support
----------------
Expand Down
Loading
Loading