puts back qualitifed names + removes afsm + prefixes pattern variable…

…s with *

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

src/export/hrs.ml

@@ -19,20 +19,26 @@ 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
    the rule number.
 
 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)

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) ->