Exports for the format TRS + small improvement to HRS export

src/cli/lambdapi.ml

@@ -100,7 +100,7 @@ let parse_cmd : Config.t -> string list -> unit = fun cfg files ->
   Error.handle_exceptions run
 
 (** Possible outputs for the export command. *)
-type output = Lp | Dk | Hrs | Xtc | RawCoq | SttCoq
+type output = Lp | Dk | Hrs | Xtc | Trs | RawCoq | SttCoq
 
 (** Running the export mode. *)
 let export_cmd (cfg:Config.t) (output:output option) (encoding:string option)
@@ -117,6 +117,8 @@ let export_cmd (cfg:Config.t) (output:output option) (encoding:string option)
     | Some Dk -> Export.Dk.sign (Compile.compile_file file)
     | Some Hrs ->
       Export.Hrs.sign Format.std_formatter (Compile.compile_file file)
+    | Some Trs ->
+      Export.Trs.sign Format.std_formatter (Compile.compile_file file)
     | Some Xtc ->
       Export.Xtc.sign Format.std_formatter (Compile.compile_file file)
     | Some RawCoq ->
@@ -231,6 +233,7 @@ let output : output option CLT.t =
       | "dk" -> Ok Dk
       | "hrs" -> Ok Hrs
       | "xtc" -> Ok Xtc
