Conditional rules

CHANGES.md

@@ -23,6 +23,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Export to Lean.
 - Tactic `all_hyps t` calls parameterized tactic term t on all hypotheses ignoring failing calls.
 - Extend `print` query to the following arguments: `verbose`, `debug`, `flag`, `builtin`, `prover`, `prover_timeout`.
+- Conditional rules `l when t1 ≡ t2 ↪ r`
 
 ### Changed
 

doc/lambdapi.bnf

@@ -35,6 +35,10 @@
 <constructor> ::= <uid> <param_list>* ":" <term>
 
 <rule> ::= <term> "↪" <term>
+         | <term> when <condition> "↪" <term>
+
+<condition> ::= <term> ≡ <term>
+              | <term> «[<term>] <term>
 
 <unif_rule> ::= <equation> "↪" "[" <equation> (";" <equation>)* "]"
 

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,9 @@ 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" condition "↪" sterm))
+      (condition (sterm "«[" sterm "]" sterm) (sterm "≡" sterm))
       (command
                ("begin" prfcontent "abort" ";")
                ("begin" prfcontent "admitted" ";")
@@ -240,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)

editors/emacs/lambdapi-vars.el

@@ -47,6 +47,7 @@
     "rule"
     "symbol"
     "unif_rule"
+    "when"
     "with")
   "Commands that enrich the signature.")
 
@@ -106,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)

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
@@ -207,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*"
@@ -215,6 +218,7 @@ syntax match PreProc  "?\(\<\h\w*\>\|\({|\([^|]\|\(|[^}]\)\)*|*|}\)\)"
 
 " Abbreviations.
 abbreviate --> ↪
+abbreviate << «
 abbreviate -> →
 abbreviate => ⇒
 abbreviate !  Π

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"}

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]{//},
@@ -26,6 +26,7 @@
   {≔}{$\coloneqq$}1
   {⊢}{$\vdash$}1
   {≡}{$\equiv$}1
+  {«}{$\ll$}1
   {𝔹}{$\mathbb{B}$}1
   {𝕃}{$\mathbb{L}$}1
   {ℕ}{$\mathbb{N}$}1

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 = R_None }
   in
   Sign.add_rule Ghost.sign (coerce, rule)

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
@@ -342,6 +369,59 @@ 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
+
+          (* 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 "%aCondCHK(\"find_doubles\",%s,%a,%a) : %a %a"
+                  D.depth !depth
+                  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. *)

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

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; _} =

src/core/term.ml

@@ -211,6 +211,20 @@ 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)
+  (* 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
     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
@@ -219,6 +233,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   : 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. *)
@@ -993,3 +1008,35 @@ 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
+
+(** [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
+  | 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

src/core/term.mli

@@ -140,6 +140,20 @@ 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)
+  (* 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
     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
@@ -148,6 +162,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   : 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. *)
@@ -177,8 +192,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,
@@ -468,3 +483,20 @@ 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
+
+(** [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
+