diff --git a/doc/options.rst b/doc/options.rst index bc5fea6f7..87d43ffd4 100644 --- a/doc/options.rst +++ b/doc/options.rst @@ -70,6 +70,7 @@ export - ``dk``: `Dedukti `__ format - ``hrs``: `HRS `__ format of the confluence competition - ``xtc``: `XTC `__ format of the termination competition + - ``sol``: format of the `SOL `__ confluence and termination checker - ``raw_coq``: `Coq `__ format - ``stt_coq``: `Coq `__ format assuming that the input file is in an encoding of simple type theory diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml index ff3b624c6..925ad1708 100644 --- a/src/cli/lambdapi.ml +++ b/src/cli/lambdapi.ml @@ -68,7 +68,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 | Sol | Xtc | RawCoq | SttCoq (** Running the export mode. *) let export_cmd (cfg:Config.t) (output:output option) (encoding:string option) @@ -85,6 +85,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 Sol -> + Export.Sol.sign Format.std_formatter (Compile.compile_file file) | Some Xtc -> Export.Xtc.sign Format.std_formatter (Compile.compile_file file) | Some RawCoq -> @@ -198,6 +200,7 @@ let output : output option CLT.t = | "lp" -> Ok Lp | "dk" -> Ok Dk | "hrs" -> Ok Hrs + | "sol" -> Ok Sol | "xtc" -> Ok Xtc | "raw_coq" -> Ok RawCoq | "stt_coq" -> Ok SttCoq @@ -209,6 +212,7 @@ let output : output option CLT.t = | Lp -> "lp" | Dk -> "dk" | Hrs -> "hrs" + | Sol -> "Sol" | Xtc -> "xtc" | RawCoq -> "raw_coq" | SttCoq -> "stt_coq") diff --git a/src/export/sol.ml b/src/export/sol.ml new file mode 100644 index 000000000..6aee99326 --- /dev/null +++ b/src/export/sol.ml @@ -0,0 +1,152 @@ +(** This module provides a function to translate a signature to the format + used by the SOL confluence and termination checker. + @see + +SOL allowed identifiers for types, function symbols, bound variables, rule +names: +- [0-9][a-zA-Z0-9_^'-!%/]* +- <[a-zA-Z0-9_^'-*+!%/]+ +- [a-z_-%][a-zA-Z0-9_^'-*+!%/]+ + +SOL allowed identifiers for metavariables: +- [A-Z][a-zA-Z0-9_^'-*!%/<>]* +*) + +open Lplib open Base open Extra +open Core open Term + +(** [syms] contains the set of symbols used in rules. *) +let syms = ref SymSet.empty + +(** [add_sym s] add [s] in [!syms] and [!eqths] if it has axioms. *) +let add_sym : sym -> unit = fun s -> syms := SymSet.add s !syms + +(** [sym s] translates the symbol [s]. *) +let sym : sym pp = fun ppf s -> + out ppf "%a_%s" (List.pp string "_") s.sym_path s.sym_name + +(** [bvar v] translates the bound variable [v]. *) +let bvar : tvar pp = fun ppf v -> out ppf "x%d" (Bindlib.uid_of v) + +(** [pvar i] translates the pattern variable of index [i]. *) +let pvar : int pp = fun ppf i -> out ppf "M%d" i + +(** [term ppf t] translates the term [t]. *) +let rec term : term pp = fun ppf t -> + match get_args t with + | Symb s, [] -> add_sym s; sym ppf s + | Symb s, ts -> add_sym s; out ppf "%a(%a)" sym s (List.pp term ",") ts + | _ -> raw_term ppf t + +and raw_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 _ -> assert false + | 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 "app(%a,%a)" term t term u + | Abst(_,b) -> + let x, b = Bindlib.unbind b in out ppf "(%a.%a)" bvar x term b + | Prod _ -> assert false + | LLet _ -> assert false + +(** [rule ppf r] translates the pair of terms [r] as a rule. *) +let rule : (term * term) pp = + let rule_nb = ref 0 in + fun ppf (l, r) -> + incr rule_nb; out ppf "\n (rule%d) %a => %a" !rule_nb term l term r + +(** [sym_rule s ppf r] translates the sym_rule [s,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 signature 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)) + +(** [typ ppf t] translates the type [t]. *) +let rec typ : term pp = fun ppf t -> + match unfold t with + | Prod(a,b) -> + if Bindlib.binder_constant b then + let _,b = Bindlib.unbind b in + out ppf "(%a -> %a)" typ a typ b + else assert false + | Symb s -> sym ppf s + | _ -> assert false + +(** [typ_decl t] translates the term [t] as a type declaration. *) +let rec typ_decl : term pp = fun ppf t -> + match unfold t with + | Prod(a,b) -> + if Bindlib.binder_constant b then + let _,b = Bindlib.unbind b in + out ppf "%a%a" typ a codomain b + else assert false + | Symb s -> sym ppf s + | _ -> assert false + +and codomain : term pp = fun ppf t -> + match unfold t with + | Prod(a,b) -> + if Bindlib.binder_constant b then + let _,b = Bindlib.unbind b in + out ppf ", %a%a" typ a codomain b + else assert false + | Symb s -> out ppf " -> %a" sym s + | _ -> assert false + +(** [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 declaring the types of function symbols. *) + let pp_syms : SymSet.t pp = fun ppf syms -> + let sym_decl : sym pp = fun ppf s -> + out ppf "\n %a : %a" sym s typ_decl Timed.(!(s.sym_type)) in + SymSet.iter (sym_decl ppf) syms + in + (* Function for declaring the axioms of function symbols. *) + let pp_axioms : SymSet.t pp = fun ppf syms -> + let rec prop s ppf p = + match p with + | Commu -> out ppf "\n (%a_com) %a(X,Y) = %a(Y,X)" sym s sym s sym s + | Assoc _ -> + out ppf "\n (%a_assoc) %a(%a(X,Y),Z) = %a(X,%a(Y,Z))" + sym s sym s sym s sym s sym s + | AC _ -> prop s ppf Commu; prop s ppf (Assoc true) + | _ -> () + in + SymSet.iter (fun s -> prop s ppf s.sym_prop) syms + in + out ppf "\ +sig = [signature| + app : (a -> b), a -> b%a +|] +rules = [rule| + (beta) app(x.M[x],N) => M[N]%s +|] +axioms = [axiom|%a +|]\n" pp_syms !syms (Buffer.contents buf_rules) pp_axioms !syms