+      | "trs" -> Ok Trs
       | "raw_coq" -> Ok RawCoq
       | "stt_coq" -> Ok SttCoq
       | _ -> Error(`Msg "Invalid format")
@@ -242,6 +245,7 @@ let output : output option CLT.t =
          | Dk -> "dk"
          | Hrs -> "hrs"
          | Xtc -> "xtc"
+         | Trs -> "trs"
          | RawCoq -> "raw_coq"
          | SttCoq -> "stt_coq")
     in

src/export/hrs.ml

@@ -21,7 +21,8 @@ Pattern variables of arity n are translated as variables of type t -> ... -> t
 
 - In the hrs format, variable names must be distinct from function symbol
    names. So bound variables are translated into positive integers and pattern
-   variables are prefixed by ["$"].
+   variables are prefixed by ["*"] (the character ["$"] is not accepted
+   by SOL).
 
 - There is no clash between function symbol names and A, B, L, P because
    function symbol names are fully qualified.
@@ -79,7 +80,7 @@ let add_bvar : tvar -> unit = fun v ->
 let bvar : tvar pp = fun ppf v -> int ppf (Bindlib.uid_of v)
 
 (** [pvar i] translates the pattern variable index [i]. *)
-let pvar : int pp = fun ppf i -> out ppf "$%d_%d" !nb_rules i
+let pvar : int pp = fun ppf i -> out ppf "*%d_%d" !nb_rules i
 
 (** [add_pvar i k] declares a pvar of index [i] and arity [k]. *)
 let add_pvar : int -> int -> unit = fun i k ->
@@ -151,15 +152,15 @@ let sign : Sign.t pp = fun ppf sign ->
   let pp_pvars = fun ppf pvars ->
     let typ : int pp = fun ppf k ->
       for _i=1 to k do string ppf "t -> " done; out ppf "t" in
-    let pvar_decl (n,i) k = out ppf "\n$%d_%d : %a" n i typ k in
+    let pvar_decl (n,i) k = out ppf "\n*%d_%d : %a" n i typ k in
     VMap.iter pvar_decl pvars in
   (* Function for printing the types of abstracted variables. *)
   let pp_bvars : IntSet.t pp = fun ppf bvars ->
     let bvar_decl : int pp = fun ppf n -> out ppf "\n%d : t" n in
     IntSet.iter (bvar_decl ppf) bvars
   in
-  (* Finally, generate the whole hrs file. Note that the variables $x, $y and
-     $z used in the rules for beta and let cannot clash with user-defined
+  (* Finally, generate the whole hrs file. Note that the variables *x, *y and
+     *z used in the rules for beta and let cannot clash with user-defined
      pattern variables which are integers. *)
   out ppf "\
 (FUN
@@ -169,11 +170,11 @@ P : t -> (t -> t) -> t
 B : t -> t -> (t -> t) -> t%a
 )
 (VAR
-$x : t
-$y : t -> t
-$z : t%a%a
+*x : t
+*y : t -> t
+*z : t%a%a
 )
 (RULES
-A(L($x,$y),$z) -> $y($z),
-B($x,$z,$y) -> $y($z)%s
+A(L(*x,*y),*z) -> *y(*z),
+B(*x,*z,*y) -> *y(*z)%s
 )\n" pp_syms !syms pp_pvars !pvars pp_bvars !bvars (Buffer.contents buf_rules)

src/export/trs.ml

@@ -0,0 +1,108 @@
+(** This module provides a function to translate a signature to the TRS format
+   used in the confluence competition.
+
+   This translation relies on the following fact: if in all rules l --> r of
+   the rewrite system both l and r are patterns, then the system is SN
+   whenever the first-order system obtained by forgeting about binders also
+   termintes. Note that because of this, we consider only termination without
+   the beta rule, as its right hand side is not a pattern.
+
+- Lambdapi terms are translated to a TRS over the following base signature:
+
+  A // binary symbol for application
+
+  L // binary symbol for λ
+
+  B // trinary symbol for let
+
+  P // binary symbol for Π
+
+- Function symbol names are fully qualified but ["."] is replaced by ["_"],
+   and metavariable names are printed unchanged (they do not clash with
+   function symbols because they start with ["$"]).
+
+TODO:
+
+- For the time being, we translate rules without verifying that the pattern
+   condition is always verified. In the future we should only translate the
+   fragment of the system that satisfy the pattern confition in both the lhs
+   and the rhs.
+
+*)
+
+open Lplib open Base open Extra
+open Common open Error
+open Core open Term
+
+(** [sym_name s] translates the symbol name of [s]. *)
+let sym_name : sym pp = fun ppf s ->
+  out ppf "%a_%s" (List.pp string "_") s.sym_path s.sym_name
+
+(** [pvar i] translates the pattern variable index [i]. *)
+let pvar : int pp = fun ppf i -> out ppf "$%d" i
+
+let max_var : int ref = ref 0
+
+let set_max_var : int -> unit = fun i ->
+  max_var := max i !max_var
+
+(** [term ppf t] translates the term [t]. *)
+let rec term : term pp = fun ppf t ->
+  match unfold t with
+  | Meta _ -> assert false
+  | Plac _ -> assert false
+  | TRef _ -> assert false
+  | TEnv _ -> assert false
+  | Wild -> assert false
+  | Kind -> assert false
+  | Type -> assert false
+  | Vari _ -> fatal_no_pos "This file cannot be interpreted as a TRS."
+  | Symb s -> sym_name ppf s
+  | Patt(None,_,_) -> assert false
+  | Patt(Some i,_,[||]) -> set_max_var i; pvar ppf i
+  | Patt(Some i,_,_) -> (* TODO: check it's only applied to bound vars*)
+    set_max_var i; pvar ppf i
+  | Appl(t,u) -> out ppf "A(%a, %a)" term t term u
+  | Abst(a,b) ->
+    let _, b = Bindlib.unbind b in
+    out ppf "L(%a, %a)" term a  term b
+  | Prod(a,b) ->
+    let _, b = Bindlib.unbind b in
+    out ppf "P(%a, %a)" term a  term b
+  | LLet(a,t,b) ->
+    let _, b = Bindlib.unbind b in
+    out ppf "B(%a,%a,%a)" term a term t term b
+
+(** [rule ppf r] translates the pair of terms [r] as a rule. *)
+let rule : (term * term) pp = fun ppf (l, r) ->
+  out ppf "\n%a -> %a" term l term r
+
+(** [sym_rule ppf s r] translates the sym_rule [r]. *)
+let sym_rule : sym -> rule pp = fun s ppf r ->
+  let sr = s, r in rule ppf (lhs sr, rhs sr)
+
+(** Translate the rules of symbol [s]. *)
+let rules_of_sym : sym pp = fun ppf s ->
+  match Timed.(!(s.sym_def)) with
+  | Some d -> rule ppf (mk_Symb s, d)
+  | None -> List.iter (sym_rule s ppf) Timed.(!(s.sym_rules))
+
+(** Translate the rules of a dependency except if it is a ghost signature. *)
+let rules_of_sign : Sign.t pp = fun ppf sign ->
+  if sign != Ghost.sign then
+    StrMap.iter (fun _ -> rules_of_sym ppf) Timed.(!(sign.sign_symbols))
+
+(** [sign ppf s] translates the Lambdapi signature [s]. *)
+let sign : Sign.t pp = fun ppf sign ->
+  (* First, generate the rules in a buffer, because it generates data
+     necessary for the other sections. *)
+  let buf_rules = Buffer.create 1000 in
+  let ppf_rules = Format.formatter_of_buffer buf_rules in
+  Sign.iterate (rules_of_sign ppf_rules) sign;
+  Format.pp_print_flush ppf_rules ();
+  let pp_vars : int pp = fun ppf k ->
+    for i = 0 to k do out ppf " $%d" i done in
+  out ppf "\
+(VAR%a)
+(RULES%s
+)\n" pp_vars !max_var (Buffer.contents buf_rules)

tests/regressions/hrs.expected

@@ -13,17 +13,17 @@ tests_OK_boolean_false : t
 tests_OK_boolean_true : t
 )
 (VAR
-$x : t
-$y : t -> t
-$z : t
-$1_0 : t
-$2_0 : t
-$3_0 : t
-$4_0 : t
-$7_0 : t
-$8_0 : t
-$9_0 : t
-$10_0 : t
+*x : t
+*y : t -> t
+*z : t
+*1_0 : t
+*2_0 : t
+*3_0 : t
+*4_0 : t
+*7_0 : t
+*8_0 : t
+*9_0 : t
+*10_0 : t
 82 : t
 83 : t
 84 : t
@@ -32,18 +32,18 @@ $10_0 : t
 87 : t
 )
 (RULES
-A(L($x,$y),$z) -> $y($z),
-B($x,$z,$y) -> $y($z),
-A(A(tests_OK_boolean_bool_and,tests_OK_boolean_true),$1_0) -> $1_0,
-A(A(tests_OK_boolean_bool_and,tests_OK_boolean_false),$2_0) -> tests_OK_boolean_false,
-A(A(tests_OK_boolean_bool_and,$3_0),tests_OK_boolean_true) -> $3_0,
-A(A(tests_OK_boolean_bool_and,$4_0),tests_OK_boolean_false) -> tests_OK_boolean_false,
+A(L(*x,*y),*z) -> *y(*z),
+B(*x,*z,*y) -> *y(*z),
+A(A(tests_OK_boolean_bool_and,tests_OK_boolean_true),*1_0) -> *1_0,
+A(A(tests_OK_boolean_bool_and,tests_OK_boolean_false),*2_0) -> tests_OK_boolean_false,
+A(A(tests_OK_boolean_bool_and,*3_0),tests_OK_boolean_true) -> *3_0,
+A(A(tests_OK_boolean_bool_and,*4_0),tests_OK_boolean_false) -> tests_OK_boolean_false,
 tests_OK_boolean_bool_impl -> L(tests_OK_boolean_B,\82.L(tests_OK_boolean_B,\83.A(A(tests_OK_boolean_bool_or,83),A(tests_OK_boolean_bool_neg,82)))),
 A(tests_OK_boolean_bool_neg,tests_OK_boolean_true) -> tests_OK_boolean_false,
 A(tests_OK_boolean_bool_neg,tests_OK_boolean_false) -> tests_OK_boolean_true,
-A(A(tests_OK_boolean_bool_or,tests_OK_boolean_true),$7_0) -> tests_OK_boolean_true,
-A(A(tests_OK_boolean_bool_or,tests_OK_boolean_false),$8_0) -> $8_0,
-A(A(tests_OK_boolean_bool_or,$9_0),tests_OK_boolean_true) -> tests_OK_boolean_true,
-A(A(tests_OK_boolean_bool_or,$10_0),tests_OK_boolean_false) -> $10_0,
+A(A(tests_OK_boolean_bool_or,tests_OK_boolean_true),*7_0) -> tests_OK_boolean_true,
+A(A(tests_OK_boolean_bool_or,tests_OK_boolean_false),*8_0) -> *8_0,
+A(A(tests_OK_boolean_bool_or,*9_0),tests_OK_boolean_true) -> tests_OK_boolean_true,
+A(A(tests_OK_boolean_bool_or,*10_0),tests_OK_boolean_false) -> *10_0,
 tests_OK_boolean_bool_xor -> L(tests_OK_boolean_B,\84.L(tests_OK_boolean_B,\85.B(tests_OK_boolean_B,A(A(tests_OK_boolean_bool_and,84),A(tests_OK_boolean_bool_neg,85)),\86.B(tests_OK_boolean_B,A(A(tests_OK_boolean_bool_and,85),A(tests_OK_boolean_bool_neg,84)),\87.A(A(tests_OK_boolean_bool_or,86),87)))))
 )