From d088d13e9e1fe1928dff7e385433d95a4493c26c Mon Sep 17 00:00:00 2001 From: bodeveix Date: Wed, 1 Jul 2026 14:39:14 +0200 Subject: [PATCH 01/15] cond rules --- src/core/term.ml | 1 + src/core/term.mli | 1 + src/core/tree.ml | 50 ++++++++++++++++++++++++++++++++++------- src/core/tree_type.ml | 7 ++++++ src/export/rawdk.ml | 9 +++++--- src/handle/inductive.ml | 2 +- src/parsing/dkRule.ml | 2 +- src/parsing/lpLexer.ml | 2 ++ src/parsing/lpParser.ml | 16 ++++++++++--- src/parsing/pretty.ml | 9 +++++--- src/parsing/scope.ml | 9 +++++++- src/parsing/syntax.ml | 24 +++++++++++++++----- 12 files changed, 106 insertions(+), 26 deletions(-) diff --git a/src/core/term.ml b/src/core/term.ml index 1791c8b57..875bd70b4 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -214,6 +214,7 @@ and sym = { lhs : term list (** Left hand side (LHS). *) ; names : string array (** Names of pattern variables. *) ; rhs : term (** Right hand side (RHS). *) + ; r_when : (term * term) option (** conditional rule constraint. *) ; arity : int (** Required number of arguments to be applicable. *) ; arities : int array (** Arities of the pattern variables bound in the RHS. *) diff --git a/src/core/term.mli b/src/core/term.mli index 5af110b65..ea56db1b5 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -146,6 +146,7 @@ and rule = { lhs : term list (** Left hand side (LHS). *) ; names : string array (** Names of pattern variables. *) ; rhs : term (** Right hand side (RHS). *) + ; r_when : (term * term) option (** conditional rule constraint. *) ; arity : int (** Required number of arguments to be applicable. *) ; arities : int array (** Arities of the pattern variables bound in the RHS. *) diff --git a/src/core/tree.ml b/src/core/tree.ml index dfbe2190e..6816b3f6f 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -71,6 +71,13 @@ module CP = struct let compare = Stdlib.compare end) + (** Functional sets of pairs of terms. *) + module TSet = Set.Make( + struct + type t = (psym * pvar list) * (psym * pvar list) + let compare = Stdlib.compare + end) + (** A pool of (convertibility and free variable) conditions. *) type t = { variables : pvar IntMap.t @@ -85,17 +92,23 @@ module CP = struct ; fv_conds : int array IntMap.t (** A mapping of [i] to [xs] represents a free variable condition that can only be satisfied if only the free variables of [x] appear in the term - stored at slot [i] in the [vars] array of [Eval.tree_walk]. *) } + stored at slot [i] in the [vars] array of [Eval.tree_walk]. *) + ; eq_conds : TSet.t + (** Set of pairs of terms that should be convertible. *) + } (** [empty] is the condition pool holding no condition. *) let empty : t = { variables = IntMap.empty ; nl_conds = PSet.empty - ; fv_conds = IntMap.empty } + ; fv_conds = IntMap.empty + ; eq_conds = TSet.empty } (** [is_empty pool] tells whether the pool of constraints is empty. *) let is_empty : t -> bool = fun pool -> - PSet.is_empty pool.nl_conds && IntMap.is_empty pool.fv_conds + PSet.is_empty pool.nl_conds + && IntMap.is_empty pool.fv_conds + && TSet.is_empty pool.eq_conds (** [register_nl i (slot,vs) pool] registers the fact that the slot [slot] in the [vars] array correspond to a term stored at index [i] in the @@ -119,6 +132,11 @@ module CP = struct let register_fv : int -> int array -> t -> t = fun i vs pool -> { pool with fv_conds = IntMap.add i vs pool.fv_conds } + (** [register_eq t1 t2 pool] registers a convertibility constraint + between terms [t1] and [t2] in [pool]. *) + let register_eq : (psym * pvar list) -> (psym * pvar list) -> t -> t = fun t1 t2 pool -> + { pool with eq_conds = TSet.add (t1,t2) pool.eq_conds } + (** [constrained_nl i pool] tells whether index [i] in the RHS's environment has already been associated to a variable of the [vars] array. *) let constrained_nl : int -> t -> bool = fun slot pool -> @@ -129,6 +147,8 @@ module CP = struct let is_contained : tree_cond -> t -> bool = fun cond pool -> match cond with | CondNL(i,j) -> PSet.mem (i,j) pool.nl_conds + | CondEQ(t1,t2) -> TSet.mem (t1,t2) pool.eq_conds + || TSet.mem (t2,t1) pool.eq_conds | CondFV(i,x) -> try Array.eq (=) x (IntMap.find i pool.fv_conds) with Not_found -> false @@ -137,6 +157,7 @@ module CP = struct let remove cond pool = match cond with | CondNL(i,j) -> {pool with nl_conds = PSet.remove (i,j) pool.nl_conds} + | CondEQ(t1,t2) -> {pool with eq_conds = TSet.remove (t1,t2) pool.eq_conds} | CondFV(i,xs) -> try let ys = IntMap.find i pool.fv_conds in @@ -161,8 +182,18 @@ module CP = struct | p :: ps -> try Some(export (IntMap.choose p.fv_conds)) with Not_found -> choose_vf ps in + let rec choose_eq pools = + let export (t1,t2) = CondEQ(t1,t2) in + match pools with + | [] -> None + | p :: ps -> try Some(export (TSet.choose p.eq_conds)) + with Not_found -> choose_eq ps + in let res = choose_nl pools in - if res = None then choose_vf pools else res + if res = None then + let res = choose_eq pools in + if res = None then choose_vf pools else res + else res end (** {1 Clause matrix and pattern matching problem} *) @@ -224,6 +255,8 @@ module CM = struct (** Left hand side of a rule. *) ; c_rhs : rule (** Right hand side of a rule, and number of extra variables. *) + ; c_when : (term * term) option + (** convertibility constraint for conditional rules *) ; c_subst : rhs_substit (** Substitution of RHS variables. *) ; xvars_nb : int @@ -290,9 +323,10 @@ module CM = struct (** [of_rules rs] transforms rewriting rules [rs] into a clause matrix. *) let of_rules : rule list -> t = fun rs -> - let r2r ({lhs; xvars_nb; _} as c_rhs) = + let r2r ({lhs; xvars_nb; r_when; _} as c_rhs) = let c_lhs = Array.of_list lhs in - { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb } + let c_when = r_when in + { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb; c_when } in let size = (* Get length of longest rule *) if rs = [] then 0 else @@ -357,7 +391,7 @@ module CM = struct (** [is_exhausted p c] tells whether clause [r] whose terms are at positions in [p] can be applied or not. *) let is_exhausted : arg list -> clause -> bool = - fun positions {c_lhs = lhs ; cond_pool ; _} -> + fun positions {c_lhs = lhs ; cond_pool ; c_when; _} -> let nonl lhs = (* Verify that there are no non linearity constraints in the remaining terms. We must check that there are no constraints in the remaining @@ -384,7 +418,7 @@ module CM = struct in Array.for_all2 check lhs de && nonl lhs in - CP.is_empty cond_pool && (lhs = [||] || ripe lhs) + c_when = None && CP.is_empty cond_pool && (lhs = [||] || ripe lhs) (** [yield m] returns the next operation to carry out on matrix [m], that is, either specialising, solving a constraint or rewriting to a rule. *) diff --git a/src/core/tree_type.ml b/src/core/tree_type.ml index c2d7d17a2..127d69d1e 100644 --- a/src/core/tree_type.ml +++ b/src/core/tree_type.ml @@ -6,6 +6,7 @@ open Common (** {3 Atomic pattern constructor representation} *) type pvar = int * int array +type psym = Path.t * string (** Representation of an atomic pattern constructor. *) module TC = @@ -56,6 +57,8 @@ type tree_cond = | CondFV of pvar (** Are the (indexed) bound variables (which are free at the time of the checking) of the term at the given index in the array? *) + | CondEQ of (psym * pvar list) * (psym * pvar list) + (** user rule condition: are the two terms equivalent *) (** {b NOTE} that when performing a [tree_cond.CondFV] check, we are concerned about variables that were bound in the term being reduced @@ -69,6 +72,10 @@ let tree_cond : tree_cond pp = fun ppf tc -> out ppf "Nl(%d[%a],%d[%a])" i (Array.pp int ",") xs j (Array.pp int ",") ys | CondFV(i, _) -> out ppf "Fv(%d)" i + | CondEQ((s1,a1), (s2,a2)) -> + out ppf "Eq(%s(%a),%s(%a))" + (snd s1) (List.pp int ",") (List.map fst a1) + (snd s2) (List.pp int ",") (List.map fst a2) (** Substitution of variables in a RHS. During the filtering process, some subterms of the filtered term may be stored in an array. Let [v] be that diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml index b9b917e67..42f94fb8d 100644 --- a/src/export/rawdk.ml +++ b/src/export/rawdk.ml @@ -135,9 +135,12 @@ let rec remove_wraps ({elt;_} as t) = let rule : p_rule pp = let varset ppf set = List.pp string ", " ppf (StrSet.elements set) in - fun ppf {elt=(l,r);_} -> - out ppf "[%a] %a --> %a.@." - varset (pvars_lhs l) term (remove_wraps l) term r + fun ppf {elt=(l,r,w);_} -> + if w = None then + out ppf "[%a] %a --> %a.@." + varset (pvars_lhs l) term (remove_wraps l) term r + else + fatal None "Cannot translate conditional rules." type modifiers = prop list * expo list * match_strat list * p_modifier_aux list diff --git a/src/handle/inductive.ml b/src/handle/inductive.ml index ff2eaa2bd..3e6d2beb2 100644 --- a/src/handle/inductive.ml +++ b/src/handle/inductive.ml @@ -347,7 +347,7 @@ let iter_rec_rules : let nonrec_dom _ _ next = next in let codom xs rhs _ ts = let cons_arg = P.appl_list (P.iden cons_sym.sym_name) (List.rev xs) in - Pos.make rules_pos (arec ind_sym ts cons_arg, rhs) + Pos.make rules_pos (arec ind_sym ts cons_arg, rhs, None) in fold_cons_type pos ind_pred_map "" ind_sym vs cons_sym inj_var init aux acc_rec_dom rec_dom acc_nonrec_dom nonrec_dom codom diff --git a/src/parsing/dkRule.ml b/src/parsing/dkRule.ml index 09d709a20..65e78eb3f 100644 --- a/src/parsing/dkRule.ml +++ b/src/parsing/dkRule.ml @@ -155,4 +155,4 @@ let to_p_rule : p_dk_rule -> p_rule = fun r -> (* NOTE the computation order is important for setting arities properly. *) let lhs = build [] lhs in let rhs = build [] rhs in - Pos.make r.pos (lhs, rhs) + Pos.make r.pos (lhs, rhs, None) diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml index 21832f264..47acb2380 100644 --- a/src/parsing/lpLexer.ml +++ b/src/parsing/lpLexer.ml @@ -93,6 +93,7 @@ type token = | TYPE_TERM | UNIF_RULE | VERBOSE + | WHEN | WHY3 | WITH @@ -298,6 +299,7 @@ let rec token ~allow_rocq_syntax lb = | "TYPE" -> TYPE_TERM | "unif_rule" -> UNIF_RULE | "verbose" -> VERBOSE + | "when" -> WHEN | "why3" -> WHY3 | "with" -> WITH diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index 911372e3d..cdfc6d433 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -115,6 +115,7 @@ let string_of_token = function | UNIF_RULE -> "unif_rule" | VBAR -> "|" | VERBOSE -> "verbose" + | WHEN -> "when" | WHY3 -> "why3" | WITH -> "with" @@ -531,7 +532,7 @@ let rec command pos1 (p_sym_mod:p_modifier list) (lb:'token lexbuf) : let (en, es) = List.(hd es, tl es) in let cat e es = P.appl (P.appl cons e) es in let rhs = List.fold_right cat es en in - let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs) in + let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs, None) in extend_pos lb (*__FUNCTION__*) pos1 (P_unif_rule(r)) | COERCE_RULE -> if p_sym_mod <> [] then expected lb "" [SYMBOL]; (*or modifiers*) @@ -686,13 +687,22 @@ and notation (lb:'token lexbuf): string Term.notation = | _ -> expected lb "" [INFIX;POSTFIX;PREFIX;QUANTIFIER] -and rule (lb:'token lexbuf): (p_term * p_term) loc = +and rule (lb:'token lexbuf): (p_term * p_term * (p_term * p_term) option) loc = if log_enabled() then log "%s" __FUNCTION__; let pos1 = current_pos lb in let l = term lb in + let w = + if (current_token lb == WHEN) then begin + consume WHEN lb; + let t1 = term lb in + consume EQUIV lb; + let t2 = term lb in + Some (t1,t2) + end + else None in consume HOOK_ARROW lb; let r = term lb in - extend_pos lb (*__FUNCTION__*) pos1 (l, r) + extend_pos lb (*__FUNCTION__*) pos1 (l, r, w) and equation (lb:'token lexbuf): p_term * p_term = if log_enabled() then log "%s" __FUNCTION__; diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml index 759eb0bfd..a313de2ef 100644 --- a/src/parsing/pretty.ml +++ b/src/parsing/pretty.ml @@ -187,8 +187,11 @@ and params_list : p_params list pp = fun ppf -> and typ : p_term option pp = fun ppf t -> Option.iter (out ppf "@ : %a" term) t -let rule : string -> p_rule pp = fun kw ppf {elt=(l,r);_} -> - out ppf "%s %a ↪ %a" kw term l term r +let rule : string -> p_rule pp = fun kw ppf {elt=(l,r,w);_} -> + match w with + | None -> out ppf "%s %a ↪ %a" kw term l term r + | Some (t1,t2) -> out ppf "%s %a when %a ≡ %a ↪ %a" + kw term l term t1 term t2 term r let inductive : string -> p_inductive pp = let cons ppf (id,a) = out ppf "@,| %a : %a" ident id term a in @@ -214,7 +217,7 @@ let rec unpack : p_term -> (p_term * p_term) list = fun eqs -> else assert false | _ -> assert false -let unif_rule : p_rule pp = fun ppf {elt=(l,r);_} -> +let unif_rule : p_rule pp = fun ppf {elt=(l,r,_);_} -> let lhs = match Syntax.p_get_args l with | (_, [t; u]) -> (t, u) diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index def6973a5..7d1c82c3a 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -547,13 +547,19 @@ let patt_vars : p_term -> (string * int) list * string list = let scope_rule : ?find_sym:find_sym -> bool -> sig_state -> p_rule -> sym_rule = fun ?(find_sym=Sig_state.find_sym) ur ss - { elt = (p_lhs, p_rhs); pos = rule_pos} -> + { elt = (p_lhs, p_rhs, p_when); pos = rule_pos} -> (* Compute the set of pattern variables on both sides. *) let (pvs_lhs, nl) = patt_vars p_lhs in (* NOTE to reject non-left-linear rules check [nl = []] here. *) let (pvs_rhs, _ ) = patt_vars p_rhs in (* Check that pattern variables of RHS that are in the LHS have the right arity. *) + let pvs_when = + match p_when with + | None -> [] + | Some (t1,t2) -> + let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in + p1 @ p2 in let check_arity (m,i) = try let j = List.assoc m pvs_lhs in @@ -561,6 +567,7 @@ let scope_rule : with Not_found -> () in List.iter check_arity pvs_rhs; + List.iter check_arity pvs_when; (* [get_root t] returns the symbol at the root of the p_term [t]. *) let rec get_root t = get_root_after_pratt (Pratt.parse ~find_sym ss [] t) and get_root_after_pratt t = diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index 18bef499a..6cbcada8f 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -134,7 +134,7 @@ let rec pvars_lhs : p_term -> StrSet.t = fun {elt;pos} -> -> pvars_lhs u (** Parser-level rewriting rule representation. *) -type p_rule_aux = p_term * p_term +type p_rule_aux = p_term * p_term * (p_term * p_term) option type p_rule = p_rule_aux loc (** Parser-level inductive type representation. *) @@ -182,7 +182,8 @@ module P = struct let abst_list : p_ident option list -> p_term -> p_term = fun idopts t -> List.fold_right abst idopts t - let rule : p_term -> p_term -> p_rule = fun l r -> Pos.none (l,r) + let rule : p_term -> p_term -> (p_term * p_term) option -> p_rule = + fun l r w -> Pos.none (l,r,w) end (** Rewrite patterns as in Coq/SSReflect. See "A Small Scale @@ -402,8 +403,13 @@ and eq_p_params : p_params eq = fun (i1,ao1,b1) (i2,ao2,b2) -> List.eq (Option.eq eq_p_ident) i1 i2 && Option.eq eq_p_term ao1 ao2 && b1 = b2 -let eq_p_rule : p_rule eq = fun {elt=(l1,r1);_} {elt=(l2,r2);_} -> - eq_p_term l1 l2 && eq_p_term r1 r2 +let pair_eq: 'a eq -> 'b eq -> ('a * 'b) eq = fun eq1 eq2 (x1,y1) (x2,y2) -> + eq1 x1 x2 && eq2 y1 y2 + +let eq_p_rule : p_rule eq = fun {elt=(l1,r1,w1);_} {elt=(l2,r2,w2);_} -> + eq_p_term l1 l2 + && eq_p_term r1 r2 + && Option.eq (pair_eq eq_p_term eq_p_term) w1 w2 let eq_p_inductive : p_inductive eq = let eq_cons (i1,t1) (i2,t2) = eq_p_ident i1 i2 && eq_p_term t1 t2 in @@ -616,8 +622,14 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a = let fold_term : 'a -> p_term -> 'a = fold_term_vars StrSet.empty in - let fold_rule : 'a -> p_rule -> 'a = fun a {elt=(l,r);_} -> - fold_term (fold_term a l) r + let fold_when : 'a -> (p_term * p_term) option -> 'a = fun a w -> + match w with + | Some (t1,t2) -> fold_term (fold_term a t1) t2 + | None -> a + in + + let fold_rule : 'a -> p_rule -> 'a = fun a {elt=(l,r,w);_} -> + fold_when (fold_term (fold_term a l) r) w in let fold_rwpatt_vars : StrSet.t -> 'a -> p_rwpatt -> 'a = fun vs a p -> From e8b0b985fc96c1bd95c731a605471b9b4d1673d9 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Wed, 1 Jul 2026 21:51:08 +0200 Subject: [PATCH 02/15] conditional rules --- src/core/coercion.ml | 2 +- src/core/eval.ml | 15 +++++++++++++ src/core/term.ml | 2 +- src/core/term.mli | 2 +- src/core/tree.ml | 45 ++++++++++++++++++++++++++++++++------- src/parsing/scope.ml | 16 +++++++++++++- src/tool/lcr.ml | 4 ++-- src/tool/tree_graphviz.ml | 4 ++++ 8 files changed, 76 insertions(+), 14 deletions(-) diff --git a/src/core/coercion.ml b/src/core/coercion.ml index 3faf8bb5b..8f9a7cffe 100644 --- a/src/core/coercion.ml +++ b/src/core/coercion.ml @@ -15,6 +15,6 @@ let _ = and t = mk_Patt (Some 1, "t", [||]) in let lhs = [a;a;t] and arities = [|0;0|] and names = [|"A";"t"|] in { lhs; names; rhs=t; arity=3; arities; vars_nb=2; xvars_nb = 0; - rule_pos = None } + rule_pos = None; r_when = None } in Sign.add_rule Ghost.sign (coerce, rule) diff --git a/src/core/eval.ml b/src/core/eval.ml index 0eaf29c56..083c29309 100644 --- a/src/core/eval.ml +++ b/src/core/eval.ml @@ -342,6 +342,21 @@ and tree_walk : config -> sym -> stack -> (term * stack) option = let vi = Array.map (fun id -> mk_Vari (var id)) vi in let tj = msubst bj vi in if eq_modulo whnf cfg vars.(i) tj then ok else fail + | CondEQ(((p1,o1) as op1,a1), ((p2,o2) as op2,a2)) -> + let v1 = List.map (fun (i,_) -> vars.(i)) a1 in + let v2 = List.map (fun (i,_) -> vars.(i)) a2 in + if Logger.log_enabled() then + log_rew "%aCondEQ(%s[%a],%s[%a]) : %s(%a) == %s(%a)" + D.depth !depth + (snd op1) (List.pp D.int ",") (List.map fst a1) + (snd op2) (List.pp D.int ",") (List.map fst a2) + (snd op1) (List.pp Raw.term ",") v1 + (snd op2) (List.pp Raw.term ",") v2; + let s1 = Sign.find_qualified p1 o1 in + let s2 = Sign.find_qualified p2 o2 in + let t1 = add_args (mk_Symb s1) v1 in + let t2 = add_args (mk_Symb s2) v2 in + if eq_modulo whnf cfg t1 t2 then ok else fail | CondFV(i,xs) -> let allowed = (* Variables that are allowed in the term. *) diff --git a/src/core/term.ml b/src/core/term.ml index 875bd70b4..0f36c6102 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -214,7 +214,7 @@ and sym = { lhs : term list (** Left hand side (LHS). *) ; names : string array (** Names of pattern variables. *) ; rhs : term (** Right hand side (RHS). *) - ; r_when : (term * term) option (** conditional rule constraint. *) + ; r_when : ((sym * int list) * (sym * int list)) option (** conditional rule constraint. *) ; arity : int (** Required number of arguments to be applicable. *) ; arities : int array (** Arities of the pattern variables bound in the RHS. *) diff --git a/src/core/term.mli b/src/core/term.mli index ea56db1b5..16a5e6925 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -146,7 +146,7 @@ and rule = { lhs : term list (** Left hand side (LHS). *) ; names : string array (** Names of pattern variables. *) ; rhs : term (** Right hand side (RHS). *) - ; r_when : (term * term) option (** conditional rule constraint. *) + ; r_when : ((sym * int list) * (sym * int list)) option (** conditional rule constraint. *) ; arity : int (** Required number of arguments to be applicable. *) ; arities : int array (** Arities of the pattern variables bound in the RHS. *) diff --git a/src/core/tree.ml b/src/core/tree.ml index 6816b3f6f..b71ee05f4 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -71,7 +71,7 @@ module CP = struct let compare = Stdlib.compare end) - (** Functional sets of pairs of terms. *) + (** Functional sets of pairs of flat terms. *) module TSet = Set.Make( struct type t = (psym * pvar list) * (psym * pvar list) @@ -134,8 +134,11 @@ module CP = struct (** [register_eq t1 t2 pool] registers a convertibility constraint between terms [t1] and [t2] in [pool]. *) - let register_eq : (psym * pvar list) -> (psym * pvar list) -> t -> t = fun t1 t2 pool -> - { pool with eq_conds = TSet.add (t1,t2) pool.eq_conds } + let register_eq : (psym * int list) -> (psym * int list) -> t -> t = + fun (s1,a1) (s2,a2) pool -> + let pv1 = List.map (fun i -> IntMap.find i pool.variables) a1 in + let pv2 = List.map (fun i -> IntMap.find i pool.variables) a2 in + { pool with eq_conds = TSet.add ((s1,pv1),(s2,pv2)) pool.eq_conds } (** [constrained_nl i pool] tells whether index [i] in the RHS's environment has already been associated to a variable of the [vars] array. *) @@ -183,10 +186,14 @@ module CP = struct with Not_found -> choose_vf ps in let rec choose_eq pools = - let export (t1,t2) = CondEQ(t1,t2) in + let export vars (((_,a1) as t1), ((_,a2) as t2)) = + if List.for_all (fun (i,_) -> IntMap.mem i vars) a1 + && List.for_all (fun (i,_) -> IntMap.mem i vars) a2 then + CondEQ(t1,t2) + else raise Not_found in match pools with | [] -> None - | p :: ps -> try Some(export (TSet.choose p.eq_conds)) + | p :: ps -> try Some(export p.variables (TSet.choose p.eq_conds)) with Not_found -> choose_eq ps in let res = choose_nl pools in @@ -255,7 +262,7 @@ module CM = struct (** Left hand side of a rule. *) ; c_rhs : rule (** Right hand side of a rule, and number of extra variables. *) - ; c_when : (term * term) option + ; c_when : ((psym * int list) * (psym * int list)) option (** convertibility constraint for conditional rules *) ; c_subst : rhs_substit (** Substitution of RHS variables. *) @@ -325,7 +332,11 @@ module CM = struct let of_rules : rule list -> t = fun rs -> let r2r ({lhs; xvars_nb; r_when; _} as c_rhs) = let c_lhs = Array.of_list lhs in - let c_when = r_when in + let c_when = match r_when with + | None -> None + | Some ((s1,a1),(s2,a2)) -> + Some (((s1.sym_path,s1.sym_name), a1), + ((s2.sym_path,s2.sym_name), a2)) in { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb; c_when } in let size = (* Get length of longest rule *) @@ -516,6 +527,24 @@ module CM = struct CP.register_nl i (mem,vs) cond_pool | None -> cond_pool in + let c_when, cond_pool = + match r.c_rhs.r_when with + | None -> r.c_when, cond_pool + | Some ((op1,a1), (op2,a2)) when + List.for_all (fun i -> IntMap.mem i cond_pool.variables) a1 + && List.for_all (fun i -> IntMap.mem i cond_pool.variables) a2 -> + if Logger.log_enabled () then + log "Registering user constraint on position [%a] \ + %s %a == %s %a" + arg_path a.arg_path + op1.sym_name (List.pp int " ") a1 + op2.sym_name (List.pp int " ") a2; + None, CP.register_eq + ((op1.sym_path,op1.sym_name), a1) + ((op2.sym_path,op2.sym_name), a2) + cond_pool + | _ -> r.c_when, cond_pool + in let c_subst = (* REVIEW: patterns may have slots in the RHS although they are not bound. *) @@ -533,7 +562,7 @@ module CM = struct (mem, (i,vs)) :: r.c_subst | _ -> r.c_subst in - {r with c_subst; cond_pool} + {r with c_subst; cond_pool; c_when} | _ -> r (** [specialize free_vars pat col pos cls] filters and transforms LHS of diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index 7d1c82c3a..5a17e9974 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -630,7 +630,21 @@ let scope_rule : let arity = List.length lhs in let f i = try Hashtbl.find names i with Not_found -> string_of_int i in let names = Array.init vars_nb f in - let r = {lhs; names; rhs; arity; arities; vars_nb; xvars_nb; rule_pos} in + let pw2rw t = + let asPatt t = match unfold t with + | Patt (Some i, _, [||]) -> i + | _ -> fatal rule_pos "arguments should be patterns in condition [%a]." + term t in + let t = scope ~find_sym 0 mode ss Env.empty t in + match get_args t with + Symb s, args -> (s, List.map asPatt args) + | _ -> fatal rule_pos "function should be a global symbol in [%a]." term t + in + let r_when = match p_when with + | None -> None + | Some (t1,t2) -> Some (pw2rw t1, pw2rw t2) in + let r = {lhs; names; rhs; arity; arities; vars_nb; xvars_nb; + rule_pos; r_when} in (sym,r) (** [scope_pattern ss env t] turns a parser-level term [t] into an actual term diff --git a/src/tool/lcr.ml b/src/tool/lcr.ml index 42719d12b..d70323b97 100644 --- a/src/tool/lcr.ml +++ b/src/tool/lcr.ml @@ -55,7 +55,7 @@ let is_definable : sym -> bool = fun s -> (** [rule_of_def s d] creates the rule [s --> d]. *) let rule_of_def : sym -> term -> rule = fun s rhs -> {lhs=[]; names=[||]; rhs; arity=0; arities=[||]; vars_nb=0; xvars_nb=0; - rule_pos=s.sym_pos} + rule_pos=s.sym_pos; r_when = None} (** [replace t p u] replaces the subterm of [t] at position [p] by [u]. *) let replace : term -> subterm_pos -> term -> term = fun t p u -> @@ -457,7 +457,7 @@ let typability_constraints : Pos.popt -> term -> subs option = fun pos t -> match get_args_len l with | Symb s, lhs, arity -> let r = {lhs; names=[||]; rhs; arity; arities=[||]; vars_nb=0; - xvars_nb=0; rule_pos=Some(new_rule_id())} in + xvars_nb=0; rule_pos=Some(new_rule_id()); r_when = None} in Some (s,r) | _ -> None in diff --git a/src/tool/tree_graphviz.ml b/src/tool/tree_graphviz.ml index 3097edf56..4af09c70c 100644 --- a/src/tool/tree_graphviz.ml +++ b/src/tool/tree_graphviz.ml @@ -46,6 +46,10 @@ let tree_to_dot : Format.formatter -> _ dtree -> unit = fun ppf dtree -> | CondNL((i,vi), (j,vj)) -> out ppf "%d[%a] ≡ %d[%a]" i ar vi j ar vj | CondFV(i,vs) -> out ppf "%a ⊆ FV(%d)" ar vs i + | CondEQ(((_p1,s1),a1), ((_p2,s2),a2)) -> + out ppf "%s[%a] ≡ %s[%a]" + s1 (List.pp int ",") (List.map fst a1) + s2 (List.pp int ",") (List.map fst a2) in let node_count = ref 0 in (* [write_tree n u v] writes tree [v] obtained from tree number [n] with a From 38ea2e75aaafb2590cbf80bff9ee09a528c6e474 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Wed, 1 Jul 2026 22:07:42 +0200 Subject: [PATCH 03/15] sanity_checks --- src/core/eval.ml | 2 +- src/core/term.ml | 3 ++- src/core/term.mli | 7 ++++--- src/core/tree.ml | 15 ++++++++------- src/parsing/lpParser.ml | 5 +++-- src/parsing/scope.ml | 2 +- 6 files changed, 19 insertions(+), 15 deletions(-) diff --git a/src/core/eval.ml b/src/core/eval.ml index 083c29309..e154756e2 100644 --- a/src/core/eval.ml +++ b/src/core/eval.ml @@ -350,7 +350,7 @@ and tree_walk : config -> sym -> stack -> (term * stack) option = D.depth !depth (snd op1) (List.pp D.int ",") (List.map fst a1) (snd op2) (List.pp D.int ",") (List.map fst a2) - (snd op1) (List.pp Raw.term ",") v1 + (snd op1) (List.pp Raw.term ",") v1 (snd op2) (List.pp Raw.term ",") v2; let s1 = Sign.find_qualified p1 o1 in let s2 = Sign.find_qualified p2 o2 in diff --git a/src/core/term.ml b/src/core/term.ml index 0f36c6102..76614350a 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -214,7 +214,8 @@ and sym = { lhs : term list (** Left hand side (LHS). *) ; names : string array (** Names of pattern variables. *) ; rhs : term (** Right hand side (RHS). *) - ; r_when : ((sym * int list) * (sym * int list)) option (** conditional rule constraint. *) + ; r_when : ((sym * int list) * (sym * int list)) option + (** conditional rule constraint. *) ; arity : int (** Required number of arguments to be applicable. *) ; arities : int array (** Arities of the pattern variables bound in the RHS. *) diff --git a/src/core/term.mli b/src/core/term.mli index 16a5e6925..086e51abe 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -146,7 +146,8 @@ and rule = { lhs : term list (** Left hand side (LHS). *) ; names : string array (** Names of pattern variables. *) ; rhs : term (** Right hand side (RHS). *) - ; r_when : ((sym * int list) * (sym * int list)) option (** conditional rule constraint. *) + ; r_when : ((sym * int list) * (sym * int list)) option + (** conditional rule constraint. *) ; arity : int (** Required number of arguments to be applicable. *) ; arities : int array (** Arities of the pattern variables bound in the RHS. *) @@ -176,8 +177,8 @@ and rule = concrete syntax) are represented in the same way, and with a unique name (in the rule) that is generated automatically. - Then, the term [f t u v w] matches the LHS with a substitution represented - by an array of terms [a] of length 3 if we + Then, the term [f t u v w] matches the LHS with a substitution + represented by an array of terms [a] of length 3 if we have [a.(0) = t], [a.(1) = u], [a.(1) = v] and [a.(2) = w]. {b TODO} memorising [w] in the substitution is sub-optimal. In practice, diff --git a/src/core/tree.ml b/src/core/tree.ml index b71ee05f4..7245b291a 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -134,12 +134,12 @@ module CP = struct (** [register_eq t1 t2 pool] registers a convertibility constraint between terms [t1] and [t2] in [pool]. *) - let register_eq : (psym * int list) -> (psym * int list) -> t -> t = + let register_eq : (psym * int list) -> (psym * int list) -> t -> t = fun (s1,a1) (s2,a2) pool -> let pv1 = List.map (fun i -> IntMap.find i pool.variables) a1 in let pv2 = List.map (fun i -> IntMap.find i pool.variables) a2 in { pool with eq_conds = TSet.add ((s1,pv1),(s2,pv2)) pool.eq_conds } - + (** [constrained_nl i pool] tells whether index [i] in the RHS's environment has already been associated to a variable of the [vars] array. *) let constrained_nl : int -> t -> bool = fun slot pool -> @@ -160,7 +160,7 @@ module CP = struct let remove cond pool = match cond with | CondNL(i,j) -> {pool with nl_conds = PSet.remove (i,j) pool.nl_conds} - | CondEQ(t1,t2) -> {pool with eq_conds = TSet.remove (t1,t2) pool.eq_conds} + | CondEQ(t,u) -> {pool with eq_conds = TSet.remove (t,u) pool.eq_conds} | CondFV(i,xs) -> try let ys = IntMap.find i pool.fv_conds in @@ -186,10 +186,10 @@ module CP = struct with Not_found -> choose_vf ps in let rec choose_eq pools = - let export vars (((_,a1) as t1), ((_,a2) as t2)) = + let export vars (((_,a1) as t1), ((_,a2) as t2)) = if List.for_all (fun (i,_) -> IntMap.mem i vars) a1 && List.for_all (fun (i,_) -> IntMap.mem i vars) a2 then - CondEQ(t1,t2) + CondEQ(t1,t2) else raise Not_found in match pools with | [] -> None @@ -528,11 +528,12 @@ module CM = struct | None -> cond_pool in let c_when, cond_pool = + let vars = cond_pool.variables in match r.c_rhs.r_when with | None -> r.c_when, cond_pool | Some ((op1,a1), (op2,a2)) when - List.for_all (fun i -> IntMap.mem i cond_pool.variables) a1 - && List.for_all (fun i -> IntMap.mem i cond_pool.variables) a2 -> + List.for_all (fun i -> IntMap.mem i vars) a1 + && List.for_all (fun i -> IntMap.mem i vars) a2 -> if Logger.log_enabled () then log "Registering user constraint on position [%a] \ %s %a == %s %a" diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index 6c7f6092c..b524f207e 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -688,7 +688,8 @@ and notation (lb:'token lexbuf): string Term.notation = | _ -> expected lb "" [INFIX;POSTFIX;PREFIX;QUANTIFIER] -and rule (lb:'token lexbuf): (p_term * p_term * (p_term * p_term) option) loc = +and rule (lb:'token lexbuf): + (p_term * p_term * (p_term * p_term) option) loc = if log_enabled() then log "%s" __FUNCTION__; let pos1 = current_pos lb in let l = term lb in @@ -700,7 +701,7 @@ and rule (lb:'token lexbuf): (p_term * p_term * (p_term * p_term) option) loc = let t2 = term lb in Some (t1,t2) end - else None in + else None in consume HOOK_ARROW lb; let r = term lb in extend_pos lb (*__FUNCTION__*) pos1 (l, r, w) diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index 5a17e9974..e544a98a2 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -639,7 +639,7 @@ let scope_rule : match get_args t with Symb s, args -> (s, List.map asPatt args) | _ -> fatal rule_pos "function should be a global symbol in [%a]." term t - in + in let r_when = match p_when with | None -> None | Some (t1,t2) -> Some (pw2rw t1, pw2rw t2) in From dfc7053bb2bd5641fe3993820472120bb81cca5d Mon Sep 17 00:00:00 2001 From: bodeveix Date: Thu, 2 Jul 2026 21:32:08 +0200 Subject: [PATCH 04/15] editors --- CHANGES.md | 1 + doc/lambdapi.bnf | 1 + editors/emacs/lambdapi-smie.el | 6 ++++-- editors/emacs/lambdapi-vars.el | 1 + editors/vim/syntax/lambdapi.vim | 2 ++ editors/vscode/syntaxes/lp.tmLanguage.json | 2 +- misc/lambdapi.tex | 2 +- tests/OK/cond_rules.lp | 18 ++++++++++++++++++ 8 files changed, 29 insertions(+), 4 deletions(-) create mode 100644 tests/OK/cond_rules.lp diff --git a/CHANGES.md b/CHANGES.md index 88f13201b..d8fc07916 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -22,6 +22,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/). - Tactic `#print` to print a symbol or the current goal. - Export to Lean. - Tactic `all_hyps t` calls parameterized tactic term t on all hypotheses ignoring failing calls. +- Conditional rules `l when t1 ≡ t2 ↪ r` ### Changed diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf index 57b19e549..e3f0444ff 100644 --- a/doc/lambdapi.bnf +++ b/doc/lambdapi.bnf @@ -33,6 +33,7 @@ ::= * ":" ::= "↪" + | when ≡ "↪" ::= "↪" "[" (";" )* "]" diff --git a/editors/emacs/lambdapi-smie.el b/editors/emacs/lambdapi-smie.el index 2b9ad2b30..6d42f46a6 100644 --- a/editors/emacs/lambdapi-smie.el +++ b/editors/emacs/lambdapi-smie.el @@ -56,7 +56,8 @@ "rule" "symbol" "unif_rule" - "verbose") + "verbose" + "when") lambdapi--queries) "Commands at top level.") @@ -142,7 +143,8 @@ Indent by `lambdapi-indent-basic' in proofs, and 0 otherwise." (symdec ("symbol" args ":" sterm)) (indcons (args ":" sterm) ("|" args ":" sterm)) (inddec (inddec "with" args ":" sterm "≔" indcons)) - (rules (rules "with" sterm "↪" sterm)) + (rules (rules "with" sterm "↪" sterm) + (rules "with" sterm "when" sterm "≡" sterm "↪" sterm)) (command ("begin" prfcontent "abort" ";") ("begin" prfcontent "admitted" ";") diff --git a/editors/emacs/lambdapi-vars.el b/editors/emacs/lambdapi-vars.el index d5f54afdb..5271515d3 100644 --- a/editors/emacs/lambdapi-vars.el +++ b/editors/emacs/lambdapi-vars.el @@ -47,6 +47,7 @@ "rule" "symbol" "unif_rule" + "when" "with") "Commands that enrich the signature.") diff --git a/editors/vim/syntax/lambdapi.vim b/editors/vim/syntax/lambdapi.vim index 4e485eb42..ebef338c9 100644 --- a/editors/vim/syntax/lambdapi.vim +++ b/editors/vim/syntax/lambdapi.vim @@ -98,6 +98,7 @@ syntax keyword KeywordOK contained type syntax keyword KeywordOK contained TYPE syntax keyword KeywordOK contained unif_rule syntax keyword KeywordOK contained verbose +syntax keyword KeywordOK contained when syntax keyword KeywordOK contained why3 syntax keyword KeywordOK contained with highlight link KeywordOK Keyword @@ -172,6 +173,7 @@ syntax keyword KeywordKO contained type syntax keyword KeywordKO contained TYPE syntax keyword KeywordKO contained unif_rule syntax keyword KeywordKO contained verbose +syntax keyword KeywordKO contained when syntax keyword KeywordKO contained why3 syntax keyword KeywordKO contained with highlight link KeywordKO Error diff --git a/editors/vscode/syntaxes/lp.tmLanguage.json b/editors/vscode/syntaxes/lp.tmLanguage.json index e7a25f740..bbf5d44ff 100644 --- a/editors/vscode/syntaxes/lp.tmLanguage.json +++ b/editors/vscode/syntaxes/lp.tmLanguage.json @@ -45,7 +45,7 @@ }, "signature-commands": { - "match": "(coerce_rule|inductive|rule|symbol|unif_rule|with)\\s+([^\\s+]*)", + "match": "(coerce_rule|inductive|rule|symbol|unif_rule|with|when)\\s+([^\\s+]*)", "captures": { "1": {"name": "storage.type.lp"}, "2": {"name": "entity.name.function.theorem.lp"} diff --git a/misc/lambdapi.tex b/misc/lambdapi.tex index 02d29e67b..090e25789 100644 --- a/misc/lambdapi.tex +++ b/misc/lambdapi.tex @@ -9,7 +9,7 @@ tabsize=2, basicstyle={\ttfamily\small\upshape}, backgroundcolor=\color{lightgrey}, - keywords={abort,admit,admitted,all_hyps,apply,as,assert,assertnot,associative,assume,assumption,begin,builtin,change,commutative,compute,constant,debug,end,eval,fail,flag,first_hyp,focus,generalize,have,in,induction,inductive,infix,injective,left,let,notation,off,on,opaque,open,orelse,prefix,print,private,proofterm,protected,prover,prover_timeout,quantifier,refine,reflexivity,repeat,require,rewrite,right,rule,sequential,set,simplify,solve,symbol,symmetry,type,TYPE,unif_rule,verbose,why3,with}, + keywords={abort,admit,admitted,all_hyps,apply,as,assert,assertnot,associative,assume,assumption,begin,builtin,change,commutative,compute,constant,debug,end,eval,fail,flag,first_hyp,focus,generalize,have,in,induction,inductive,infix,injective,left,let,notation,off,on,opaque,open,orelse,prefix,print,private,proofterm,protected,prover,prover_timeout,quantifier,refine,reflexivity,repeat,require,rewrite,right,rule,sequential,set,simplify,solve,symbol,symmetry,type,TYPE,unif_rule,verbose,why3,with,when}, sensitive=true, keywordstyle=\color{blue}, morecomment=[l]{//}, diff --git a/tests/OK/cond_rules.lp b/tests/OK/cond_rules.lp new file mode 100644 index 000000000..4c50b840c --- /dev/null +++ b/tests/OK/cond_rules.lp @@ -0,0 +1,18 @@ +symbol Prop: TYPE; +symbol ∧: Prop → Prop → Prop; +notation ∧ infix right 7; +constant symbol ⊤ : Prop; +constant symbol ⊥ : Prop; +symbol simp: Prop → Prop; +symbol simp1: Prop → Prop → Prop; + +sequential symbol subterm: Prop → Prop → Prop; +rule subterm $p $p ↪ ⊤ +with subterm $p ($p ∧ $q) ↪ ⊤ +with subterm $p (_ ∧ $q) ↪ subterm $p $q +with subterm _ _ ↪ ⊥; + +rule simp ($p ∧ ⊤) ↪ $p; +rule simp ($p ∧ $q ∧ $r) when subterm $p $r ≡ ⊤ ↪ simp1 $p $r; + +assert p q r ⊢ (simp (p ∧ q ∧ p ∧ r)) ≡ simp1 p (p ∧ r); From 944470d19a2626aeca6c6a00ffaa7792dadb8d20 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Thu, 2 Jul 2026 21:59:21 +0200 Subject: [PATCH 05/15] exclude cond_rules --- tests/export_dk.sh | 2 ++ tests/export_raw_dk.sh | 2 ++ 2 files changed, 4 insertions(+) diff --git a/tests/export_dk.sh b/tests/export_dk.sh index 741967625..e30ed6590 100755 --- a/tests/export_dk.sh +++ b/tests/export_dk.sh @@ -49,6 +49,8 @@ do Tactic|1374);; # use Tactic first_hyp|all_hyps);; + # use cond rules + cond_rules);; # requires an excluded file assume|first_hyp);; # default case diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh index 860ea29cb..40965bfdf 100755 --- a/tests/export_raw_dk.sh +++ b/tests/export_raw_dk.sh @@ -58,6 +58,8 @@ do require_nondkmident);; # module alias alias);; + # conditional rules + cond_rules);; # proofs why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp|all_hyps);; # "open" From 409d1d0938250fb35ab2ce403547d37df5cd0e60 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Fri, 3 Jul 2026 11:41:41 +0200 Subject: [PATCH 06/15] change example --- src/core/tree.ml | 8 ++------ src/parsing/scope.ml | 2 +- tests/OK/cond_rules.lp | 22 ++++++++++++---------- 3 files changed, 15 insertions(+), 17 deletions(-) diff --git a/src/core/tree.ml b/src/core/tree.ml index 7245b291a..7f768a3f3 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -186,14 +186,10 @@ module CP = struct with Not_found -> choose_vf ps in let rec choose_eq pools = - let export vars (((_,a1) as t1), ((_,a2) as t2)) = - if List.for_all (fun (i,_) -> IntMap.mem i vars) a1 - && List.for_all (fun (i,_) -> IntMap.mem i vars) a2 then - CondEQ(t1,t2) - else raise Not_found in + let export (t1, t2) = CondEQ(t1,t2) in match pools with | [] -> None - | p :: ps -> try Some(export p.variables (TSet.choose p.eq_conds)) + | p :: ps -> try Some(export (TSet.choose p.eq_conds)) with Not_found -> choose_eq ps in let res = choose_nl pools in diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index e544a98a2..9493bc62d 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -599,7 +599,7 @@ let scope_rule : ; m_lhs_arities = Hashtbl.create 7 ; m_lhs_names = Hashtbl.create 7 ; m_lhs_size = 0 - ; m_lhs_in_env = nl @ List.map fst pvs_rhs } + ; m_lhs_in_env = nl @ List.map fst pvs_rhs @ List.map fst pvs_when} in let lhs = scope ~find_sym 0 mode ss Env.empty p_lhs in match mode with diff --git a/tests/OK/cond_rules.lp b/tests/OK/cond_rules.lp index 4c50b840c..0402de7e0 100644 --- a/tests/OK/cond_rules.lp +++ b/tests/OK/cond_rules.lp @@ -3,16 +3,18 @@ symbol ∧: Prop → Prop → Prop; notation ∧ infix right 7; constant symbol ⊤ : Prop; constant symbol ⊥ : Prop; -symbol simp: Prop → Prop; -symbol simp1: Prop → Prop → Prop; -sequential symbol subterm: Prop → Prop → Prop; -rule subterm $p $p ↪ ⊤ -with subterm $p ($p ∧ $q) ↪ ⊤ -with subterm $p (_ ∧ $q) ↪ subterm $p $q -with subterm _ _ ↪ ⊥; +sequential symbol doubles_in_and : Prop → Prop; +sequential symbol occurs_in_and : Prop → Prop → Prop; -rule simp ($p ∧ ⊤) ↪ $p; -rule simp ($p ∧ $q ∧ $r) when subterm $p $r ≡ ⊤ ↪ simp1 $p $r; +rule doubles_in_and ($p ∧ $q) when occurs_in_and $p $q ≡ ⊤ ↪ ⊤ +with doubles_in_and (_ ∧ $q) ↪ doubles_in_and $q +with doubles_in_and _ ↪ ⊥; -assert p q r ⊢ (simp (p ∧ q ∧ p ∧ r)) ≡ simp1 p (p ∧ r); +rule occurs_in_and $p $p ↪ ⊤ +with occurs_in_and $p ($p ∧ _) ↪ ⊤ +with occurs_in_and $p (_ ∧ $q) ↪ occurs_in_and $p $q +with occurs_in_and _ _ ↪ ⊥; + +assert p q r ⊢ doubles_in_and (p ∧ q ∧ r) ≡ ⊥; +assert p q r ⊢ doubles_in_and (p ∧ q ∧ p ∧ r) ≡ ⊤; From b1a6f11999f4c6ea189deb185186a31f48108ff6 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Fri, 3 Jul 2026 11:44:01 +0200 Subject: [PATCH 07/15] long line --- src/parsing/scope.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index 9493bc62d..f94c1a6ae 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -599,7 +599,8 @@ let scope_rule : ; m_lhs_arities = Hashtbl.create 7 ; m_lhs_names = Hashtbl.create 7 ; m_lhs_size = 0 - ; m_lhs_in_env = nl @ List.map fst pvs_rhs @ List.map fst pvs_when} + ; m_lhs_in_env = + nl @ List.map fst pvs_rhs @ List.map fst pvs_when} in let lhs = scope ~find_sym 0 mode ss Env.empty p_lhs in match mode with From bb35eaf234e7397bb8bba535872ad7ab8cdca1d9 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Tue, 7 Jul 2026 16:12:46 +0200 Subject: [PATCH 08/15] add subterm conditions in rules --- doc/lambdapi.bnf | 5 ++- editors/emacs/lambdapi-smie.el | 5 ++- editors/emacs/lambdapi-vars.el | 1 + editors/vim/syntax/lambdapi.vim | 2 + misc/lambdapi.tex | 1 + src/core/coercion.ml | 2 +- src/core/eval.ml | 12 ++++++ src/core/term.ml | 11 ++++- src/core/term.mli | 11 ++++- src/core/tree.ml | 72 +++++++++++++++++++++++++++------ src/core/tree_type.ml | 4 ++ src/export/rawdk.ml | 2 +- src/handle/inductive.ml | 2 +- src/parsing/dkRule.ml | 2 +- src/parsing/lpLexer.ml | 2 + src/parsing/lpParser.ml | 23 ++++++++--- src/parsing/pretty.ml | 6 ++- src/parsing/scope.ml | 26 ++++++++---- src/parsing/syntax.ml | 28 +++++++++---- src/tool/lcr.ml | 4 +- src/tool/tree_graphviz.ml | 1 + tests/OK/cond_rules_st.lp | 15 +++++++ tests/export_dk.sh | 2 +- tests/export_raw_dk.sh | 2 +- 24 files changed, 191 insertions(+), 50 deletions(-) create mode 100644 tests/OK/cond_rules_st.lp diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf index e3f0444ff..71c2efe43 100644 --- a/doc/lambdapi.bnf +++ b/doc/lambdapi.bnf @@ -33,7 +33,10 @@ ::= * ":" ::= "↪" - | when ≡ "↪" + | when "↪" + + ::= ≡ + | «[] ::= "↪" "[" (";" )* "]" diff --git a/editors/emacs/lambdapi-smie.el b/editors/emacs/lambdapi-smie.el index 6d42f46a6..c004074a2 100644 --- a/editors/emacs/lambdapi-smie.el +++ b/editors/emacs/lambdapi-smie.el @@ -144,7 +144,8 @@ Indent by `lambdapi-indent-basic' in proofs, and 0 otherwise." (indcons (args ":" sterm) ("|" args ":" sterm)) (inddec (inddec "with" args ":" sterm "≔" indcons)) (rules (rules "with" sterm "↪" sterm) - (rules "with" sterm "when" sterm "≡" sterm "↪" sterm)) + (rules "with" sterm "when" condition "↪" sterm)) + (condition (sterm "«[" sterm "]" sterm) (sterm "≡" sterm)) (command ("begin" prfcontent "abort" ";") ("begin" prfcontent "admitted" ";") @@ -242,7 +243,7 @@ The default lexer is used because the syntax is primarily made of sexps." "print" "proofterm" "search" "type")) (lambdapi--query-indent)) - (`(,_ . ,(or "," "↪" "→" "≡")) (smie-rule-separator kind)) + (`(,_ . ,(or "«" "," "↪" "→" "≡")) (smie-rule-separator kind)) (`(,(or :before :list-intro) . ,(or "≔" ":")) (smie-rule-separator kind)) (`(:after . ,(or "≔" ":")) lambdapi-indent-basic) diff --git a/editors/emacs/lambdapi-vars.el b/editors/emacs/lambdapi-vars.el index 5271515d3..57513f00c 100644 --- a/editors/emacs/lambdapi-vars.el +++ b/editors/emacs/lambdapi-vars.el @@ -107,6 +107,7 @@ (modify-syntax-entry ?→ "." table) (modify-syntax-entry ?↪ "." table) (modify-syntax-entry ?≔ "." table) + (modify-syntax-entry ?« "." table) (modify-syntax-entry ?$ "." table) (modify-syntax-entry ?? "." table) (modify-syntax-entry ?: "." table) diff --git a/editors/vim/syntax/lambdapi.vim b/editors/vim/syntax/lambdapi.vim index ebef338c9..5c1635815 100644 --- a/editors/vim/syntax/lambdapi.vim +++ b/editors/vim/syntax/lambdapi.vim @@ -209,6 +209,7 @@ syntax match Keyword "," syntax match Keyword ";" syntax match Keyword "_" syntax match Keyword "≡" +syntax match Keyword "«" " Other special classes. syntax match Type "\u\w*" @@ -217,6 +218,7 @@ syntax match PreProc "?\(\<\h\w*\>\|\({|\([^|]\|\(|[^}]\)\)*|*|}\)\)" " Abbreviations. abbreviate --> ↪ +abbreviate << « abbreviate -> → abbreviate => ⇒ abbreviate ! Π diff --git a/misc/lambdapi.tex b/misc/lambdapi.tex index 090e25789..7b4f739ad 100644 --- a/misc/lambdapi.tex +++ b/misc/lambdapi.tex @@ -26,6 +26,7 @@ {≔}{$\coloneqq$}1 {⊢}{$\vdash$}1 {≡}{$\equiv$}1 + {«}{$\ll$}1 {𝔹}{$\mathbb{B}$}1 {𝕃}{$\mathbb{L}$}1 {ℕ}{$\mathbb{N}$}1 diff --git a/src/core/coercion.ml b/src/core/coercion.ml index 8f9a7cffe..7cc708ecc 100644 --- a/src/core/coercion.ml +++ b/src/core/coercion.ml @@ -15,6 +15,6 @@ let _ = and t = mk_Patt (Some 1, "t", [||]) in let lhs = [a;a;t] and arities = [|0;0|] and names = [|"A";"t"|] in { lhs; names; rhs=t; arity=3; arities; vars_nb=2; xvars_nb = 0; - rule_pos = None; r_when = None } + rule_pos = None; r_when = R_None } in Sign.add_rule Ghost.sign (coerce, rule) diff --git a/src/core/eval.ml b/src/core/eval.ml index e154756e2..68ba96f52 100644 --- a/src/core/eval.ml +++ b/src/core/eval.ml @@ -357,6 +357,18 @@ and tree_walk : config -> sym -> stack -> (term * stack) option = let t1 = add_args (mk_Symb s1) v1 in let t2 = add_args (mk_Symb s2) v2 in if eq_modulo whnf cfg t1 t2 then ok else fail + | CondST((pth,op), p1, p2) -> + let v1 = vars.(fst p1) and v2 = vars.(fst p2) in + if Logger.log_enabled() then + log_rew "%aCondST(%s,%d,%d) : %a <<[%s] %a" + D.depth !depth + op (fst p1) (fst p2) Raw.term v1 op Raw.term v2; + let rec find (p: term -> bool) (t: term) = + match unfold t with + | Appl(Appl(Symb s,a1), a2) + when s.sym_path=pth && s.sym_name=op -> p a1 || find p a2 + | t -> p t in + if find (eq_modulo whnf cfg v1) v2 then ok else fail | CondFV(i,xs) -> let allowed = (* Variables that are allowed in the term. *) diff --git a/src/core/term.ml b/src/core/term.ml index 76614350a..472a3f056 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -206,6 +206,14 @@ and sym = (** {3 Representation of rewriting rules} *) +(** optional rule constraints *) +and r_constraint = + (* equality constraint f p1 ... pn == g q1 ... qm *) + | R_EQ of (sym * int list) * (sym * int list) + (* subterm constraint p <<[op] q *) + | R_ST of sym * int * int + | R_None (* no constraint *) + (** Representation of a rewriting rule. A rewriting rule is mainly formed of a LHS (left hand side), which is the pattern that should be matched for the rule to apply, and a RHS (right hand side) giving the action to perform if @@ -214,8 +222,7 @@ and sym = { lhs : term list (** Left hand side (LHS). *) ; names : string array (** Names of pattern variables. *) ; rhs : term (** Right hand side (RHS). *) - ; r_when : ((sym * int list) * (sym * int list)) option - (** conditional rule constraint. *) + ; r_when : r_constraint (** conditional rule constraint. *) ; arity : int (** Required number of arguments to be applicable. *) ; arities : int array (** Arities of the pattern variables bound in the RHS. *) diff --git a/src/core/term.mli b/src/core/term.mli index 086e51abe..32bb0eb6e 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -138,6 +138,14 @@ and sym = (** {3 Representation of rewriting rules} *) +(** optional rule constraints *) +and r_constraint = + (* equality constraint f p1 ... pn == g q1 ... qm *) + | R_EQ of (sym * int list) * (sym * int list) + (* subterm constraint p <<[op] q *) + | R_ST of sym * int * int + | R_None (* no constraint *) + (** Representation of a rewriting rule. A rewriting rule is mainly formed of a LHS (left hand side), which is the pattern that should be matched for the rule to apply, and a RHS (right hand side) giving the action to perform if @@ -146,8 +154,7 @@ and rule = { lhs : term list (** Left hand side (LHS). *) ; names : string array (** Names of pattern variables. *) ; rhs : term (** Right hand side (RHS). *) - ; r_when : ((sym * int list) * (sym * int list)) option - (** conditional rule constraint. *) + ; r_when : r_constraint (** conditional rule constraint. *) ; arity : int (** Required number of arguments to be applicable. *) ; arities : int array (** Arities of the pattern variables bound in the RHS. *) diff --git a/src/core/tree.ml b/src/core/tree.ml index 7f768a3f3..e70f56729 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -78,6 +78,13 @@ module CP = struct let compare = Stdlib.compare end) + (** Functional sets of subterm constraints. *) + module STSet = Set.Make( + struct + type t = psym * pvar * pvar + let compare = Stdlib.compare + end) + (** A pool of (convertibility and free variable) conditions. *) type t = { variables : pvar IntMap.t @@ -95,6 +102,8 @@ module CP = struct stored at slot [i] in the [vars] array of [Eval.tree_walk]. *) ; eq_conds : TSet.t (** Set of pairs of terms that should be convertible. *) + ; st_conds : STSet.t + (** sets of subterm constraints. *) } (** [empty] is the condition pool holding no condition. *) @@ -102,13 +111,15 @@ module CP = struct { variables = IntMap.empty ; nl_conds = PSet.empty ; fv_conds = IntMap.empty - ; eq_conds = TSet.empty } + ; eq_conds = TSet.empty + ; st_conds = STSet.empty } (** [is_empty pool] tells whether the pool of constraints is empty. *) let is_empty : t -> bool = fun pool -> PSet.is_empty pool.nl_conds && IntMap.is_empty pool.fv_conds && TSet.is_empty pool.eq_conds + && STSet.is_empty pool.st_conds (** [register_nl i (slot,vs) pool] registers the fact that the slot [slot] in the [vars] array correspond to a term stored at index [i] in the @@ -140,6 +151,12 @@ module CP = struct let pv2 = List.map (fun i -> IntMap.find i pool.variables) a2 in { pool with eq_conds = TSet.add ((s1,pv1),(s2,pv2)) pool.eq_conds } + let register_st : psym -> int -> int -> t -> t = + fun op i j pool -> + let pv1 = IntMap.find i pool.variables in + let pv2 = IntMap.find j pool.variables in + { pool with st_conds = STSet.add (op, pv1, pv2) pool.st_conds } + (** [constrained_nl i pool] tells whether index [i] in the RHS's environment has already been associated to a variable of the [vars] array. *) let constrained_nl : int -> t -> bool = fun slot pool -> @@ -152,6 +169,7 @@ module CP = struct | CondNL(i,j) -> PSet.mem (i,j) pool.nl_conds | CondEQ(t1,t2) -> TSet.mem (t1,t2) pool.eq_conds || TSet.mem (t2,t1) pool.eq_conds + | CondST(o,t1,t2) -> STSet.mem (o,t1,t2) pool.st_conds | CondFV(i,x) -> try Array.eq (=) x (IntMap.find i pool.fv_conds) with Not_found -> false @@ -161,6 +179,8 @@ module CP = struct match cond with | CondNL(i,j) -> {pool with nl_conds = PSet.remove (i,j) pool.nl_conds} | CondEQ(t,u) -> {pool with eq_conds = TSet.remove (t,u) pool.eq_conds} + | CondST(o,t,u) -> + {pool with st_conds = STSet.remove (o,t,u) pool.st_conds} | CondFV(i,xs) -> try let ys = IntMap.find i pool.fv_conds in @@ -192,10 +212,20 @@ module CP = struct | p :: ps -> try Some(export (TSet.choose p.eq_conds)) with Not_found -> choose_eq ps in + let rec choose_st pools = + let export (op, t1, t2) = CondST(op,t1,t2) in + match pools with + | [] -> None + | p :: ps -> try Some(export (STSet.choose p.st_conds)) + with Not_found -> choose_st ps + in let res = choose_nl pools in if res = None then let res = choose_eq pools in - if res = None then choose_vf pools else res + if res = None then + let res = choose_st pools in + if res = None then choose_vf pools else res + else res else res end @@ -252,14 +282,23 @@ module CM = struct [0] index is used when going under abstractions. In that case, the field [arg_rank] is incremented. *) + (** rule constraints *) + type c_constraint = + | C_EQ of (psym * int list) * (psym * int list) + (** convertibility between flat terms *) + | C_ST of psym * int * int + (** subterm constraint between pattern variables *) + | C_None + (** no cnostraint *) + (** A clause matrix row (schematically {i c_lhs ↪ c_rhs if cond_pool}). *) type clause = { c_lhs : term array (** Left hand side of a rule. *) ; c_rhs : rule (** Right hand side of a rule, and number of extra variables. *) - ; c_when : ((psym * int list) * (psym * int list)) option - (** convertibility constraint for conditional rules *) + ; c_when : c_constraint + (** constraints for conditional rules *) ; c_subst : rhs_substit (** Substitution of RHS variables. *) ; xvars_nb : int @@ -329,10 +368,12 @@ module CM = struct let r2r ({lhs; xvars_nb; r_when; _} as c_rhs) = let c_lhs = Array.of_list lhs in let c_when = match r_when with - | None -> None - | Some ((s1,a1),(s2,a2)) -> - Some (((s1.sym_path,s1.sym_name), a1), - ((s2.sym_path,s2.sym_name), a2)) in + | R_None -> C_None + | R_EQ ((s1,a1),(s2,a2)) -> + C_EQ (((s1.sym_path,s1.sym_name), a1), + ((s2.sym_path,s2.sym_name), a2)) + | R_ST (op,p,q) -> C_ST ((op.sym_path,op.sym_name), p, q) + in { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb; c_when } in let size = (* Get length of longest rule *) @@ -425,7 +466,7 @@ module CM = struct in Array.for_all2 check lhs de && nonl lhs in - c_when = None && CP.is_empty cond_pool && (lhs = [||] || ripe lhs) + c_when = C_None && CP.is_empty cond_pool && (lhs = [||] || ripe lhs) (** [yield m] returns the next operation to carry out on matrix [m], that is, either specialising, solving a constraint or rewriting to a rule. *) @@ -526,8 +567,15 @@ module CM = struct let c_when, cond_pool = let vars = cond_pool.variables in match r.c_rhs.r_when with - | None -> r.c_when, cond_pool - | Some ((op1,a1), (op2,a2)) when + | R_None -> r.c_when, cond_pool + | R_ST (sy, i, j) when + IntMap.mem i vars && IntMap.mem j vars -> + if Logger.log_enabled () then + log "Registering subterm constraint on position [%a] \ + %d <<[%s] %d" + arg_path a.arg_path i sy.sym_name j; + C_None, CP.register_st (sy.sym_path,sy.sym_name) i j cond_pool + | R_EQ ((op1,a1), (op2,a2)) when List.for_all (fun i -> IntMap.mem i vars) a1 && List.for_all (fun i -> IntMap.mem i vars) a2 -> if Logger.log_enabled () then @@ -536,7 +584,7 @@ module CM = struct arg_path a.arg_path op1.sym_name (List.pp int " ") a1 op2.sym_name (List.pp int " ") a2; - None, CP.register_eq + C_None, CP.register_eq ((op1.sym_path,op1.sym_name), a1) ((op2.sym_path,op2.sym_name), a2) cond_pool diff --git a/src/core/tree_type.ml b/src/core/tree_type.ml index 127d69d1e..89933a92f 100644 --- a/src/core/tree_type.ml +++ b/src/core/tree_type.ml @@ -59,6 +59,9 @@ type tree_cond = checking) of the term at the given index in the array? *) | CondEQ of (psym * pvar list) * (psym * pvar list) (** user rule condition: are the two terms equivalent *) + | CondST of psym * pvar * pvar + (** user rule condition: is the 1st pvar a subterm of the 2nd while + traversing psym calls *) (** {b NOTE} that when performing a [tree_cond.CondFV] check, we are concerned about variables that were bound in the term being reduced @@ -76,6 +79,7 @@ let tree_cond : tree_cond pp = fun ppf tc -> out ppf "Eq(%s(%a),%s(%a))" (snd s1) (List.pp int ",") (List.map fst a1) (snd s2) (List.pp int ",") (List.map fst a2) + | CondST(op,p,q) -> out ppf "St(%s,%d,%d)" (snd op) (fst p) (fst q) (** Substitution of variables in a RHS. During the filtering process, some subterms of the filtered term may be stored in an array. Let [v] be that diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml index 42f94fb8d..d39d350dd 100644 --- a/src/export/rawdk.ml +++ b/src/export/rawdk.ml @@ -136,7 +136,7 @@ let rec remove_wraps ({elt;_} as t) = let rule : p_rule pp = let varset ppf set = List.pp string ", " ppf (StrSet.elements set) in fun ppf {elt=(l,r,w);_} -> - if w = None then + if w = P_None then out ppf "[%a] %a --> %a.@." varset (pvars_lhs l) term (remove_wraps l) term r else diff --git a/src/handle/inductive.ml b/src/handle/inductive.ml index 3e6d2beb2..57c15b97f 100644 --- a/src/handle/inductive.ml +++ b/src/handle/inductive.ml @@ -347,7 +347,7 @@ let iter_rec_rules : let nonrec_dom _ _ next = next in let codom xs rhs _ ts = let cons_arg = P.appl_list (P.iden cons_sym.sym_name) (List.rev xs) in - Pos.make rules_pos (arec ind_sym ts cons_arg, rhs, None) + Pos.make rules_pos (arec ind_sym ts cons_arg, rhs, P_None) in fold_cons_type pos ind_pred_map "" ind_sym vs cons_sym inj_var init aux acc_rec_dom rec_dom acc_nonrec_dom nonrec_dom codom diff --git a/src/parsing/dkRule.ml b/src/parsing/dkRule.ml index 65e78eb3f..135420c42 100644 --- a/src/parsing/dkRule.ml +++ b/src/parsing/dkRule.ml @@ -155,4 +155,4 @@ let to_p_rule : p_dk_rule -> p_rule = fun r -> (* NOTE the computation order is important for setting arities properly. *) let lhs = build [] lhs in let rhs = build [] rhs in - Pos.make r.pos (lhs, rhs, None) + Pos.make r.pos (lhs, rhs, P_None) diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml index 20ce558e8..2e6efa99a 100644 --- a/src/parsing/lpLexer.ml +++ b/src/parsing/lpLexer.ml @@ -129,6 +129,7 @@ type token = | R_PAREN | R_SQ_BRACKET | SEMICOLON + | SUBTERM | THICKARROW (* only in Rocq *) | TURNSTILE | UNDERSCORE @@ -332,6 +333,7 @@ let rec token ~allow_rocq_syntax lb = | ')' -> R_PAREN | ']' -> R_SQ_BRACKET | ';' -> SEMICOLON + | 0xab (* « *) -> SUBTERM | 0x22a2 (* ⊢ *) -> TURNSTILE | '|' -> VBAR | '_' -> UNDERSCORE diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index b524f207e..3f464da8a 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -99,6 +99,7 @@ let string_of_token = function | SIMPLIFY -> "simplify" | SOLVE -> "solve" | STRINGLIT _ -> "string literal" + | SUBTERM -> "«" | SWITCH false -> "off" | SWITCH true -> "on or off" | SYMBOL -> "symbol" @@ -533,7 +534,7 @@ let rec command pos1 (p_sym_mod:p_modifier list) (lb:'token lexbuf) : let (en, es) = List.(hd es, tl es) in let cat e es = P.appl (P.appl cons e) es in let rhs = List.fold_right cat es en in - let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs, None) in + let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs, P_None) in extend_pos lb (*__FUNCTION__*) pos1 (P_unif_rule(r)) | COERCE_RULE -> if p_sym_mod <> [] then expected lb "" [SYMBOL]; (*or modifiers*) @@ -689,7 +690,7 @@ and notation (lb:'token lexbuf): string Term.notation = expected lb "" [INFIX;POSTFIX;PREFIX;QUANTIFIER] and rule (lb:'token lexbuf): - (p_term * p_term * (p_term * p_term) option) loc = + (p_term * p_term * p_constraint) loc = if log_enabled() then log "%s" __FUNCTION__; let pos1 = current_pos lb in let l = term lb in @@ -697,11 +698,21 @@ and rule (lb:'token lexbuf): if (current_token lb == WHEN) then begin consume WHEN lb; let t1 = term lb in - consume EQUIV lb; - let t2 = term lb in - Some (t1,t2) + if (current_token lb == EQUIV) then begin + consume EQUIV lb; + let t2 = term lb in + P_EQ(t1, t2) + end + else begin + consume SUBTERM lb; + consume L_SQ_BRACKET lb; + let op = term lb in + consume R_SQ_BRACKET lb; + let t2 = term lb in + P_ST (op,t1,t2) + end end - else None in + else P_None in consume HOOK_ARROW lb; let r = term lb in extend_pos lb (*__FUNCTION__*) pos1 (l, r, w) diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml index c05355899..299a57edf 100644 --- a/src/parsing/pretty.ml +++ b/src/parsing/pretty.ml @@ -189,9 +189,11 @@ and typ : p_term option pp = fun ppf t -> let rule : string -> p_rule pp = fun kw ppf {elt=(l,r,w);_} -> match w with - | None -> out ppf "%s %a ↪ %a" kw term l term r - | Some (t1,t2) -> out ppf "%s %a when %a ≡ %a ↪ %a" + | P_None -> out ppf "%s %a ↪ %a" kw term l term r + | P_EQ (t1,t2) -> out ppf "%s %a when %a ≡ %a ↪ %a" kw term l term t1 term t2 term r + | P_ST (o,t1,t2) -> out ppf "%s %a when %a «[%a] %a ↪ %a" + kw term l term t1 term o term t2 term r let inductive : string -> p_inductive pp = let cons ppf (id,a) = out ppf "@,| %a : %a" ident id term a in diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index f94c1a6ae..003d93af9 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -556,8 +556,11 @@ let scope_rule : arity. *) let pvs_when = match p_when with - | None -> [] - | Some (t1,t2) -> + | P_None -> [] + | P_EQ (t1,t2) -> + let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in + p1 @ p2 + | P_ST (_o,t1,t2) -> let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in p1 @ p2 in let check_arity (m,i) = @@ -631,19 +634,26 @@ let scope_rule : let arity = List.length lhs in let f i = try Hashtbl.find names i with Not_found -> string_of_int i in let names = Array.init vars_nb f in + let asPatt t = match unfold t with + | Patt (Some i, _, [||]) -> i + | _ -> fatal rule_pos "arguments should be patterns in condition [%a]." + term t in + let asSymb t = + match unfold t with + | Symb s -> s + | _ -> fatal rule_pos "symbol expected [%a]." term t in + let p_asPatt t = asPatt (scope ~find_sym 0 mode ss Env.empty t) in + let p_asSymb t = asSymb (scope ~find_sym 0 mode ss Env.empty t) in let pw2rw t = - let asPatt t = match unfold t with - | Patt (Some i, _, [||]) -> i - | _ -> fatal rule_pos "arguments should be patterns in condition [%a]." - term t in let t = scope ~find_sym 0 mode ss Env.empty t in match get_args t with Symb s, args -> (s, List.map asPatt args) | _ -> fatal rule_pos "function should be a global symbol in [%a]." term t in let r_when = match p_when with - | None -> None - | Some (t1,t2) -> Some (pw2rw t1, pw2rw t2) in + | P_None -> R_None + | P_EQ (t1,t2) -> R_EQ (pw2rw t1, pw2rw t2) + | P_ST (o,t1,t2) -> R_ST (p_asSymb o, p_asPatt t1, p_asPatt t2) in let r = {lhs; names; rhs; arity; arities; vars_nb; xvars_nb; rule_pos; r_when} in (sym,r) diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index ae159fd14..356ad8fdc 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -133,8 +133,13 @@ let rec pvars_lhs : p_term -> StrSet.t = fun {elt;pos} -> | P_Expl u -> pvars_lhs u +type p_constraint = + P_EQ of p_term * p_term (* t1 == t2 *) +| P_ST of p_term * p_term * p_term (* t2 <<[t1] t3 *) +| P_None + (** Parser-level rewriting rule representation. *) -type p_rule_aux = p_term * p_term * (p_term * p_term) option +type p_rule_aux = p_term * p_term * p_constraint type p_rule = p_rule_aux loc (** Parser-level inductive type representation. *) @@ -182,7 +187,7 @@ module P = struct let abst_list : p_ident option list -> p_term -> p_term = fun idopts t -> List.fold_right abst idopts t - let rule : p_term -> p_term -> (p_term * p_term) option -> p_rule = + let rule : p_term -> p_term -> p_constraint -> p_rule = fun l r w -> Pos.none (l,r,w) end @@ -404,13 +409,21 @@ and eq_p_params : p_params eq = fun (i1,ao1,b1) (i2,ao2,b2) -> List.eq (Option.eq eq_p_ident) i1 i2 && Option.eq eq_p_term ao1 ao2 && b1 = b2 +let eq_p_constraint: p_constraint eq = fun c1 c2 -> + match c1,c2 with + P_EQ (t1,u1), P_EQ (t2,u2) -> eq_p_term t1 t2 && eq_p_term u1 u2 + | P_ST (o1,t1,u1), P_ST (o2,t2,u2) -> + eq_p_term o1 o2 && eq_p_term t1 t2 && eq_p_term u1 u2 + | P_None, P_None -> true + | _ -> false + let pair_eq: 'a eq -> 'b eq -> ('a * 'b) eq = fun eq1 eq2 (x1,y1) (x2,y2) -> eq1 x1 x2 && eq2 y1 y2 let eq_p_rule : p_rule eq = fun {elt=(l1,r1,w1);_} {elt=(l2,r2,w2);_} -> eq_p_term l1 l2 && eq_p_term r1 r2 - && Option.eq (pair_eq eq_p_term eq_p_term) w1 w2 + && eq_p_constraint w1 w2 let eq_p_inductive : p_inductive eq = let eq_cons (i1,t1) (i2,t2) = eq_p_ident i1 i2 && eq_p_term t1 t2 in @@ -624,14 +637,15 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a = let fold_term : 'a -> p_term -> 'a = fold_term_vars StrSet.empty in - let fold_when : 'a -> (p_term * p_term) option -> 'a = fun a w -> + let fold_constraint : 'a -> p_constraint -> 'a = fun a w -> match w with - | Some (t1,t2) -> fold_term (fold_term a t1) t2 - | None -> a + | P_EQ (t1,t2) -> fold_term (fold_term a t1) t2 + | P_ST (o,t1,t2) -> fold_term (fold_term (fold_term a o) t1) t2 + | P_None -> a in let fold_rule : 'a -> p_rule -> 'a = fun a {elt=(l,r,w);_} -> - fold_when (fold_term (fold_term a l) r) w + fold_constraint (fold_term (fold_term a l) r) w in let fold_rwpatt_vars : StrSet.t -> 'a -> p_rwpatt -> 'a = fun vs a p -> diff --git a/src/tool/lcr.ml b/src/tool/lcr.ml index d70323b97..ef2b81f35 100644 --- a/src/tool/lcr.ml +++ b/src/tool/lcr.ml @@ -55,7 +55,7 @@ let is_definable : sym -> bool = fun s -> (** [rule_of_def s d] creates the rule [s --> d]. *) let rule_of_def : sym -> term -> rule = fun s rhs -> {lhs=[]; names=[||]; rhs; arity=0; arities=[||]; vars_nb=0; xvars_nb=0; - rule_pos=s.sym_pos; r_when = None} + rule_pos=s.sym_pos; r_when = R_None} (** [replace t p u] replaces the subterm of [t] at position [p] by [u]. *) let replace : term -> subterm_pos -> term -> term = fun t p u -> @@ -457,7 +457,7 @@ let typability_constraints : Pos.popt -> term -> subs option = fun pos t -> match get_args_len l with | Symb s, lhs, arity -> let r = {lhs; names=[||]; rhs; arity; arities=[||]; vars_nb=0; - xvars_nb=0; rule_pos=Some(new_rule_id()); r_when = None} in + xvars_nb=0; rule_pos=Some(new_rule_id()); r_when = R_None} in Some (s,r) | _ -> None in diff --git a/src/tool/tree_graphviz.ml b/src/tool/tree_graphviz.ml index 4af09c70c..2780eb305 100644 --- a/src/tool/tree_graphviz.ml +++ b/src/tool/tree_graphviz.ml @@ -46,6 +46,7 @@ let tree_to_dot : Format.formatter -> _ dtree -> unit = fun ppf dtree -> | CondNL((i,vi), (j,vj)) -> out ppf "%d[%a] ≡ %d[%a]" i ar vi j ar vj | CondFV(i,vs) -> out ppf "%a ⊆ FV(%d)" ar vs i + | CondST(op,i,j) -> out ppf "%d «[%s] %d" (fst i) (snd op) (fst j) | CondEQ(((_p1,s1),a1), ((_p2,s2),a2)) -> out ppf "%s[%a] ≡ %s[%a]" s1 (List.pp int ",") (List.map fst a1) diff --git a/tests/OK/cond_rules_st.lp b/tests/OK/cond_rules_st.lp new file mode 100644 index 000000000..9a8d98fcd --- /dev/null +++ b/tests/OK/cond_rules_st.lp @@ -0,0 +1,15 @@ +symbol Prop: TYPE; +symbol ∧: Prop → Prop → Prop; +notation ∧ infix right 7; +constant symbol ⊤ : Prop; +constant symbol ⊥ : Prop; + +sequential symbol doubles_in_and : Prop → Prop; + +rule doubles_in_and ($p ∧ $q) when $p «[@∧] $q ↪ ⊤ +with doubles_in_and ($p ∧ $q) ↪ doubles_in_and $q +with doubles_in_and $p ↪ ⊥; + + +assert p q r ⊢ doubles_in_and (p ∧ q ∧ r) ≡ ⊥; +assert p q r ⊢ doubles_in_and (q ∧ p ∧ r ∧ p) ≡ ⊤; diff --git a/tests/export_dk.sh b/tests/export_dk.sh index e30ed6590..d53991647 100755 --- a/tests/export_dk.sh +++ b/tests/export_dk.sh @@ -50,7 +50,7 @@ do # use Tactic first_hyp|all_hyps);; # use cond rules - cond_rules);; + cond_rules*);; # requires an excluded file assume|first_hyp);; # default case diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh index 40965bfdf..fd01bc2bf 100755 --- a/tests/export_raw_dk.sh +++ b/tests/export_raw_dk.sh @@ -59,7 +59,7 @@ do # module alias alias);; # conditional rules - cond_rules);; + cond_rules*);; # proofs why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp|all_hyps);; # "open" From 634c3d4b2ed50ccc3b6e900c817e301cf31cef20 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Tue, 7 Jul 2026 16:18:09 +0200 Subject: [PATCH 09/15] sanity checks --- src/core/tree.ml | 6 +++--- src/parsing/scope.ml | 2 +- src/parsing/syntax.ml | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/core/tree.ml b/src/core/tree.ml index e70f56729..e1c12d7a7 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -222,7 +222,7 @@ module CP = struct let res = choose_nl pools in if res = None then let res = choose_eq pools in - if res = None then + if res = None then let res = choose_st pools in if res = None then choose_vf pools else res else res @@ -371,7 +371,7 @@ module CM = struct | R_None -> C_None | R_EQ ((s1,a1),(s2,a2)) -> C_EQ (((s1.sym_path,s1.sym_name), a1), - ((s2.sym_path,s2.sym_name), a2)) + ((s2.sym_path,s2.sym_name), a2)) | R_ST (op,p,q) -> C_ST ((op.sym_path,op.sym_name), p, q) in { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb; c_when } @@ -568,7 +568,7 @@ module CM = struct let vars = cond_pool.variables in match r.c_rhs.r_when with | R_None -> r.c_when, cond_pool - | R_ST (sy, i, j) when + | R_ST (sy, i, j) when IntMap.mem i vars && IntMap.mem j vars -> if Logger.log_enabled () then log "Registering subterm constraint on position [%a] \ diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index 003d93af9..48fdd2e81 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -638,7 +638,7 @@ let scope_rule : | Patt (Some i, _, [||]) -> i | _ -> fatal rule_pos "arguments should be patterns in condition [%a]." term t in - let asSymb t = + let asSymb t = match unfold t with | Symb s -> s | _ -> fatal rule_pos "symbol expected [%a]." term t in diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index 356ad8fdc..9b7a4caeb 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -412,7 +412,7 @@ and eq_p_params : p_params eq = fun (i1,ao1,b1) (i2,ao2,b2) -> let eq_p_constraint: p_constraint eq = fun c1 c2 -> match c1,c2 with P_EQ (t1,u1), P_EQ (t2,u2) -> eq_p_term t1 t2 && eq_p_term u1 u2 - | P_ST (o1,t1,u1), P_ST (o2,t2,u2) -> + | P_ST (o1,t1,u1), P_ST (o2,t2,u2) -> eq_p_term o1 o2 && eq_p_term t1 t2 && eq_p_term u1 u2 | P_None, P_None -> true | _ -> false From 1a3435281809041de94cdd455c5ab619a020a7f5 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Thu, 9 Jul 2026 15:08:25 +0200 Subject: [PATCH 10/15] merge-master --- src/parsing/lpParser.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index e5e720957..c48ccaa80 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -599,7 +599,7 @@ and command (lb:'token lexbuf) : p_command = let (en, es) = List.(hd es, tl es) in let cat e es = P.appl (P.appl cons e) es in let rhs = List.fold_right cat es en in - let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs) in + let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs, P_None) in extend_pos lb (*__FUNCTION__*) pos1 (P_unif_rule(r)) | COERCE_RULE -> consume_token lb; From 45d5f965f1f1001d921f95fd5ea4af0791c1a54b Mon Sep 17 00:00:00 2001 From: bodeveix Date: Wed, 15 Jul 2026 09:06:44 +0200 Subject: [PATCH 11/15] add find doubles constraint --- src/core/eval.ml | 6 ++-- src/core/term.ml | 26 ++++++++++++-- src/core/term.mli | 19 ++++++++-- src/core/tree.ml | 74 +++++++++++++++++++++++---------------- src/core/tree_type.ml | 17 ++++++--- src/handle/tactic.ml | 2 +- src/parsing/lpLexer.ml | 2 -- src/parsing/lpParser.ml | 11 ++---- src/parsing/pretty.ml | 3 +- src/parsing/scope.ml | 27 +++++++++++--- src/parsing/syntax.ml | 9 +++-- src/tool/tree_graphviz.ml | 2 +- tests/OK/assume.lp | 8 +---- 13 files changed, 134 insertions(+), 72 deletions(-) diff --git a/src/core/eval.ml b/src/core/eval.ml index 68ba96f52..50df0c129 100644 --- a/src/core/eval.ml +++ b/src/core/eval.ml @@ -357,7 +357,8 @@ and tree_walk : config -> sym -> stack -> (term * stack) option = let t1 = add_args (mk_Symb s1) v1 in let t2 = add_args (mk_Symb s2) v2 in if eq_modulo whnf cfg t1 t2 then ok else fail - | CondST((pth,op), p1, p2) -> + | CondCHK((_pth,_op), _args) -> fail +(* let v1 = vars.(fst p1) and v2 = vars.(fst p2) in if Logger.log_enabled() then log_rew "%aCondST(%s,%d,%d) : %a <<[%s] %a" @@ -368,7 +369,8 @@ and tree_walk : config -> sym -> stack -> (term * stack) option = | Appl(Appl(Symb s,a1), a2) when s.sym_path=pth && s.sym_name=op -> p a1 || find p a2 | t -> p t in - if find (eq_modulo whnf cfg v1) v2 then ok else fail + if find (eq_modulo whnf cfg v1) v2 then ok else fail + *) | CondFV(i,xs) -> let allowed = (* Variables that are allowed in the term. *) diff --git a/src/core/term.ml b/src/core/term.ml index 472a3f056..28561a909 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -206,12 +206,18 @@ and sym = (** {3 Representation of rewriting rules} *) +(** terms in rule constraints *) +and r_term = + | R_App of sym * r_term list (* application *) + | R_Patt of int (* pattern variable *) + | R_Sym of sym (* global symbol *) + (** optional rule constraints *) and r_constraint = (* equality constraint f p1 ... pn == g q1 ... qm *) | R_EQ of (sym * int list) * (sym * int list) - (* subterm constraint p <<[op] q *) - | R_ST of sym * int * int + (* predefined constraint *) + | R_CHK of sym * r_term list | R_None (* no constraint *) (** Representation of a rewriting rule. A rewriting rule is mainly formed of a @@ -997,3 +1003,19 @@ module Raw = struct let term = term let _ = term let ctxt = ctxt let _ = ctxt end + +(** {4 functions over constraints} *) + +(** [rAll p t] checks [p] on all pattern variables of [t] *) +let rec rAll : (int -> bool) -> r_term -> bool = fun p t -> + match t with + | R_App(_s,al) -> List.for_all (rAll p) al + | R_Patt i -> p i + | R_Sym _ -> true + +(** Printing function for debug *) +let rec r_term : r_term pp = fun ppf t -> + match t with + | R_App (s,al) -> out ppf "(%a %a)" sym s (List.pp r_term " ") al + | R_Patt i -> out ppf "?%d" i + | R_Sym s -> out ppf "%a" sym s diff --git a/src/core/term.mli b/src/core/term.mli index 32bb0eb6e..e69410c8e 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -138,12 +138,18 @@ and sym = (** {3 Representation of rewriting rules} *) +(** terms in rule constraints *) +and r_term = + | R_App of sym * r_term list (* application *) + | R_Patt of int (* pattern variable *) + | R_Sym of sym (* global symbol *) + (** optional rule constraints *) and r_constraint = (* equality constraint f p1 ... pn == g q1 ... qm *) | R_EQ of (sym * int list) * (sym * int list) - (* subterm constraint p <<[op] q *) - | R_ST of sym * int * int + (* predefined constraint *) + | R_CHK of sym * r_term list | R_None (* no constraint *) (** Representation of a rewriting rule. A rewriting rule is mainly formed of a @@ -475,3 +481,12 @@ module Raw : sig val term : term pp val ctxt : ctxt pp end + +(** {4 functions over constraints} *) + +(** [rAll p t] checks [p] on all pattern variables of [t] *) +val rAll : (int -> bool) -> r_term -> bool + +(** Printing function for debug *) +val r_term : r_term pp + diff --git a/src/core/tree.ml b/src/core/tree.ml index e1c12d7a7..9ddcc1828 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -78,10 +78,10 @@ module CP = struct let compare = Stdlib.compare end) - (** Functional sets of subterm constraints. *) - module STSet = Set.Make( + (** Functional sets of predefined constraints. *) + module CHKSet = Set.Make( struct - type t = psym * pvar * pvar + type t = psym * c_term list let compare = Stdlib.compare end) @@ -102,8 +102,8 @@ module CP = struct stored at slot [i] in the [vars] array of [Eval.tree_walk]. *) ; eq_conds : TSet.t (** Set of pairs of terms that should be convertible. *) - ; st_conds : STSet.t - (** sets of subterm constraints. *) + ; chk_conds : CHKSet.t + (** sets of predefined constraints. *) } (** [empty] is the condition pool holding no condition. *) @@ -112,14 +112,14 @@ module CP = struct ; nl_conds = PSet.empty ; fv_conds = IntMap.empty ; eq_conds = TSet.empty - ; st_conds = STSet.empty } + ; chk_conds = CHKSet.empty } (** [is_empty pool] tells whether the pool of constraints is empty. *) let is_empty : t -> bool = fun pool -> PSet.is_empty pool.nl_conds && IntMap.is_empty pool.fv_conds && TSet.is_empty pool.eq_conds - && STSet.is_empty pool.st_conds + && CHKSet.is_empty pool.chk_conds (** [register_nl i (slot,vs) pool] registers the fact that the slot [slot] in the [vars] array correspond to a term stored at index [i] in the @@ -151,11 +151,15 @@ module CP = struct let pv2 = List.map (fun i -> IntMap.find i pool.variables) a2 in { pool with eq_conds = TSet.add ((s1,pv1),(s2,pv2)) pool.eq_conds } - let register_st : psym -> int -> int -> t -> t = - fun op i j pool -> - let pv1 = IntMap.find i pool.variables in - let pv2 = IntMap.find j pool.variables in - { pool with st_conds = STSet.add (op, pv1, pv2) pool.st_conds } + let register_chk : sym -> r_term list -> t -> t = fun op args pool -> + let sy2sy sy = (sy.sym_path, sy.sym_name) in + let rec rt2ct t = match t with + | R_App (s, al) -> C_App(sy2sy s, List.map rt2ct al) + | R_Patt i -> C_Patt (IntMap.find i pool.variables) + | R_Sym s -> C_Sym (sy2sy s) + in + { pool with chk_conds = CHKSet.add (sy2sy op, List.map rt2ct args) + pool.chk_conds } (** [constrained_nl i pool] tells whether index [i] in the RHS's environment has already been associated to a variable of the [vars] array. *) @@ -169,7 +173,7 @@ module CP = struct | CondNL(i,j) -> PSet.mem (i,j) pool.nl_conds | CondEQ(t1,t2) -> TSet.mem (t1,t2) pool.eq_conds || TSet.mem (t2,t1) pool.eq_conds - | CondST(o,t1,t2) -> STSet.mem (o,t1,t2) pool.st_conds + | CondCHK(s,al) -> CHKSet.mem (s,al) pool.chk_conds | CondFV(i,x) -> try Array.eq (=) x (IntMap.find i pool.fv_conds) with Not_found -> false @@ -179,8 +183,8 @@ module CP = struct match cond with | CondNL(i,j) -> {pool with nl_conds = PSet.remove (i,j) pool.nl_conds} | CondEQ(t,u) -> {pool with eq_conds = TSet.remove (t,u) pool.eq_conds} - | CondST(o,t,u) -> - {pool with st_conds = STSet.remove (o,t,u) pool.st_conds} + | CondCHK(s,al) -> + {pool with chk_conds = CHKSet.remove (s,al) pool.chk_conds} | CondFV(i,xs) -> try let ys = IntMap.find i pool.fv_conds in @@ -212,18 +216,18 @@ module CP = struct | p :: ps -> try Some(export (TSet.choose p.eq_conds)) with Not_found -> choose_eq ps in - let rec choose_st pools = - let export (op, t1, t2) = CondST(op,t1,t2) in + let rec choose_chk pools = + let export (op, al) = CondCHK(op,al) in match pools with | [] -> None - | p :: ps -> try Some(export (STSet.choose p.st_conds)) - with Not_found -> choose_st ps + | p :: ps -> try Some(export (CHKSet.choose p.chk_conds)) + with Not_found -> choose_chk ps in let res = choose_nl pools in if res = None then let res = choose_eq pools in if res = None then - let res = choose_st pools in + let res = choose_chk pools in if res = None then choose_vf pools else res else res else res @@ -286,8 +290,8 @@ module CM = struct type c_constraint = | C_EQ of (psym * int list) * (psym * int list) (** convertibility between flat terms *) - | C_ST of psym * int * int - (** subterm constraint between pattern variables *) + | C_CHK of psym * c_term list + (** predefined constraint between terms *) | C_None (** no cnostraint *) @@ -365,14 +369,19 @@ module CM = struct (** [of_rules rs] transforms rewriting rules [rs] into a clause matrix. *) let of_rules : rule list -> t = fun rs -> + let sy2sy s = (s.sym_path,s.sym_name) in + let rec rt2ct : r_term -> c_term = fun t -> + match t with + | R_App(s,tl) -> C_App (sy2sy s, List.map rt2ct tl) + | R_Patt i -> C_Patt (i,[||]) + | R_Sym s -> C_Sym (sy2sy s) + in let r2r ({lhs; xvars_nb; r_when; _} as c_rhs) = let c_lhs = Array.of_list lhs in let c_when = match r_when with | R_None -> C_None - | R_EQ ((s1,a1),(s2,a2)) -> - C_EQ (((s1.sym_path,s1.sym_name), a1), - ((s2.sym_path,s2.sym_name), a2)) - | R_ST (op,p,q) -> C_ST ((op.sym_path,op.sym_name), p, q) + | R_EQ ((s1,a1),(s2,a2)) -> C_EQ ((sy2sy s1, a1), (sy2sy s2, a2)) + | R_CHK (f,al) -> C_CHK (sy2sy f, List.map rt2ct al) in { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb; c_when } in @@ -568,13 +577,16 @@ module CM = struct let vars = cond_pool.variables in match r.c_rhs.r_when with | R_None -> r.c_when, cond_pool - | R_ST (sy, i, j) when - IntMap.mem i vars && IntMap.mem j vars -> + (* find_doubles op! n! t! d? before? middle? after? *) + | R_CHK ({sym_path=[];sym_name="#find_doubles";_} as sy, + ([R_Sym _;u;t;_d;_b;_m;_a] as al)) when + rAll (fun i -> IntMap.mem i vars) u + && rAll (fun i -> IntMap.mem i vars) t -> if Logger.log_enabled () then log "Registering subterm constraint on position [%a] \ - %d <<[%s] %d" - arg_path a.arg_path i sy.sym_name j; - C_None, CP.register_st (sy.sym_path,sy.sym_name) i j cond_pool + %a %a" + arg_path a.arg_path Raw.sym sy (List.pp r_term " ") al; + C_None, CP.register_chk sy al cond_pool | R_EQ ((op1,a1), (op2,a2)) when List.for_all (fun i -> IntMap.mem i vars) a1 && List.for_all (fun i -> IntMap.mem i vars) a2 -> diff --git a/src/core/tree_type.ml b/src/core/tree_type.ml index 89933a92f..49a460f8f 100644 --- a/src/core/tree_type.ml +++ b/src/core/tree_type.ml @@ -7,6 +7,16 @@ open Common type pvar = int * int array type psym = Path.t * string +type c_term = + | C_App of psym * c_term list (* application *) + | C_Patt of pvar (* pattern variable *) + | C_Sym of psym (* global symbol *) + +let rec c_term : c_term pp = fun ppf t -> + match t with + | C_App(s,al) -> out ppf "%s [%a]" (snd s) (List.pp c_term ",") al + | C_Patt (i,_) -> out ppf "?%d" i + | C_Sym s -> out ppf "%s" (snd s) (** Representation of an atomic pattern constructor. *) module TC = @@ -59,9 +69,8 @@ type tree_cond = checking) of the term at the given index in the array? *) | CondEQ of (psym * pvar list) * (psym * pvar list) (** user rule condition: are the two terms equivalent *) - | CondST of psym * pvar * pvar - (** user rule condition: is the 1st pvar a subterm of the 2nd while - traversing psym calls *) + | CondCHK of psym * c_term list + (** user rule predefined condition *) (** {b NOTE} that when performing a [tree_cond.CondFV] check, we are concerned about variables that were bound in the term being reduced @@ -79,7 +88,7 @@ let tree_cond : tree_cond pp = fun ppf tc -> out ppf "Eq(%s(%a),%s(%a))" (snd s1) (List.pp int ",") (List.map fst a1) (snd s2) (List.pp int ",") (List.map fst a2) - | CondST(op,p,q) -> out ppf "St(%s,%d,%d)" (snd op) (fst p) (fst q) + | CondCHK(op,al) -> out ppf "CHK %s[%a]" (snd op) (List.pp c_term " ") al (** Substitution of variables in a RHS. During the filtering process, some subterms of the filtered term may be stored in an array. Let [v] be that diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index e82a4f6fa..1ee9d400a 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -783,7 +783,7 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool) let term = term_in (Ctxt.names c) in fatal pt.pos "Cannot infer the type of [%a]" term t | Some(t,_) -> - if Unif.solve_noexn p then + if Unif.solve_noexn p && !p.unsolved = [] then let ps, t = p_tactic ps g env pos t in handle ps t else fatal pos "Cannot solve typing constraints for [%a]" term t diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml index 275284dab..d900f4057 100644 --- a/src/parsing/lpLexer.ml +++ b/src/parsing/lpLexer.ml @@ -135,7 +135,6 @@ type token = | R_PAREN | R_SQ_BRACKET | SEMICOLON - | SUBTERM | THICKARROW (* only in Rocq *) | TURNSTILE | UNDERSCORE @@ -339,7 +338,6 @@ let rec token ~allow_rocq_syntax lb = | ')' -> R_PAREN | ']' -> R_SQ_BRACKET | ';' -> SEMICOLON - | 0xab (* « *) -> SUBTERM | 0x22a2 (* ⊢ *) -> TURNSTILE | '|' -> VBAR | '_' -> UNDERSCORE diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index c48ccaa80..d0162f3ea 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -99,7 +99,6 @@ let string_of_token = function | SIMPLIFY -> "simplify" | SOLVE -> "solve" | STRINGLIT _ -> "string literal" - | SUBTERM -> "«" | SWITCH false -> "off" | SWITCH true -> "on or off" | SYMBOL -> "symbol" @@ -769,14 +768,8 @@ and rule (lb:'token lexbuf): let t2 = term lb in P_EQ(t1, t2) end - else begin - consume SUBTERM lb; - consume L_SQ_BRACKET lb; - let op = term lb in - consume R_SQ_BRACKET lb; - let t2 = term lb in - P_ST (op,t1,t2) - end + else + P_CHK t1 end else P_None in consume HOOK_ARROW lb; diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml index 299a57edf..44c3f02b4 100644 --- a/src/parsing/pretty.ml +++ b/src/parsing/pretty.ml @@ -192,8 +192,7 @@ let rule : string -> p_rule pp = fun kw ppf {elt=(l,r,w);_} -> | P_None -> out ppf "%s %a ↪ %a" kw term l term r | P_EQ (t1,t2) -> out ppf "%s %a when %a ≡ %a ↪ %a" kw term l term t1 term t2 term r - | P_ST (o,t1,t2) -> out ppf "%s %a when %a «[%a] %a ↪ %a" - kw term l term t1 term o term t2 term r + | P_CHK t -> out ppf "%s %a when %a ↪ %a" kw term l term t term r let inductive : string -> p_inductive pp = let cons ppf (id,a) = out ppf "@,| %a : %a" ident id term a in diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index 48fdd2e81..80f157c45 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -560,9 +560,8 @@ let scope_rule : | P_EQ (t1,t2) -> let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in p1 @ p2 - | P_ST (_o,t1,t2) -> - let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in - p1 @ p2 in + | P_CHK t -> fst (patt_vars t) + in let check_arity (m,i) = try let j = List.assoc m pvs_lhs in @@ -638,12 +637,32 @@ let scope_rule : | Patt (Some i, _, [||]) -> i | _ -> fatal rule_pos "arguments should be patterns in condition [%a]." term t in +(* let asSymb t = match unfold t with | Symb s -> s | _ -> fatal rule_pos "symbol expected [%a]." term t in let p_asPatt t = asPatt (scope ~find_sym 0 mode ss Env.empty t) in let p_asSymb t = asSymb (scope ~find_sym 0 mode ss Env.empty t) in + *) + let rec asRTerm: Term.term -> Term.r_term = fun t -> + match get_args t with + | Patt (Some i, _, [||]), [] -> R_Patt i + | Patt (None, _, _), _ -> + fatal rule_pos "anonymous pattern not allowed in constraint [%a]." + term t + | Patt _, _ -> + fatal rule_pos "pattern applicationn not allowed in constraint [%a]." + term t + | Symb s, tl -> R_App (s, List.map asRTerm tl) + | f,_ -> fatal rule_pos "function not allowed in constraint [%a]." + term f in + let asRTerm : Term.term -> sym * Term.r_term list = fun t -> + match asRTerm t with + | R_App (s,al) -> s,al + | _ -> fatal rule_pos "constraint should be a function call [%a]." + term t in + let p_asRTerm t = asRTerm (scope ~find_sym 0 mode ss Env.empty t) in let pw2rw t = let t = scope ~find_sym 0 mode ss Env.empty t in match get_args t with @@ -653,7 +672,7 @@ let scope_rule : let r_when = match p_when with | P_None -> R_None | P_EQ (t1,t2) -> R_EQ (pw2rw t1, pw2rw t2) - | P_ST (o,t1,t2) -> R_ST (p_asSymb o, p_asPatt t1, p_asPatt t2) in + | P_CHK t -> let (f,al) = p_asRTerm t in R_CHK (f,al) in let r = {lhs; names; rhs; arity; arities; vars_nb; xvars_nb; rule_pos; r_when} in (sym,r) diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index 9b7a4caeb..3f893192b 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -134,8 +134,8 @@ let rec pvars_lhs : p_term -> StrSet.t = fun {elt;pos} -> -> pvars_lhs u type p_constraint = - P_EQ of p_term * p_term (* t1 == t2 *) -| P_ST of p_term * p_term * p_term (* t2 <<[t1] t3 *) + P_EQ of p_term * p_term (* when t1 == t2 *) +| P_CHK of p_term (* when t *) | P_None (** Parser-level rewriting rule representation. *) @@ -412,8 +412,7 @@ and eq_p_params : p_params eq = fun (i1,ao1,b1) (i2,ao2,b2) -> let eq_p_constraint: p_constraint eq = fun c1 c2 -> match c1,c2 with P_EQ (t1,u1), P_EQ (t2,u2) -> eq_p_term t1 t2 && eq_p_term u1 u2 - | P_ST (o1,t1,u1), P_ST (o2,t2,u2) -> - eq_p_term o1 o2 && eq_p_term t1 t2 && eq_p_term u1 u2 + | P_CHK t1, P_CHK t2 -> eq_p_term t1 t2 | P_None, P_None -> true | _ -> false @@ -640,7 +639,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a = let fold_constraint : 'a -> p_constraint -> 'a = fun a w -> match w with | P_EQ (t1,t2) -> fold_term (fold_term a t1) t2 - | P_ST (o,t1,t2) -> fold_term (fold_term (fold_term a o) t1) t2 + | P_CHK t -> fold_term a t | P_None -> a in diff --git a/src/tool/tree_graphviz.ml b/src/tool/tree_graphviz.ml index 2780eb305..cbab95dfc 100644 --- a/src/tool/tree_graphviz.ml +++ b/src/tool/tree_graphviz.ml @@ -46,7 +46,7 @@ let tree_to_dot : Format.formatter -> _ dtree -> unit = fun ppf dtree -> | CondNL((i,vi), (j,vj)) -> out ppf "%d[%a] ≡ %d[%a]" i ar vi j ar vj | CondFV(i,vs) -> out ppf "%a ⊆ FV(%d)" ar vs i - | CondST(op,i,j) -> out ppf "%d «[%s] %d" (fst i) (snd op) (fst j) + | CondCHK(op,al) -> out ppf "%s[%a]" (snd op) (List.pp c_term ",") al | CondEQ(((_p1,s1),a1), ((_p2,s2),a2)) -> out ppf "%s[%a] ≡ %s[%a]" s1 (List.pp int ",") (List.map fst a1) diff --git a/tests/OK/assume.lp b/tests/OK/assume.lp index 6c6bb1487..607900877 100644 --- a/tests/OK/assume.lp +++ b/tests/OK/assume.lp @@ -1,7 +1,3 @@ -symbol Set: TYPE; -symbol Prop: TYPE; -injective symbol τ: Set → TYPE; -injective symbol π: Prop → TYPE; require open tests.OK.Tactic; constant symbol OK: Prop; @@ -10,7 +6,5 @@ symbol isOK [a:Set] (x:τ a): π OK; symbol test [a:Set] (x: τ a) (y: τ a): π OK ≔ begin assume a; - eval (#assume "x" (λ x1, - (#assume "x" (λ x2, - #apply (isOK x1))))); + eval (#assume "x" (λ x1, #assume "x" (λ x2, #apply (isOK x1)))); end; From db3115b3cef85c633bbbcac57e5ab604a9b45c10 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Wed, 15 Jul 2026 09:11:10 +0200 Subject: [PATCH 12/15] merge dk --- src/parsing/lpParser.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index c31ab2d0f..f8d92ef1e 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -119,7 +119,6 @@ let string_of_token = | UID_EXPL _ -> "@-prefixed non-qualified identifier" | UID_META _ -> "?-prefixed metavariable number" | UID_PATT _ -> "$-prefixed non-qualified identifier" - | UNDERSCORE -> q"_" | UNIF_RULE -> q"unif_rule" | VBAR -> q"|" @@ -129,7 +128,6 @@ let string_of_token = | WITH -> q"with" let string_of_tokens = List.fold_left (fun s t -> s^", "^string_of_token t) ->>>>>>> dk/master let pp_token ppf t = Base.string ppf (string_of_token t) From a46fd3918e151826da6fb5db1b76e1b4efac2eb6 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Thu, 16 Jul 2026 21:34:27 +0200 Subject: [PATCH 13/15] find_doubles --- src/core/eval.ml | 75 ++++++++++++++++++++++++++++++++------- src/core/term.ml | 16 +++++++++ src/core/term.mli | 10 +++++- src/core/tree.ml | 25 ++++++++----- src/parsing/scope.ml | 35 +++++++++--------- src/tool/sr.ml | 29 +++++++++++++++ tests/OK/cond_rules_st.lp | 19 ++++++---- 7 files changed, 165 insertions(+), 44 deletions(-) diff --git a/src/core/eval.ml b/src/core/eval.ml index 50df0c129..689d31597 100644 --- a/src/core/eval.ml +++ b/src/core/eval.ml @@ -291,6 +291,33 @@ and tree_walk : config -> sym -> stack -> (term * stack) option = let (lazy capacity, lazy tree) = cfg.dtree s in let vars = Array.make capacity mk_Kind in (* dummy terms *) let bound = Array.make capacity None in + (* [ct2t t] transforms a contraint to a term by replacing pattern variables + by their values *) + let rec ct2t : Tree_type.c_term -> term = fun t -> + match t with + | Tree_type.C_App ((p,s), al) -> + add_args (mk_Symb (Sign.find_qualified p s)) (List.map ct2t al) + | C_Patt pv -> vars.(fst pv) + | C_Sym (p,s) -> mk_Symb (Sign.find_qualified p s) + in + (* [flatten op t] returns the list of arguments of [op] + considered as associative at the top level of [t] *) + let flatten: sym -> term -> term list = fun sy t -> + let rec flatten acc t = + match get_args t with + | (Symb s, al) when s == sy -> List.fold_left flatten acc al + | _ -> t::acc + in flatten [] t + in + (* [rebuild op u l] applies the binary [op] on arguments of [l], + returns [u] if [l] is empty. + *) + let rebuild: sym -> term -> term list -> term = fun sy u l -> + match l with + | [] -> u + | [t] -> t + | _ -> List.fold_left (fun a t -> mk_Appl(a,t)) (mk_Symb sy) l + in (* [walk tree stk cursor vars_id id_vars] where [stk] is the stack of terms to match and [cursor] the cursor indicating where to write in the [vars] array described in {!module:Term} as the environment of the RHS during @@ -357,20 +384,44 @@ and tree_walk : config -> sym -> stack -> (term * stack) option = let t1 = add_args (mk_Symb s1) v1 in let t2 = add_args (mk_Symb s2) v2 in if eq_modulo whnf cfg t1 t2 then ok else fail - | CondCHK((_pth,_op), _args) -> fail -(* - let v1 = vars.(fst p1) and v2 = vars.(fst p2) in + + (* find_doubles ty! op! n! t! d? before? middle? after? *) + | CondCHK((_,"#find_doubles"), [ty;C_App((p,o),[]);u;t;d;b;m;a]) -> if Logger.log_enabled() then - log_rew "%aCondST(%s,%d,%d) : %a <<[%s] %a" + log_rew "%aCondCHK(\"find_doubles\",%s,%a,%a) : %a %a" D.depth !depth - op (fst p1) (fst p2) Raw.term v1 op Raw.term v2; - let rec find (p: term -> bool) (t: term) = - match unfold t with - | Appl(Appl(Symb s,a1), a2) - when s.sym_path=pth && s.sym_name=op -> p a1 || find p a2 - | t -> p t in - if find (eq_modulo whnf cfg v1) v2 then ok else fail - *) + o c_term u c_term t Raw.term (ct2t u) Raw.term (ct2t t); + let sy = Sign.find_qualified p o in + let _ty = ct2t ty and u = ct2t u and t = ct2t t in + let d,b,m,a = ct2t d, ct2t b, ct2t m, ct2t a in + let rec doubles l = + match l with + [] -> raise Not_found + | t::l' -> + try + let (b,_,a) = List.split (fun u -> Term.cmp t u = 0) l' + in (t, [], b, a) + with Not_found -> + let (d,b,m,a) = doubles l' in + (d,(t::b),m,a) + in + begin + try + let t = snf (whnf cfg) t in + let (sd,sb,sm,sa) = doubles (flatten sy t) in + let sb = rebuild sy u sb in + let sm = rebuild sy u sm in + let sa = rebuild sy u sa in + if eq_modulo whnf cfg sd d + && eq_modulo whnf cfg sb b + && eq_modulo whnf cfg sm m + && eq_modulo whnf cfg sa a then + ok + else + fail + with Not_found -> fail + end + | CondCHK((_pth,_op), _args) -> fail | CondFV(i,xs) -> let allowed = (* Variables that are allowed in the term. *) diff --git a/src/core/term.ml b/src/core/term.ml index eb7450fbc..31b853f91 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -1016,6 +1016,22 @@ let rec rAll : (int -> bool) -> r_term -> bool = fun p t -> | R_Patt i -> p i | R_Sym _ -> true +(** [rFind f t] applies [f] to each pvar of [t] and returns the first + successful result, None if all calls fail. *) +let rec rFind : (int -> 'a option) -> r_term -> 'a option = fun f t -> + match t with + | R_App(_s,al) -> List.find_map (rFind f) al + | R_Patt i -> f i + | R_Sym _ -> None + +(** [rFold o a t] computes [a o pv1 o ... pvn] where pv1...pvn are the + pattern variables of t. *) +let rec rFold : ('a -> int -> 'a) -> 'a -> r_term -> 'a = fun f a t -> + match t with + | R_App(_s,al) -> List.fold_left (rFold f) a al + | R_Patt i -> f a i + | R_Sym _ -> a + (** Printing function for debug *) let rec r_term : r_term pp = fun ppf t -> match t with diff --git a/src/core/term.mli b/src/core/term.mli index e69410c8e..0ca1b30d0 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -484,9 +484,17 @@ end (** {4 functions over constraints} *) -(** [rAll p t] checks [p] on all pattern variables of [t] *) +(** [rAll p t] checks [p] on all pattern variables of [t]. *) val rAll : (int -> bool) -> r_term -> bool +(** [rFind f t] applies [f] to each pvar of [t] and returns the first + successful result, None if all calls fail. *) +val rFind : (int -> 'a option) -> r_term -> 'a option + +(** [rFold o a t] computes [a o pv1 o ... pvn] where pv1...pvn are the + pattern variables of t. *) +val rFold : ('a -> int -> 'a) -> 'a -> r_term -> 'a + (** Printing function for debug *) val r_term : r_term pp diff --git a/src/core/tree.ml b/src/core/tree.ml index 9ddcc1828..42039a9be 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -577,16 +577,25 @@ module CM = struct let vars = cond_pool.variables in match r.c_rhs.r_when with | R_None -> r.c_when, cond_pool - (* find_doubles op! n! t! d? before? middle? after? *) - | R_CHK ({sym_path=[];sym_name="#find_doubles";_} as sy, - ([R_Sym _;u;t;_d;_b;_m;_a] as al)) when - rAll (fun i -> IntMap.mem i vars) u - && rAll (fun i -> IntMap.mem i vars) t -> + (* find_doubles ty! op! n! t! d? before? middle? after? *) + | R_CHK ({sym_name="#find_doubles";_} as sy, + ([ty; R_App (_, []);u;t;rd;rb;rm;ra] as al)) when + rAll (fun i -> IntMap.mem i vars) ty + && rAll (fun i -> IntMap.mem i vars) u + && rAll (fun i -> IntMap.mem i vars) t -> begin + let (_mem, cond_pool) = List.fold_left (rFold (fun (m,p) i -> m+1,CP.register_nl i (m,vs) p)) + (mem,cond_pool) [rd;rb;rm;ra] in +(* + match List.find_map (rFind (fun i -> if IntMap.mem i vars then None else Some i)) [rd;rb;rm;ra] with + Some i -> r.c_when, CP.register_nl i (mem,vs) cond_pool + | None -> +*) if Logger.log_enabled () then - log "Registering subterm constraint on position [%a] \ + log "Registering predefined constraint on position [%a] \ %a %a" arg_path a.arg_path Raw.sym sy (List.pp r_term " ") al; - C_None, CP.register_chk sy al cond_pool + C_None, CP.register_chk sy al cond_pool + end | R_EQ ((op1,a1), (op2,a2)) when List.for_all (fun i -> IntMap.mem i vars) a1 && List.for_all (fun i -> IntMap.mem i vars) a2 -> @@ -844,7 +853,7 @@ let compile : match_strat -> CM.t -> tree = fun mstrat m -> in let right = compile_cv {cm with clauses=CM.not_empty_stack clauses} in Eos(left, right) - | Specialise(swap) -> + | Specialise(swap) -> if Logger.log_enabled () then log "Swap on column %d" swap; let store = CM.store cm swap in let updated = diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index 557d07f50..973888b32 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -559,16 +559,23 @@ let scope_rule : let (pvs_lhs, nl) = patt_vars p_lhs in (* NOTE to reject non-left-linear rules check [nl = []] here. *) let (pvs_rhs, _ ) = patt_vars p_rhs in - (* Check that pattern variables of RHS that are in the LHS have the right - arity. *) + (* input/output variables in condition *) let pvs_when = match p_when with - | P_None -> [] + | P_None -> [],[] | P_EQ (t1,t2) -> let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in - p1 @ p2 - | P_CHK t -> fst (patt_vars t) + (p1 @ p2), [] + | P_CHK t -> + match p_get_args t with + (* find_doubles op! n! t! d? before? middle? after? *) + | {elt=P_Iden({elt=(_,"#find_doubles");_},_);_}, [ty;op;u;t;d;b;m;a] -> + (List.concat_map (fun t -> fst (patt_vars t)) [ty;u;t]), + (List.concat_map (fun t -> fst (patt_vars t)) [d;b;m;a]) + | _ -> fatal t.pos "Undefined constraint." in + (* Check that pattern variables of RHS that are in the LHS have the right + arity. *) let check_arity (m,i) = try let j = List.assoc m pvs_lhs in @@ -576,7 +583,8 @@ let scope_rule : with Not_found -> () in List.iter check_arity pvs_rhs; - List.iter check_arity pvs_when; + List.iter check_arity (fst pvs_when); + List.iter check_arity (snd pvs_when); (* [get_root t] returns the symbol at the root of the p_term [t]. *) let rec get_root t = get_root_after_pratt (Pratt.parse ~find_sym ss [] t) and get_root_after_pratt t = @@ -609,9 +617,12 @@ let scope_rule : ; m_lhs_names = Hashtbl.create 7 ; m_lhs_size = 0 ; m_lhs_in_env = - nl @ List.map fst pvs_rhs @ List.map fst pvs_when} + nl @ List.map fst pvs_rhs @ List.map fst (snd pvs_when)} in let lhs = scope ~find_sym 0 mode ss Env.empty p_lhs in + let _ = match p_when with + P_CHK t -> ignore (scope ~find_sym 0 mode ss Env.empty t) + | _ -> () in match mode with | M_LHS{ m_lhs_indices; m_lhs_names; m_lhs_size; m_lhs_arities; _} -> let lhs = snd (get_args lhs) in @@ -644,14 +655,6 @@ let scope_rule : | Patt (Some i, _, [||]) -> i | _ -> fatal rule_pos "arguments should be patterns in condition [%a]." term t in -(* - let asSymb t = - match unfold t with - | Symb s -> s - | _ -> fatal rule_pos "symbol expected [%a]." term t in - let p_asPatt t = asPatt (scope ~find_sym 0 mode ss Env.empty t) in - let p_asSymb t = asSymb (scope ~find_sym 0 mode ss Env.empty t) in - *) let rec asRTerm: Term.term -> Term.r_term = fun t -> match get_args t with | Patt (Some i, _, [||]), [] -> R_Patt i @@ -662,7 +665,7 @@ let scope_rule : fatal rule_pos "pattern applicationn not allowed in constraint [%a]." term t | Symb s, tl -> R_App (s, List.map asRTerm tl) - | f,_ -> fatal rule_pos "function not allowed in constraint [%a]." + | f,_ -> fatal rule_pos "Not allowed in constraint [%a]." term f in let asRTerm : Term.term -> sym * Term.r_term list = fun t -> match asRTerm t with diff --git a/src/tool/sr.ml b/src/tool/sr.ml index 1aefa6e18..22f63cdef 100644 --- a/src/tool/sr.ml +++ b/src/tool/sr.ml @@ -83,6 +83,29 @@ let symb_to_patt : Pos.popt -> (int * int option) SymMap.t -> string array in symb_to_patt +(** [check_constraint p metas c] adds typing constraints associated to + rule condition [c] to [p] after replacing variable indexes by metas + variables in [c]. *) +let check_constraint : + problem -> meta array -> r_constraint -> + (term * term) option + = fun p metas c -> + let rec asTerm : r_term -> term = fun t -> + match t with + | R_App(sy,al) -> + List.fold_left (fun f a -> mk_Appl(f,asTerm a)) (mk_Symb sy) al + | R_Patt i -> mk_Meta (metas.(i),[||]) + | R_Sym sy -> mk_Symb sy in + match c with + | R_EQ ((sy1,al1),(sy2,al2)) -> + let t1 = asTerm (R_App(sy1, List.map (fun i -> R_Patt i) al1)) in + let t2 = asTerm (R_App(sy2, List.map (fun i -> R_Patt i) al2)) in + let t = add_args (mk_Symb Unif_rule.equiv) [t1;t2] in + Infer.infer_noexn p [] t + | R_CHK (sy, al) -> + Infer.infer_noexn p [] (asTerm (R_App(sy,al))) + | R_None -> Infer.infer_noexn p [] mk_Type + (** [check_rule r] checks whether the rule [r] preserves typing. *) let check_rule : Pos.popt -> sym_rule -> sym_rule = fun pos ((s,({lhs;names;rhs;arities;vars_nb;xvars_nb;_} as r)) as sr) -> @@ -121,6 +144,12 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule = | Some (lhs_with_metas, ty_lhs) -> if not (Unif.solve_noexn ~type_check:false p) then fatal pos "The LHS is not typable."; + (* Infer the typing constraints of the condition. *) + match check_constraint p metas r.r_when with + | None -> fatal pos "The constraint is not typable." + | Some (_,_) -> + if not (Unif.solve_noexn ~type_check:false p) then + fatal pos "The constraint is not typable."; (* Try to simplify constraints. *) let norm_constr (c,t,u) = (c, Eval.snf [] t, Eval.snf [] u) in let lhs_constrs = List.map norm_constr !p.unsolved in diff --git a/tests/OK/cond_rules_st.lp b/tests/OK/cond_rules_st.lp index 9a8d98fcd..c9aa5a6fd 100644 --- a/tests/OK/cond_rules_st.lp +++ b/tests/OK/cond_rules_st.lp @@ -1,15 +1,20 @@ -symbol Prop: TYPE; +require open tests.OK.List; + symbol ∧: Prop → Prop → Prop; notation ∧ infix right 7; constant symbol ⊤ : Prop; constant symbol ⊥ : Prop; -sequential symbol doubles_in_and : Prop → Prop; +constant symbol o: Set; +rule τ o ↪ Prop; + +symbol #find_doubles (T:Set) (op: τ T → τ T → τ T) (u: τ T) (p: τ T) (d: τ T) (b m a: τ T): Prop; -rule doubles_in_and ($p ∧ $q) when $p «[@∧] $q ↪ ⊤ -with doubles_in_and ($p ∧ $q) ↪ doubles_in_and $q -with doubles_in_and $p ↪ ⊥; +sequential symbol simpl: Prop → Prop; +rule simpl $p when #find_doubles o @∧ ⊤ $p $d $b $m $a ↪ $b ∧ $d ∧ $m ∧ $a; +rule simpl $p ↪ $p; +//compute (λ p q r, simpl (p ∧ q ∧ r ∧ p)); -assert p q r ⊢ doubles_in_and (p ∧ q ∧ r) ≡ ⊥; -assert p q r ⊢ doubles_in_and (q ∧ p ∧ r ∧ p) ≡ ⊤; +//assert p q r ⊢ simpl (p ∧ q ∧ r) ≡ p ∧ q ∧ r; +assert p q r ⊢ simpl (q ∧ p ∧ r ∧ p) ≡ p; From 9b8cb7ccd1783cbe40a9b9a9c9a327644c398f30 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Tue, 21 Jul 2026 11:30:45 +0200 Subject: [PATCH 14/15] merging --- src/core/libMeta.ml | 9 ++++++++- src/core/sign.ml | 5 +++-- src/core/tree.ml | 4 +++- src/core/unif.ml | 4 +++- src/handle/tactic.ml | 5 +++-- 5 files changed, 20 insertions(+), 7 deletions(-) diff --git a/src/core/libMeta.ml b/src/core/libMeta.ml index bff70f3e1..60d7720b0 100644 --- a/src/core/libMeta.ml +++ b/src/core/libMeta.ml @@ -37,7 +37,14 @@ let set : problem -> meta -> mbinder -> unit = fun p m v -> let make : problem -> ctxt -> term -> term = fun p ctx a -> let a,k = Ctxt.to_prod ctx a in let m = fresh p a k in - mk_Meta(m, Array.of_list (List.rev_map (fun (x,_,_) -> mk_Vari x) ctx)) +(* + mk_Meta(m, Array.of_list (List.rev_map (fun (x,_,_) -> mk_Vari x) ctx)) +*) + mk_Meta(m, Array.of_list (List.filter_rev_map + (fun (x,_,v) -> if v=None then + Some (mk_Vari x) else None) + ctx)) + (* jpb *) (** [make_codomain p ctx a] creates a fresh metavariable term of type [Type] in the context [ctx] extended with a fresh variable of type [a], and diff --git a/src/core/sign.ml b/src/core/sign.ml index 329cd423a..31e3694bc 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -137,14 +137,15 @@ let link : t -> unit = fun sign -> and link_term = link_term mk_Appl in let link_rule r = let lhs = List.map link_lhs r.lhs in + let arity = List.length lhs in let rhs = link_term r.rhs in - {r with lhs ; rhs} + {r with lhs ; rhs; arity} (* jpb *) in let f _ s = s.sym_type := link_term !(s.sym_type); s.sym_def := Option.map link_term !(s.sym_def); s.sym_rules := List.map link_rule !(s.sym_rules); - Tree.update_dtree s [] + Tree.update_dtree s []; in StrMap.iter f !(sign.sign_symbols); let f mp {dep_symbols=sm; _} = diff --git a/src/core/tree.ml b/src/core/tree.ml index 42039a9be..9959d827e 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -264,6 +264,7 @@ module CM = struct | Abst _, _ -> "λ" | Prod _, _ -> "Π" | Type, _ -> "TYPE" + | Appl _, _ -> "@" | _ -> assert false (* Terms that souldn't appear in lhs *) ) (** Representation of a subterm in argument position in a pattern. *) @@ -464,6 +465,7 @@ module CM = struct let depths = Array.of_list (List.map (fun i -> i.arg_rank) positions) in let ripe lhs = (* [ripe l] returns whether [lhs] can be applied. *) + Array.length lhs <= Array.length depths && (* jpb *) let de = Array.sub depths 0 (Array.length lhs) in let check pt de = (* We verify that there are no variable constraints, that is, if @@ -799,7 +801,7 @@ let harvest : in default_node true (loop ts subst (slot + 1)) | Patt(None,_,_)::ts -> default_node false (loop ts subst slot) - | _ -> assert false + | t :: _ -> log "tree error %a" CM.head t; assert false in loop (Array.to_list lhs) subst slot diff --git a/src/core/unif.ml b/src/core/unif.ml index 17b2a2048..eb939bad3 100644 --- a/src/core/unif.ml +++ b/src/core/unif.ml @@ -63,7 +63,9 @@ let rec type_app : ctxt -> term -> term list -> term option = fun c a ts -> | _, [] -> Some a | Prod(_,b), t::ts -> type_app c (subst b t) ts | LLet(_,d,b), t::ts -> - assert (Eval.pure_eq_modulo c d t); type_app c (subst b d) ts +let _ = if not (Eval.pure_eq_modulo c d t) then +log "LET ERROR??? %a -- %a" term a term t in + (*assert (Eval.pure_eq_modulo c d t);*) type_app c (subst b d) ts | _ -> match Eval.whnf c a, ts with | Prod(_,b), t::ts -> type_app c (subst b t) ts diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index a87ddf256..b66bb690f 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -109,6 +109,7 @@ let tac_solve : popt -> proof_state -> proof_state = fun pos ps -> gs_typ @ MetaSet.fold add_goal (!p).metas (List.map (fun c -> Unif c) (!p).unsolved) in +let _ = log "SOLVE: %a" (List.pp Goal.pp "\n") proof_goals in {ps with proof_goals} (** [tac_refine pos ps gt gs p t] refines the typing goal [gt] with [t]. *) @@ -235,7 +236,7 @@ let get_config (ss:Sig_state.t) (pos:Pos.popt) : config = Hashtbl.add t s.sym_name v in add "admit" T_admit; - add "and" T_and; + add "then" T_and; add "all_hyps" T_all_hyps; add "apply" T_apply; add "assume" T_assume; @@ -398,7 +399,7 @@ let handle (ss:Sig_state.t) (sym_pos:popt) (priv:bool) | T_all_hyps, _ -> assert false | T_apply, [_;t] -> ps, mk(P_tac_apply(p_term t)) | T_apply, _ -> assert false - | T_assume, [prefix;_;Abst(_, t)] -> + | T_assume, [prefix;_;_;Abst(_, t)] -> begin let n = new_name (string_of_term pos prefix) env in let idopts = [Some(Pos.make pos n)] in From 4834ac3e35b19d70fb5488740ae0d8881e2b5225 Mon Sep 17 00:00:00 2001 From: bodeveix Date: Wed, 22 Jul 2026 17:21:39 +0200 Subject: [PATCH 15/15] merging --- src/tool/sr.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/tool/sr.ml b/src/tool/sr.ml index 712ce2b11..43e258430 100644 --- a/src/tool/sr.ml +++ b/src/tool/sr.ml @@ -144,6 +144,13 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule = | Some (lhs_with_metas, ty_lhs) -> if not (Unif.solve_noexn ~type_check:false p) then fatal pos "The LHS is not typable."; + (* Infer the typing constraints of the condition. *) + match check_constraint p metas r.r_when with + | None -> fatal pos "The constraint is not typable." + | Some (_,_) -> + if not (Unif.solve_noexn ~type_check:false p) then + fatal pos "The constraint is not typable."; + (* Try to simplify constraints. *) (* Normalize constraints. *) let norm_constr (c,t,u) = (c, Eval.snf [] t, Eval.snf [] u) in let lhs_constrs = List.map norm_constr !p.unsolved in