From 9f0b399ee141651c04afa5a8ab9a5bf1eb2d40fd Mon Sep 17 00:00:00 2001 From: thiagofelicissimo Date: Fri, 19 Jan 2024 08:44:31 +0100 Subject: [PATCH 1/8] afsm export --- src/cli/lambdapi.ml | 8 ++- src/export/afsm.ml | 164 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 170 insertions(+), 2 deletions(-) create mode 100644 src/export/afsm.ml diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml index 9e3246a2d..986a6ec0e 100644 --- a/src/cli/lambdapi.ml +++ b/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 | Afsm | 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 Afsm -> + Export.Afsm.sign Format.std_formatter (Compile.compile_file file) | Some Xtc -> Export.Xtc.sign Format.std_formatter (Compile.compile_file file) | Some RawCoq -> @@ -229,8 +231,9 @@ let output : output option CLT.t = match s with | "lp" -> Ok Lp | "dk" -> Ok Dk - | "hrs" -> Ok Hrs + | "hrs" -> Ok Hrs | "xtc" -> Ok Xtc + | "afsm" -> Ok Afsm | "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" + | Afsm -> "afsm" | RawCoq -> "raw_coq" | SttCoq -> "stt_coq") in diff --git a/src/export/afsm.ml b/src/export/afsm.ml new file mode 100644 index 000000000..c63c4d663 --- /dev/null +++ b/src/export/afsm.ml @@ -0,0 +1,164 @@ +(** This module provides a function to translate a signature to the AFSM format + used by the Wanda termination checker. Note that because termination is + checked at the untyped level, Wanda will *always* answer NO, as we have an + untyped beta rule. However, by removing the beta rule we can sometimes show + termination of the rest of the system. This can be useful when showing + confluence of the system: by Von Oostrom's orthogonal combinations + criterion, if the system without beta is confluent, then by combining it + with beta it stays confluent. Thus, if the system without beta is weakly + confluent, then by checking its termination we can deduce the confluence + of the system with beta. + +- Lambdapi terms are translated to terms over the following base signature: + + A : t -> t -> t // for application + + L : t -> (t -> t) -> t // for λ + + B : t -> t -> (t -> t) -> t // for let + + P : t -> (t -> t) -> t // for Π + +Function symbols and variables are translated as symbols of type t. + +Pattern variables of arity n are translated as variables of type t -> ... -> t + with n times ->. + +- In the afsm format, variable names must be distinct from function symbol + names. So bound variables are translated into positive integers and pattern + variables are translated as XiNj where i is the number of the rule and j + is the indice of the variable. Function symbols are translated directly + by their unqualified names. If a function symbol name clashes with the + name of a variable, metavariable or a symbol declared in the base + signature, we prefix it with !. In order to do this, we assume that no + function symbol starts with !. + +- Unicode is translated as unicode, and Wanda does not accept it. We chose not + to implement a translation to their codes, as the output would be unreadable. + In this case, it is better if the user removes manually the unicode from their + file, this way they can chose a more readable replacement for the occuring + unicode characters. + *) + +open Lplib open Base open Extra +open Core open Term + +(** [syms] maps every symbol to a name. *) +let syms = ref SymMap.empty + +(** [nb_rules] is the number of rewrite rules. *) +let nb_rules = ref 0 + +let sanitize_name : string -> string = fun s -> + (* we considere names starting with '!' as forbiden, so we can + use it as an escape character to prevent clashes *) + if s.[0] = '!' then assert false; + match s with + | "A" | "L" | "P" | "B" -> + (* prevents clashes with the names in the base signature *) + "!" ^ s + | _ -> + (* prevent clashes metavariable names *) + if s.[0] = 'X' then "!" ^ s + (* prevent clashes with variable names, which are just numbers *) + else if Str.string_match (Str.regexp "[0-9]+$") s 0 then "!" ^ s + else s (* ok names *) + +(** [sym_name s] translates the symbol name of [s]. *) +let sym_name : sym pp = fun ppf s -> + out ppf "%s" (sanitize_name s.sym_name) + +(** [add_sym] declares a Lambdapi symbol. *) +let add_sym : sym -> unit = fun s -> + syms := SymMap.add s (Format.asprintf "%a" sym_name s) !syms + +(** [sym ppf s] translates the Lambdapi symbol [s]. *) +let sym : sym pp = fun ppf s -> string ppf (SymMap.find s !syms) + +(** [bvar v] translates the Lambdapi variable [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 "X%dN%d" !nb_rules i + +(** [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 v -> bvar ppf v + | Symb s -> add_sym s; sym ppf s + | Patt(None,_,_) -> assert false + | Patt(Some i,_,[||]) -> pvar ppf i + | Patt(Some i,_,ts) -> + let k = Array.length ts in + let args ppf ts = for i=1 to k-1 do out ppf ",%a" term ts.(i) done in + out ppf "%a[%a%a]" pvar i term ts.(0) args ts + | Appl(t,u) -> out ppf "A %a %a" term_safe t term_safe u + | Abst(a,b) -> + let x, b = Bindlib.unbind b in + out ppf "L %a (/\\%a.%a)" term_safe a bvar x term b + | Prod(a,b) -> + let x, b = Bindlib.unbind b in + out ppf "P %a (/\\%a.%a)" term_safe a bvar x term b + | LLet(a,t,b) -> + let x, b = Bindlib.unbind b in + out ppf "B %a %a (/\\%a.%a)" term_safe a term_safe t bvar x term b +and term_safe : term pp = fun ppf t -> + match unfold t with + | Vari v -> bvar ppf v + | Symb s -> add_sym s; sym ppf s + | Patt(Some i,_,[||]) -> pvar ppf i + | Patt(Some i,_,ts) -> + let k = Array.length ts in + let args ppf ts = for i=1 to k-1 do out ppf ",%a" term ts.(i) done in + out ppf "%a[%a%a]" pvar i term ts.(0) args ts + | _ -> out ppf "(%a)" term t + +(** [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] increases the number of rules and translates the + sym_rule [r]. *) +let sym_rule : sym -> rule pp = fun s ppf r -> + incr nb_rules; 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 (); + (* Function for printing the types of function symbols. *) + let pp_syms : string SymMap.t pp = fun ppf syms -> + let sym_decl : string pp = fun ppf n -> out ppf "\n%s : t" n in + let sym_decl _ n = sym_decl ppf n in SymMap.iter sym_decl syms + in + out ppf "\ +A : t -> t -> t +L : t -> (t -> t) -> t +P : t -> (t -> t) -> t +B : t -> t -> (t -> t) -> t%a + +A (L V Y) Z => Y Z +B V Z Y => Y Z%s +\n" pp_syms !syms (Buffer.contents buf_rules) From 8c9450cb73532450ee45545823c14ba7d5039d48 Mon Sep 17 00:00:00 2001 From: thiagofelicissimo Date: Fri, 19 Jan 2024 09:19:05 +0100 Subject: [PATCH 2/8] trs export --- src/cli/lambdapi.ml | 10 ++-- src/export/trs.ml | 119 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 126 insertions(+), 3 deletions(-) create mode 100644 src/export/trs.ml diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml index 986a6ec0e..efc5fb874 100644 --- a/src/cli/lambdapi.ml +++ b/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 | Afsm | RawCoq | SttCoq +type output = Lp | Dk | Hrs | Xtc | Afsm | Trs | RawCoq | SttCoq (** Running the export mode. *) let export_cmd (cfg:Config.t) (output:output option) (encoding:string option) @@ -118,7 +118,9 @@ let export_cmd (cfg:Config.t) (output:output option) (encoding:string option) | Some Hrs -> Export.Hrs.sign Format.std_formatter (Compile.compile_file file) | Some Afsm -> - Export.Afsm.sign Format.std_formatter (Compile.compile_file file) + Export.Afsm.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 -> @@ -233,7 +235,8 @@ let output : output option CLT.t = | "dk" -> Ok Dk | "hrs" -> Ok Hrs | "xtc" -> Ok Xtc - | "afsm" -> Ok Afsm + | "afsm" -> Ok Afsm + | "trs" -> Ok Trs | "raw_coq" -> Ok RawCoq | "stt_coq" -> Ok SttCoq | _ -> Error(`Msg "Invalid format") @@ -246,6 +249,7 @@ let output : output option CLT.t = | Hrs -> "hrs" | Xtc -> "xtc" | Afsm -> "afsm" + | Trs -> "trs" | RawCoq -> "raw_coq" | SttCoq -> "stt_coq") in diff --git a/src/export/trs.ml b/src/export/trs.ml new file mode 100644 index 000000000..70f2ac19d --- /dev/null +++ b/src/export/trs.ml @@ -0,0 +1,119 @@ +(** 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 symbols are translated directly by their unqualified names. If a + function symbol name clashes with the name of a variable, metavariable or + a symbol declared in the base signature, we prefix it with !. In order to + do this, we assume that no function symbol starts 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 Core open Term + +let sanitize_name : string -> string = fun s -> + (* we considere names starting with '!' as forbiden, so we can + use it as an escape character to prevent clashes *) + if s.[0] = '!' then assert false; + match s with + | "A" | "L" | "P" | "B" -> + (* prevents clashes with the names in the base signature *) + "!" ^ s + | _ -> s + +(** [sym_name s] translates the symbol name of [s]. *) +let sym_name : sym pp = fun ppf s -> + out ppf "%s" (sanitize_name 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 _ -> assert false + | 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) From f284e2f2bf40669c9e73721637f2791ee4ecaeca Mon Sep 17 00:00:00 2001 From: thiagofelicissimo Date: Fri, 19 Jan 2024 09:33:34 +0100 Subject: [PATCH 3/8] removes trailing spaces --- src/cli/lambdapi.ml | 2 +- src/export/afsm.ml | 54 ++++++++++++++++++++++----------------------- src/export/trs.ml | 40 ++++++++++++++++----------------- 3 files changed, 48 insertions(+), 48 deletions(-) diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml index efc5fb874..e53b1cfae 100644 --- a/src/cli/lambdapi.ml +++ b/src/cli/lambdapi.ml @@ -233,7 +233,7 @@ let output : output option CLT.t = match s with | "lp" -> Ok Lp | "dk" -> Ok Dk - | "hrs" -> Ok Hrs + | "hrs" -> Ok Hrs | "xtc" -> Ok Xtc | "afsm" -> Ok Afsm | "trs" -> Ok Trs diff --git a/src/export/afsm.ml b/src/export/afsm.ml index c63c4d663..016e9ec9a 100644 --- a/src/export/afsm.ml +++ b/src/export/afsm.ml @@ -1,13 +1,13 @@ -(** This module provides a function to translate a signature to the AFSM format - used by the Wanda termination checker. Note that because termination is - checked at the untyped level, Wanda will *always* answer NO, as we have an - untyped beta rule. However, by removing the beta rule we can sometimes show - termination of the rest of the system. This can be useful when showing - confluence of the system: by Von Oostrom's orthogonal combinations - criterion, if the system without beta is confluent, then by combining it - with beta it stays confluent. Thus, if the system without beta is weakly - confluent, then by checking its termination we can deduce the confluence - of the system with beta. +(** This module provides a function to translate a signature to the AFSM + format used by the Wanda termination checker. Note that because + termination is checked at the untyped level, Wanda will *always* answer NO, + as we have an untyped beta rule. However, by removing the beta rule we can + sometimes show termination of the rest of the system. This can be useful + when showing confluence of the system: by Von Oostrom's orthogonal + combinations criterion, if the system without beta is confluent, then by + combining it with beta it stays confluent. Thus, if the system without beta + is weakly confluent, then by checking its termination we can deduce the + confluence of the system with beta. - Lambdapi terms are translated to terms over the following base signature: @@ -28,16 +28,16 @@ Pattern variables of arity n are translated as variables of type t -> ... -> t names. So bound variables are translated into positive integers and pattern variables are translated as XiNj where i is the number of the rule and j is the indice of the variable. Function symbols are translated directly - by their unqualified names. If a function symbol name clashes with the - name of a variable, metavariable or a symbol declared in the base - signature, we prefix it with !. In order to do this, we assume that no + by their unqualified names. If a function symbol name clashes with the + name of a variable, metavariable or a symbol declared in the base + signature, we prefix it with !. In order to do this, we assume that no function symbol starts with !. - Unicode is translated as unicode, and Wanda does not accept it. We chose not - to implement a translation to their codes, as the output would be unreadable. - In this case, it is better if the user removes manually the unicode from their - file, this way they can chose a more readable replacement for the occuring - unicode characters. + to implement a translation to their codes, as the output would be + unreadable. In this case, it is better if the user removes manually the + unicode from their file, this way they can chose a more readable + replacement for the occuring unicode characters. *) open Lplib open Base open Extra @@ -49,19 +49,19 @@ let syms = ref SymMap.empty (** [nb_rules] is the number of rewrite rules. *) let nb_rules = ref 0 -let sanitize_name : string -> string = fun s -> +let sanitize_name : string -> string = fun s -> (* we considere names starting with '!' as forbiden, so we can use it as an escape character to prevent clashes *) if s.[0] = '!' then assert false; - match s with - | "A" | "L" | "P" | "B" -> + match s with + | "A" | "L" | "P" | "B" -> (* prevents clashes with the names in the base signature *) - "!" ^ s - | _ -> + "!" ^ s + | _ -> (* prevent clashes metavariable names *) - if s.[0] = 'X' then "!" ^ s + if s.[0] = 'X' then "!" ^ s (* prevent clashes with variable names, which are just numbers *) - else if Str.string_match (Str.regexp "[0-9]+$") s 0 then "!" ^ s + else if Str.string_match (Str.regexp "[0-9]+$") s 0 then "!" ^ s else s (* ok names *) (** [sym_name s] translates the symbol name of [s]. *) @@ -109,7 +109,7 @@ let rec term : term pp = fun ppf t -> | LLet(a,t,b) -> let x, b = Bindlib.unbind b in out ppf "B %a %a (/\\%a.%a)" term_safe a term_safe t bvar x term b -and term_safe : term pp = fun ppf t -> +and term_safe : term pp = fun ppf t -> match unfold t with | Vari v -> bvar ppf v | Symb s -> add_sym s; sym ppf s @@ -117,7 +117,7 @@ and term_safe : term pp = fun ppf t -> | Patt(Some i,_,ts) -> let k = Array.length ts in let args ppf ts = for i=1 to k-1 do out ppf ",%a" term ts.(i) done in - out ppf "%a[%a%a]" pvar i term ts.(0) args ts + out ppf "%a[%a%a]" pvar i term ts.(0) args ts | _ -> out ppf "(%a)" term t (** [rule ppf r] translates the pair of terms [r] as a rule. *) @@ -152,7 +152,7 @@ let sign : Sign.t pp = fun ppf sign -> let pp_syms : string SymMap.t pp = fun ppf syms -> let sym_decl : string pp = fun ppf n -> out ppf "\n%s : t" n in let sym_decl _ n = sym_decl ppf n in SymMap.iter sym_decl syms - in + in out ppf "\ A : t -> t -> t L : t -> (t -> t) -> t diff --git a/src/export/trs.ml b/src/export/trs.ml index 70f2ac19d..ba482b2a0 100644 --- a/src/export/trs.ml +++ b/src/export/trs.ml @@ -2,10 +2,10 @@ 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. + 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: @@ -17,33 +17,33 @@ P // binary symbol for Π -- Function symbols are translated directly by their unqualified names. If a +- Function symbols are translated directly by their unqualified names. If a function symbol name clashes with the name of a variable, metavariable or a symbol declared in the base signature, we prefix it with !. In order to do this, we assume that no function symbol starts with !. -TODO: +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. -- 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 Core open Term -let sanitize_name : string -> string = fun s -> +let sanitize_name : string -> string = fun s -> (* we considere names starting with '!' as forbiden, so we can use it as an escape character to prevent clashes *) if s.[0] = '!' then assert false; - match s with - | "A" | "L" | "P" | "B" -> + match s with + | "A" | "L" | "P" | "B" -> (* prevents clashes with the names in the base signature *) - "!" ^ s + "!" ^ s | _ -> s - + (** [sym_name s] translates the symbol name of [s]. *) let sym_name : sym pp = fun ppf s -> out ppf "%s" (sanitize_name s.sym_name) @@ -71,7 +71,7 @@ let rec term : term pp = fun ppf t -> | 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 + 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 @@ -81,7 +81,7 @@ let rec term : term pp = fun ppf t -> 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 + 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) -> @@ -110,8 +110,8 @@ let sign : Sign.t pp = fun ppf sign -> 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 + 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 From 150ebc77bcebb90fcdbeef1a496b2eb71ebd69de Mon Sep 17 00:00:00 2001 From: thiagofelicissimo Date: Sat, 20 Jan 2024 12:32:35 +0100 Subject: [PATCH 4/8] improvements in hrs export --- src/export/hrs.ml | 54 +++++++++++++++++++++++++++-------------------- 1 file changed, 31 insertions(+), 23 deletions(-) diff --git a/src/export/hrs.ml b/src/export/hrs.ml index 899232b21..66d7430d2 100644 --- a/src/export/hrs.ml +++ b/src/export/hrs.ml @@ -19,16 +19,13 @@ Function symbols and variables are translated as symbols of type t. Pattern variables of arity n are translated as variables of type t -> ... -> t with n times ->. -- 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 ["$"]. - -- There is no clash between function symbol names and A, B, L, P because - function symbol names are fully qualified. - -- Function symbol names are fully qualified but ["."] is replaced by ["_"] - because ["."] cannot be used in identifiers (["."] is used in lambda - abstractions). +- Bound variables are translated into positive integers and pattern + variables are translated as XiNj where i is the number of the rule and j + is the indice of the variable. Function symbols are translated directly + by their unqualified names. If a function symbol name clashes with the + name of a variable, metavariable or a symbol declared in the base + signature, we prefix it with !. In order to do this, we assume that no + function symbol starts with !. - Two occurrences of the same pattern variable name may have two different arities (in two different rules). So pattern variable names are prefixed by @@ -36,8 +33,6 @@ Pattern variables of arity n are translated as variables of type t -> ... -> t TO DO: -- HRS does not accept unicode characters. - - Optim: output only the symbols used in the rules. *) open Lplib open Base open Extra @@ -60,9 +55,24 @@ end module VMap = Map.Make(V) let pvars = ref VMap.empty +let sanitize_name : string -> string = fun s -> + (* we considere names starting with '!' as forbiden, so we can + use it as an escape character to prevent clashes *) + if s.[0] = '!' then assert false; + match s with + | "A" | "L" | "P" | "B" -> + (* prevents clashes with the names in the base signature *) + "!" ^ s + | _ -> + (* prevent clashes metavariable names *) + if s.[0] = 'X' then "!" ^ s + (* prevent clashes with variable names, which are just numbers *) + else if Str.string_match (Str.regexp "[0-9]+$") s 0 then "!" ^ s + else s (* ok names *) + (** [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 + out ppf "%s" (sanitize_name s.sym_name) (** [add_sym] declares a Lambdapi symbol. *) let add_sym : sym -> unit = fun s -> @@ -79,7 +89,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 "X%dN%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,16 +161,14 @@ 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 "\nX%dN%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 - pattern variables which are integers. *) + (* Finally, generate the whole hrs file. *) out ppf "\ (FUN A : t -> t -> t @@ -169,11 +177,11 @@ P : t -> (t -> t) -> t B : t -> t -> (t -> t) -> t%a ) (VAR -$x : t -$y : t -> t -$z : t%a%a +X0 : t +X1 : t -> t +X2 : t%a%a ) (RULES -A(L($x,$y),$z) -> $y($z), -B($x,$z,$y) -> $y($z)%s +A(L(X0,X1),X2) -> X1(X2), +B(X0,X2,X1) -> X1(X2)%s )\n" pp_syms !syms pp_pvars !pvars pp_bvars !bvars (Buffer.contents buf_rules) From 4dad34ef99b94f330fefa5036e3f04774229c5e5 Mon Sep 17 00:00:00 2001 From: thiagofelicissimo Date: Sun, 21 Jan 2024 17:49:48 +0100 Subject: [PATCH 5/8] detail --- src/export/trs.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/export/trs.ml b/src/export/trs.ml index ba482b2a0..15e82c525 100644 --- a/src/export/trs.ml +++ b/src/export/trs.ml @@ -114,6 +114,5 @@ let sign : Sign.t pp = fun ppf sign -> for i = 0 to k do out ppf " $%d" i done in out ppf "\ (VAR%a) -(RULES -%s +(RULES%s )\n" pp_vars !max_var (Buffer.contents buf_rules) From a004b82deac74b8f16946d4c5c04bcb52ca0f1de Mon Sep 17 00:00:00 2001 From: thiagofelicissimo Date: Mon, 22 Jan 2024 10:52:59 +0100 Subject: [PATCH 6/8] updates hrs regression --- tests/regressions/hrs.expected | 66 +++++++++++++++++----------------- 1 file changed, 33 insertions(+), 33 deletions(-) diff --git a/tests/regressions/hrs.expected b/tests/regressions/hrs.expected index f3dc68acd..9f7f7e986 100644 --- a/tests/regressions/hrs.expected +++ b/tests/regressions/hrs.expected @@ -3,27 +3,27 @@ A : t -> t -> t L : t -> (t -> t) -> t P : t -> (t -> t) -> t B : t -> t -> (t -> t) -> t -tests_OK_boolean_B : t -tests_OK_boolean_bool_and : t -tests_OK_boolean_bool_impl : t -tests_OK_boolean_bool_neg : t -tests_OK_boolean_bool_or : t -tests_OK_boolean_bool_xor : t -tests_OK_boolean_false : t -tests_OK_boolean_true : t +!B : t +bool_and : t +bool_impl : t +bool_neg : t +bool_or : t +bool_xor : t +false : t +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 +X0 : t +X1 : t -> t +X2 : t +X1N0 : t +X2N0 : t +X3N0 : t +X4N0 : t +X7N0 : t +X8N0 : t +X9N0 : t +X10N0 : 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,$1_0),tests_OK_boolean_false) -> tests_OK_boolean_false, -A(A(tests_OK_boolean_bool_and,$2_0),tests_OK_boolean_true) -> $2_0, -A(A(tests_OK_boolean_bool_and,tests_OK_boolean_false),$3_0) -> tests_OK_boolean_false, -A(A(tests_OK_boolean_bool_and,tests_OK_boolean_true),$4_0) -> $4_0, -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_false) -> tests_OK_boolean_true, -A(tests_OK_boolean_bool_neg,tests_OK_boolean_true) -> tests_OK_boolean_false, -A(A(tests_OK_boolean_bool_or,$7_0),tests_OK_boolean_false) -> $7_0, -A(A(tests_OK_boolean_bool_or,$8_0),tests_OK_boolean_true) -> tests_OK_boolean_true, -A(A(tests_OK_boolean_bool_or,tests_OK_boolean_false),$9_0) -> $9_0, -A(A(tests_OK_boolean_bool_or,tests_OK_boolean_true),$10_0) -> tests_OK_boolean_true, -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))))) +A(L(X0,X1),X2) -> X1(X2), +B(X0,X2,X1) -> X1(X2), +A(A(bool_and,X1N0),false) -> false, +A(A(bool_and,X2N0),true) -> X2N0, +A(A(bool_and,false),X3N0) -> false, +A(A(bool_and,true),X4N0) -> X4N0, +bool_impl -> L(!B,\82.L(!B,\83.A(A(bool_or,83),A(bool_neg,82)))), +A(bool_neg,false) -> true, +A(bool_neg,true) -> false, +A(A(bool_or,X7N0),false) -> X7N0, +A(A(bool_or,X8N0),true) -> true, +A(A(bool_or,false),X9N0) -> X9N0, +A(A(bool_or,true),X10N0) -> true, +bool_xor -> L(!B,\84.L(!B,\85.B(!B,A(A(bool_and,84),A(bool_neg,85)),\86.B(!B,A(A(bool_and,85),A(bool_neg,84)),\87.A(A(bool_or,86),87))))) ) From 6aaa545c3c07dc23cc5fa35fb59cf443007d3ec5 Mon Sep 17 00:00:00 2001 From: thiagofelicissimo Date: Tue, 6 Feb 2024 10:06:22 +0100 Subject: [PATCH 7/8] does not print beta and let rules in afsm export --- src/export/afsm.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/export/afsm.ml b/src/export/afsm.ml index 016e9ec9a..50d5ba470 100644 --- a/src/export/afsm.ml +++ b/src/export/afsm.ml @@ -158,7 +158,5 @@ A : t -> t -> t L : t -> (t -> t) -> t P : t -> (t -> t) -> t B : t -> t -> (t -> t) -> t%a - -A (L V Y) Z => Y Z -B V Z Y => Y Z%s +%s \n" pp_syms !syms (Buffer.contents buf_rules) From 9bee3be398b341df21da72bba219dc6e0b724b20 Mon Sep 17 00:00:00 2001 From: thiagofelicissimo Date: Tue, 6 Feb 2024 11:19:53 +0100 Subject: [PATCH 8/8] puts back qualitifed names + removes afsm + prefixes pattern variables with * --- src/cli/lambdapi.ml | 6 +- src/export/afsm.ml | 162 --------------------------------- src/export/hrs.ml | 55 +++++------ src/export/trs.ml | 24 ++--- tests/regressions/hrs.expected | 66 +++++++------- 5 files changed, 65 insertions(+), 248 deletions(-) delete mode 100644 src/export/afsm.ml diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml index e53b1cfae..58af0e0e7 100644 --- a/src/cli/lambdapi.ml +++ b/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 | Afsm | Trs | 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,8 +117,6 @@ 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 Afsm -> - Export.Afsm.sign Format.std_formatter (Compile.compile_file file) | Some Trs -> Export.Trs.sign Format.std_formatter (Compile.compile_file file) | Some Xtc -> @@ -235,7 +233,6 @@ let output : output option CLT.t = | "dk" -> Ok Dk | "hrs" -> Ok Hrs | "xtc" -> Ok Xtc - | "afsm" -> Ok Afsm | "trs" -> Ok Trs | "raw_coq" -> Ok RawCoq | "stt_coq" -> Ok SttCoq @@ -248,7 +245,6 @@ let output : output option CLT.t = | Dk -> "dk" | Hrs -> "hrs" | Xtc -> "xtc" - | Afsm -> "afsm" | Trs -> "trs" | RawCoq -> "raw_coq" | SttCoq -> "stt_coq") diff --git a/src/export/afsm.ml b/src/export/afsm.ml deleted file mode 100644 index 50d5ba470..000000000 --- a/src/export/afsm.ml +++ /dev/null @@ -1,162 +0,0 @@ -(** This module provides a function to translate a signature to the AFSM - format used by the Wanda termination checker. Note that because - termination is checked at the untyped level, Wanda will *always* answer NO, - as we have an untyped beta rule. However, by removing the beta rule we can - sometimes show termination of the rest of the system. This can be useful - when showing confluence of the system: by Von Oostrom's orthogonal - combinations criterion, if the system without beta is confluent, then by - combining it with beta it stays confluent. Thus, if the system without beta - is weakly confluent, then by checking its termination we can deduce the - confluence of the system with beta. - -- Lambdapi terms are translated to terms over the following base signature: - - A : t -> t -> t // for application - - L : t -> (t -> t) -> t // for λ - - B : t -> t -> (t -> t) -> t // for let - - P : t -> (t -> t) -> t // for Π - -Function symbols and variables are translated as symbols of type t. - -Pattern variables of arity n are translated as variables of type t -> ... -> t - with n times ->. - -- In the afsm format, variable names must be distinct from function symbol - names. So bound variables are translated into positive integers and pattern - variables are translated as XiNj where i is the number of the rule and j - is the indice of the variable. Function symbols are translated directly - by their unqualified names. If a function symbol name clashes with the - name of a variable, metavariable or a symbol declared in the base - signature, we prefix it with !. In order to do this, we assume that no - function symbol starts with !. - -- Unicode is translated as unicode, and Wanda does not accept it. We chose not - to implement a translation to their codes, as the output would be - unreadable. In this case, it is better if the user removes manually the - unicode from their file, this way they can chose a more readable - replacement for the occuring unicode characters. - *) - -open Lplib open Base open Extra -open Core open Term - -(** [syms] maps every symbol to a name. *) -let syms = ref SymMap.empty - -(** [nb_rules] is the number of rewrite rules. *) -let nb_rules = ref 0 - -let sanitize_name : string -> string = fun s -> - (* we considere names starting with '!' as forbiden, so we can - use it as an escape character to prevent clashes *) - if s.[0] = '!' then assert false; - match s with - | "A" | "L" | "P" | "B" -> - (* prevents clashes with the names in the base signature *) - "!" ^ s - | _ -> - (* prevent clashes metavariable names *) - if s.[0] = 'X' then "!" ^ s - (* prevent clashes with variable names, which are just numbers *) - else if Str.string_match (Str.regexp "[0-9]+$") s 0 then "!" ^ s - else s (* ok names *) - -(** [sym_name s] translates the symbol name of [s]. *) -let sym_name : sym pp = fun ppf s -> - out ppf "%s" (sanitize_name s.sym_name) - -(** [add_sym] declares a Lambdapi symbol. *) -let add_sym : sym -> unit = fun s -> - syms := SymMap.add s (Format.asprintf "%a" sym_name s) !syms - -(** [sym ppf s] translates the Lambdapi symbol [s]. *) -let sym : sym pp = fun ppf s -> string ppf (SymMap.find s !syms) - -(** [bvar v] translates the Lambdapi variable [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 "X%dN%d" !nb_rules i - -(** [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 v -> bvar ppf v - | Symb s -> add_sym s; sym ppf s - | Patt(None,_,_) -> assert false - | Patt(Some i,_,[||]) -> pvar ppf i - | Patt(Some i,_,ts) -> - let k = Array.length ts in - let args ppf ts = for i=1 to k-1 do out ppf ",%a" term ts.(i) done in - out ppf "%a[%a%a]" pvar i term ts.(0) args ts - | Appl(t,u) -> out ppf "A %a %a" term_safe t term_safe u - | Abst(a,b) -> - let x, b = Bindlib.unbind b in - out ppf "L %a (/\\%a.%a)" term_safe a bvar x term b - | Prod(a,b) -> - let x, b = Bindlib.unbind b in - out ppf "P %a (/\\%a.%a)" term_safe a bvar x term b - | LLet(a,t,b) -> - let x, b = Bindlib.unbind b in - out ppf "B %a %a (/\\%a.%a)" term_safe a term_safe t bvar x term b -and term_safe : term pp = fun ppf t -> - match unfold t with - | Vari v -> bvar ppf v - | Symb s -> add_sym s; sym ppf s - | Patt(Some i,_,[||]) -> pvar ppf i - | Patt(Some i,_,ts) -> - let k = Array.length ts in - let args ppf ts = for i=1 to k-1 do out ppf ",%a" term ts.(i) done in - out ppf "%a[%a%a]" pvar i term ts.(0) args ts - | _ -> out ppf "(%a)" term t - -(** [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] increases the number of rules and translates the - sym_rule [r]. *) -let sym_rule : sym -> rule pp = fun s ppf r -> - incr nb_rules; 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 (); - (* Function for printing the types of function symbols. *) - let pp_syms : string SymMap.t pp = fun ppf syms -> - let sym_decl : string pp = fun ppf n -> out ppf "\n%s : t" n in - let sym_decl _ n = sym_decl ppf n in SymMap.iter sym_decl syms - in - out ppf "\ -A : t -> t -> t -L : t -> (t -> t) -> t -P : t -> (t -> t) -> t -B : t -> t -> (t -> t) -> t%a -%s -\n" pp_syms !syms (Buffer.contents buf_rules) diff --git a/src/export/hrs.ml b/src/export/hrs.ml index 66d7430d2..9e62c282f 100644 --- a/src/export/hrs.ml +++ b/src/export/hrs.ml @@ -19,13 +19,17 @@ Function symbols and variables are translated as symbols of type t. Pattern variables of arity n are translated as variables of type t -> ... -> t with n times ->. -- Bound variables are translated into positive integers and pattern - variables are translated as XiNj where i is the number of the rule and j - is the indice of the variable. Function symbols are translated directly - by their unqualified names. If a function symbol name clashes with the - name of a variable, metavariable or a symbol declared in the base - signature, we prefix it with !. In order to do this, we assume that no - function symbol starts with !. +- 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 ["*"] (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. + +- Function symbol names are fully qualified but ["."] is replaced by ["_"] + because ["."] cannot be used in identifiers (["."] is used in lambda + abstractions). - Two occurrences of the same pattern variable name may have two different arities (in two different rules). So pattern variable names are prefixed by @@ -33,6 +37,8 @@ Pattern variables of arity n are translated as variables of type t -> ... -> t TO DO: +- HRS does not accept unicode characters. + - Optim: output only the symbols used in the rules. *) open Lplib open Base open Extra @@ -55,24 +61,9 @@ end module VMap = Map.Make(V) let pvars = ref VMap.empty -let sanitize_name : string -> string = fun s -> - (* we considere names starting with '!' as forbiden, so we can - use it as an escape character to prevent clashes *) - if s.[0] = '!' then assert false; - match s with - | "A" | "L" | "P" | "B" -> - (* prevents clashes with the names in the base signature *) - "!" ^ s - | _ -> - (* prevent clashes metavariable names *) - if s.[0] = 'X' then "!" ^ s - (* prevent clashes with variable names, which are just numbers *) - else if Str.string_match (Str.regexp "[0-9]+$") s 0 then "!" ^ s - else s (* ok names *) - (** [sym_name s] translates the symbol name of [s]. *) let sym_name : sym pp = fun ppf s -> - out ppf "%s" (sanitize_name s.sym_name) + out ppf "%a_%s" (List.pp string "_") s.sym_path s.sym_name (** [add_sym] declares a Lambdapi symbol. *) let add_sym : sym -> unit = fun s -> @@ -89,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 "X%dN%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 -> @@ -161,14 +152,16 @@ 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 "\nX%dN%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. *) + (* 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 A : t -> t -> t @@ -177,11 +170,11 @@ P : t -> (t -> t) -> t B : t -> t -> (t -> t) -> t%a ) (VAR -X0 : t -X1 : t -> t -X2 : t%a%a +*x : t +*y : t -> t +*z : t%a%a ) (RULES -A(L(X0,X1),X2) -> X1(X2), -B(X0,X2,X1) -> X1(X2)%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) diff --git a/src/export/trs.ml b/src/export/trs.ml index 15e82c525..bba518a06 100644 --- a/src/export/trs.ml +++ b/src/export/trs.ml @@ -17,10 +17,9 @@ P // binary symbol for Π -- Function symbols are translated directly by their unqualified names. If a - function symbol name clashes with the name of a variable, metavariable or - a symbol declared in the base signature, we prefix it with !. In order to - do this, we assume that no function symbol starts with !. +- 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: @@ -32,21 +31,12 @@ TODO: *) open Lplib open Base open Extra +open Common open Error open Core open Term -let sanitize_name : string -> string = fun s -> - (* we considere names starting with '!' as forbiden, so we can - use it as an escape character to prevent clashes *) - if s.[0] = '!' then assert false; - match s with - | "A" | "L" | "P" | "B" -> - (* prevents clashes with the names in the base signature *) - "!" ^ s - | _ -> s - (** [sym_name s] translates the symbol name of [s]. *) let sym_name : sym pp = fun ppf s -> - out ppf "%s" (sanitize_name s.sym_name) + 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 @@ -66,11 +56,11 @@ let rec term : term pp = fun ppf t -> | Wild -> assert false | Kind -> assert false | Type -> assert false - | Vari _ -> 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*) + | 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) -> diff --git a/tests/regressions/hrs.expected b/tests/regressions/hrs.expected index 9f7f7e986..83e5f4e8f 100644 --- a/tests/regressions/hrs.expected +++ b/tests/regressions/hrs.expected @@ -3,27 +3,27 @@ A : t -> t -> t L : t -> (t -> t) -> t P : t -> (t -> t) -> t B : t -> t -> (t -> t) -> t -!B : t -bool_and : t -bool_impl : t -bool_neg : t -bool_or : t -bool_xor : t -false : t -true : t +tests_OK_boolean_B : t +tests_OK_boolean_bool_and : t +tests_OK_boolean_bool_impl : t +tests_OK_boolean_bool_neg : t +tests_OK_boolean_bool_or : t +tests_OK_boolean_bool_xor : t +tests_OK_boolean_false : t +tests_OK_boolean_true : t ) (VAR -X0 : t -X1 : t -> t -X2 : t -X1N0 : t -X2N0 : t -X3N0 : t -X4N0 : t -X7N0 : t -X8N0 : t -X9N0 : t -X10N0 : 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 @@ X10N0 : t 87 : t ) (RULES -A(L(X0,X1),X2) -> X1(X2), -B(X0,X2,X1) -> X1(X2), -A(A(bool_and,X1N0),false) -> false, -A(A(bool_and,X2N0),true) -> X2N0, -A(A(bool_and,false),X3N0) -> false, -A(A(bool_and,true),X4N0) -> X4N0, -bool_impl -> L(!B,\82.L(!B,\83.A(A(bool_or,83),A(bool_neg,82)))), -A(bool_neg,false) -> true, -A(bool_neg,true) -> false, -A(A(bool_or,X7N0),false) -> X7N0, -A(A(bool_or,X8N0),true) -> true, -A(A(bool_or,false),X9N0) -> X9N0, -A(A(bool_or,true),X10N0) -> true, -bool_xor -> L(!B,\84.L(!B,\85.B(!B,A(A(bool_and,84),A(bool_neg,85)),\86.B(!B,A(A(bool_and,85),A(bool_neg,84)),\87.A(A(bool_or,86),87))))) +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, +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))))) )