diff --git a/CHANGES.md b/CHANGES.md index 415a31503..e0782c298 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -3,6 +3,12 @@ All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/), and this project adheres to [Semantic Versioning](https://semver.org/). +## Unreleased + +### Added + +- add export format `raw_dk` + ## 2.5.0 (2024-02-25) ### Added diff --git a/Makefile b/Makefile index e7d106cbc..c97110fef 100644 --- a/Makefile +++ b/Makefile @@ -31,6 +31,7 @@ tests: lambdapi @dune exec --only-packages lambdapi -- tests/dtrees.sh @dune exec --only-packages lambdapi -- tests/export_dk.sh @dune exec --only-packages lambdapi -- tests/export_lp.sh + @dune exec --only-packages lambdapi -- tests/export_raw_dk.sh .PHONY: tests_alt_ergo tests_alt_ergo: lambdapi @@ -169,4 +170,3 @@ uninstall_vim_mode: .PHONY: build-vscode-extension build-vscode-extension: cd editors/vscode && make && mkdir extensionFolder && vsce package -o extensionFolder - diff --git a/doc/about.rst b/doc/about.rst index 3e051604e..127b09515 100644 --- a/doc/about.rst +++ b/doc/about.rst @@ -10,15 +10,23 @@ This allows to simplify some proofs, and formalize complex mathematical objects that are otherwise impossible or difficult to formalize in more traditional proof systems. -Lambdapi can also take as input `Dedukti`_ files, and can thus be used -as an interoperability tool. +Lambdapi is mostly compatible with `Dedukti`_ in the sense that it can +take Dedukti files as input and output Dedukti files as well. -Lambdapi is a logical framework and does not come with a pre-defined -logic. However, it is easy to define a logic by a few symbols and -rules. See for instance, the file `FOL.lp +Definitions and proofs written in Lambdapi can be exported to Coq as +well, to some extent. Lambdapi can thus be used as an interoperability +tool. + +Finally, Lambdapi is a logical framework, that is, it does not come +with a pre-defined logic. Instead, one has to start defining its own +logic. It is usually not too difficult to define a logic with a few +symbols and rewrite rules, and Lambdapi comes with a `repository of +pre-defined logics +`__. See for instance, +the file `FOL.lp `__ which defines (polymorphic) first-order logic. There also exist definitions for the -logics of HOL, Coq or Agda. +logics of HOL-Light, Coq or Agda. Here are some of the features of Lambdapi: diff --git a/doc/dedukti.rst b/doc/dedukti.rst index 15543b013..0208922d0 100644 --- a/doc/dedukti.rst +++ b/doc/dedukti.rst @@ -19,13 +19,11 @@ accept the same class of identifiers and module/file names), we try to rename them instead of failing: - ``lp`` identifiers that are not valid ``dk`` identifiers or that are - ``dk`` keywords are enclosed between ``{|`` and ``|}`` and, in - escaped identifiers, spaces and newlines are replaced by - underscores. + ``dk`` keywords are enclosed between ``{|`` and ``|}``. - In module names, dots are replaced by underscores and, if a ``lp`` file requires the module ``mylib.logic.untyped.fol``, its translation will require the file ``mylib_logic_untyped_fol.dk``. Therefore, in a package whose - ``root_path`` is ``mylib.logic``, the file ``untyped/fol.lp`` should - be translated into ``mylib_logic_untyped_fol.dk``. + ``root_path`` is ``mylib.logic``, the file ``untyped/fol.lp`` is + translated into ``mylib_logic_untyped_fol.dk``. diff --git a/doc/options.rst b/doc/options.rst index 8cc25bbf3..e79607143 100644 --- a/doc/options.rst +++ b/doc/options.rst @@ -38,11 +38,11 @@ handled independently in the order they are given. The program immediately stops on the first failure, without going to the next file (if any). -**index:** +**Remark on index:** The ``index`` command generates the file ``~/.LPSearch.db``. This file contains an indexation of all the symbols and rules occurring in the dk/lp files given in argument. By default, the file ``~/.LPSearch.db`` is erased first. To append new symbols and rules, use the option ``--add``. It is also possile to normalize terms wrt some rules before indexation by using ``--rules`` options. -**search:** +**Remark on search:** The command ``search`` takes as argument a query and runs it against the index file ``~/.LPSearch.db``. See :doc:`query_language` for the specification of the query language. @@ -63,13 +63,11 @@ The commands ``check``, ``decision-tree``, ``export``, ``parse``, * ``-v ``, ``--verbose=`` sets the verbosity level to the given natural number (the default value is 1). A value of 0 should not print anything, and the higher values print more and more information. - check ----- * ``-c``, ``--gen-obj`` instructs Lambdapi to generate object files for every checked module (including dependencies). Object files have the extension ``.lpo`` and they are automatically read back when necessary if they exist and are up to date (they are regenerated otherwise). - * ``--too-long=`` gives a warning for each interpreted source file command taking more than the given number of seconds to be checked. The parameter ``FLOAT`` is expected to be a floating point number. export @@ -79,14 +77,17 @@ export - ``lp``: Lambdapi format - ``dk``: `Dedukti `__ format + - ``raw_dk``: `Dedukti `__ format - ``hrs``: `HRS `__ format of the confluence competition - ``xtc``: `XTC `__ format of the termination competition - ``raw_coq``: `Coq `__ format - ``stt_coq``: `Coq `__ format assuming that the input file is in an encoding of simple type theory -**WARNING**: The options ``raw_coq`` and ``stt_coq`` are still experimental. +**WARNING**: With the formats ``raw_coq``, ``stt_coq`` and ``raw_dk``, the translation is done just after parsing, thus before scoping and elaboration. So Lambdapi cannot translate any input file, and the output may be incomplete or fail to type-check. + +The format ``raw_dk`` does not accept the commands ``notation`` and ``inductive``, and proofs and tactics, which require elaboration. -With the options ``raw_coq`` and ``stt_coq``, rules are ignored. The encoding of simple type theory can however be defined in Coq using `STTfa.v `__. +The formats ``raw_coq`` and ``stt_coq`` only accept the commands ``require``, ``open``, ``symbol`` and ``rule``, but rules are simply ignored. The encoding of simple type theory can however be defined in Coq using `STTfa.v `__. For the format ``stt_coq``, several other options are available: diff --git a/doc/vim.rst b/doc/vim.rst index 676a9fa46..27504c9e8 100644 --- a/doc/vim.rst +++ b/doc/vim.rst @@ -1,5 +1,5 @@ -`Vim `__ -============================== +`Vim `__ (not maintained anymore) +======================================================= A minimal Vim mode is provided to edit Lambdapi files. It provides syntax highlighting and abbreviations to enter unicode characters. diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml index 9e3246a2d..5557e6e15 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 | RawDk | Hrs | Xtc | RawCoq | SttCoq (** Running the export mode. *) let export_cmd (cfg:Config.t) (output:output option) (encoding:string option) @@ -115,6 +115,7 @@ let export_cmd (cfg:Config.t) (output:output option) (encoding:string option) | None | Some Lp -> Pretty.ast Format.std_formatter (Parser.parse_file file) | Some Dk -> Export.Dk.sign (Compile.compile_file file) + | Some RawDk -> Export.Rawdk.print (Parser.parse_file file) | Some Hrs -> Export.Hrs.sign Format.std_formatter (Compile.compile_file file) | Some Xtc -> @@ -229,6 +230,7 @@ let output : output option CLT.t = match s with | "lp" -> Ok Lp | "dk" -> Ok Dk + | "raw_dk" -> Ok RawDk | "hrs" -> Ok Hrs | "xtc" -> Ok Xtc | "raw_coq" -> Ok RawCoq @@ -240,6 +242,7 @@ let output : output option CLT.t = (match o with | Lp -> "lp" | Dk -> "dk" + | RawDk -> "raw_dk" | Hrs -> "hrs" | Xtc -> "xtc" | RawCoq -> "raw_coq" @@ -249,7 +252,8 @@ let output : output option CLT.t = in let doc = "Set the output format of the export command. The value of $(docv) \ - must be `lp' (default), `dk`, `hrs`, `xtc`, `raw_coq` or `stt_coq`." + must be `lp' (default), `raw_dk`, `dk`, `hrs`, `xtc`, `raw_coq` or \ + `stt_coq`." in Arg.(value & opt (some output) None & info ["output";"o"] ~docv:"FMT" ~doc) diff --git a/src/common/escape.ml b/src/common/escape.ml index 1c0480ab0..81de7b2e8 100644 --- a/src/common/escape.ml +++ b/src/common/escape.ml @@ -1,4 +1,5 @@ (** Escaped identifiers ["{|...|}"]. *) +let escape : string -> string = fun s -> "{|" ^ s ^ "|}" (** [is_escaped s] tells if [s] begins with ["{|"] and ends with ["|}"] without overlapping. For efficiency, we just test that it starts with @@ -13,10 +14,10 @@ let unescape : string -> string = fun s -> too, then [add_prefix p n] is just [p ^ n]. Otherwise, it is ["{|" ^ p ^ unescape n ^ "|}"]. *) let add_prefix : string -> string -> string = fun p n -> - if is_escaped n then "{|" ^ p ^ unescape n ^ "|}" else p ^ n + if is_escaped n then escape (p ^ unescape n) else p ^ n (** [s] is assumed to be a regular identifier. If [n] is a regular identifier too, then [add_suffix n s] is just [n ^ s]. Otherwise, it is ["{" ^ unescape n ^ s ^ "|}"]. *) let add_suffix : string -> string -> string = fun n s -> - if is_escaped n then "{|" ^ unescape n ^ s ^ "|}" else n ^ s + if is_escaped n then escape (unescape n ^ s) else n ^ s diff --git a/src/core/term.ml b/src/core/term.ml index bbdd6d715..ae85b0d3b 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -365,7 +365,8 @@ let create_sym : Path.t -> expo -> prop -> match_strat -> bool -> { elt = sym_name; pos = sym_pos } sym_decl_pos typ sym_impl -> {sym_path; sym_name; sym_type = ref typ; sym_impl; sym_def = ref None; - sym_opaq = ref sym_opaq; sym_rules = ref []; sym_dtree = ref Tree_type.empty_dtree; + sym_opaq = ref sym_opaq; sym_rules = ref []; + sym_dtree = ref Tree_type.empty_dtree; sym_mstrat; sym_prop; sym_expo; sym_pos ; sym_decl_pos } (** [is_constant s] tells whether [s] is a constant. *) diff --git a/src/export/dk.ml b/src/export/dk.ml index f3e91f685..3ab646dac 100644 --- a/src/export/dk.ml +++ b/src/export/dk.ml @@ -5,8 +5,6 @@ open Timed open Common open Core open Term -let string = string - (** Translation of identifiers. Lambdapi identifiers that are Dedukti keywords or invalid Dedukti identifiers are escaped, a feature offered by Dedukti. *) @@ -56,9 +54,7 @@ let is_ident : string -> bool = fun s -> let is_mident : string -> bool = fun s -> Parsing.DkLexer.is_mident (Lexing.from_string s) -let escape : string pp = fun ppf s -> out ppf "{|%s|}" s - -let replace_spaces : string -> string = fun s -> +(*let replace_spaces : string -> string = fun s -> let open Bytes in let b = of_string s in for i=0 to length b - 1 do @@ -66,23 +62,22 @@ let replace_spaces : string -> string = fun s -> | ' ' | '\n' -> set b i '_' | _ -> () done; - to_string b + to_string b*) let ident : string pp = fun ppf s -> - if s = "" then escape ppf s - else if s.[0] = '{' then string ppf (replace_spaces s) - else if is_keyword s then escape ppf s - else if is_ident s then string ppf s - else escape ppf s + string ppf + (if s = "" then Escape.escape s + else if s.[0] = '{' then s + else if is_keyword s then Escape.escape s + else if is_ident s then s + else Escape.escape s) (** Translation of paths. Paths equal to the [!current_path] are not printed. Non-empty paths end with a dot. We assume that the module p1.p2.p3 is in the file p1_p2_p3.dk. *) let path_elt : string pp = fun ppf s -> - if s <> "" && s.[0] = '{' then - string ppf (replace_spaces (Escape.unescape s)) - else string ppf s + string ppf (if Escape.is_escaped s then Escape.unescape s else s) let current_path = Stdlib.ref [] @@ -91,11 +86,9 @@ let path : Path.t pp = fun ppf p -> match p with | [] -> () | p -> - let joined_path = Format.asprintf "%a" (List.pp path_elt "_") p in - if List.for_all is_mident p then - out ppf "%s." joined_path - else - Format.fprintf ppf "%a." escape joined_path + let m = Format.asprintf "%a" (List.pp path_elt "_") p in + let m = if is_mident m then m else Escape.escape m in + out ppf "%s." m let qid : (Path.t * string) pp = fun ppf (p, i) -> out ppf "%a%a" path p ident i diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml new file mode 100644 index 000000000..13375a447 --- /dev/null +++ b/src/export/rawdk.ml @@ -0,0 +1,213 @@ +(** Translate the parser-level AST to Dedukti. *) + +open Lplib open Base open Extra +open Common open Pos open Error +open Parsing open Syntax +open Format +open Core open Eval open Term + +let raw_ident : string pp = fun ppf s -> Dk.ident ppf s + +let ident : p_ident pp = fun ppf {elt;_} -> raw_ident ppf elt + +let qident : p_qident pp = fun ppf {elt=(mp,s);_} -> + out ppf "%a%a" Dk.path mp raw_ident s + +let param_id : p_ident option pp = fun ppf idopt -> + match idopt with + | Some id -> ident ppf id + | None -> out ppf "_" + +let rec term : p_term pp = fun ppf t -> + match t.elt with + | P_Meta _ -> assert false + | P_Patt(id,ts) -> out ppf "%a%a" param_id id (Option.pp terms) ts; + | P_Expl u -> out ppf "(%a)" term u + | P_Type -> out ppf "Type" + | P_Wild -> out ppf "_" + | P_NLit i -> string ppf i + | P_Iden(qid,_) -> qident ppf qid + | P_Arro(u,v) -> out ppf "%a -> %a" pterm u term v + | P_Abst(xs,u) -> out ppf "%a%a" abs xs term u + | P_Prod(xs,u) -> out ppf "%a%a" prod xs term u + | P_LLet(x,xs,a,u,v) -> + out ppf "(%a%a => %a) %a" + ident x (Option.pp (let_typ xs)) a term v (let_dfn xs) u + | P_Wrap u -> out ppf "(%a)" term u + | P_Appl(u,v) -> out ppf "%a %a" term u pterm v + +and let_typ : p_params list -> p_term pp = fun xs ppf u -> + match xs with + | [] -> typ ppf u + | _ -> out ppf ": (%a%a)" prod xs term u + +and let_dfn : p_params list -> p_term pp = fun xs ppf u -> + match xs with + | [] -> pterm ppf u + | _ -> out ppf "(%a%a)" abs xs term u + +and pterm : p_term pp = fun ppf t -> + match t.elt with + (* doesn't need surrounding parentheses *) + | P_Meta _ + | P_Patt(_,None) + | P_Expl _ + | P_Type + | P_Wild + | P_NLit _ + | P_Iden _ + | P_Wrap _ + -> term ppf t + (* add surrounding parentheses *) + | P_Patt(_,Some _) + | P_Arro _ + | P_Abst _ + | P_Prod _ + | P_LLet _ + | P_Appl _ + -> out ppf "(%a)" term t + +and terms : p_term array pp = fun ppf -> Array.iter (out ppf " %a" term) + +and param : p_term option -> string -> p_ident option pp = fun a sep ppf id -> + if sep = "" then + match a with + | None -> out ppf " %a" param_id id + | Some a -> out ppf " (%a%a)" param_id id typ a + else out ppf "%a%a%s" param_id id (Option.pp typ) a sep + +and params : string -> p_params pp = fun sep ppf (ids,a,_) -> + match ids, a with + | None::_, None -> + fatal_no_pos "Cannot translate \"_\" parameters with no type." + | Some {pos;_}::_, None -> + fatal pos "Cannot translate parameters with no type." + | _ -> List.iter (out ppf "%a" (param a sep)) ids + +and params_list : string -> p_params list pp = fun sep ppf -> + List.iter (out ppf "%a" (params sep)) + +and abs : p_params list pp = fun ppf -> params_list " => " ppf +and prod : p_params list pp = fun ppf -> params_list " -> " ppf +and arg : p_params list pp = fun ppf -> params_list "" ppf + +and typ : p_term pp = fun ppf t -> out ppf " : %a" pterm t + +let bool : bool pp = fun ppf b -> if not b then out ppf "NOT" + +let assertion : (bool * p_assertion) pp = fun ppf (b,a) -> + match a with + | P_assert_typing(t,u) -> + out ppf "#ASSERT%a %a : %a.@." bool b term t term u + | P_assert_conv(t,u) -> + out ppf "#ASSERT%a %a == %a.@." bool b pterm t pterm u + +let strat : Eval.strat pp = fun ppf {strategy; steps} -> + match strategy, steps with + | NONE, _ + | HNF, _ -> assert false + | WHNF, None -> out ppf "[WHNF]" + | WHNF, Some k -> out ppf "[%d,WHNF]" k + | SNF, None -> () + | SNF, Some k -> out ppf "[%d]" k + +let query : p_query pp = fun ppf ({elt;pos} as q) -> + match elt with + | P_query_verbose _ + | P_query_debug _ + | P_query_prover _ + | P_query_prover_timeout _ + | P_query_print _ + | P_query_proofterm + | P_query_search _ + | P_query_flag _ -> out ppf "(;%a;)" Pretty.query q (*FIXME?*) + | P_query_infer(_,{strategy=(SNF|HNF|WHNF);_}) + | P_query_normalize(_,{strategy=(NONE|HNF);_}) -> + fatal pos "Cannot be translated: %a" Pretty.query q + | P_query_assert(b,a) -> assertion ppf (not b,a) + | P_query_infer(t,{strategy=NONE;_}) -> out ppf "#INFER %a.@." term t + | P_query_normalize(t,s) -> out ppf "#EVAL%a %a.@." strat s term t + +(*https://github.com/Deducteam/Dedukti/issues/318*) +let rec remove_wraps ({elt;_} as t) = + match elt with + | P_Wrap u -> remove_wraps u + | _ -> t + +let rule : p_rule pp = + let varset ppf set = List.pp string ", " ppf (StrSet.elements set) in + fun ppf {elt=(l,r);_} -> + out ppf "[%a] %a --> %a.@." varset (pvars_lhs l) term (remove_wraps l) term r + +let partition_modifiers ms = + let ms = List.map (fun {elt;_} -> elt) ms in + let ms = List.sort_uniq Stdlib.compare ms in + let is_prop elt = match elt with P_prop _ -> true | _ -> false in + let props, non_props = List.partition is_prop ms in + let props = List.map (function P_prop p -> p | _ -> assert false) props in + let is_expo elt = match elt with P_expo _ -> true | _ -> false in + let expos, non_expos = List.partition is_expo non_props in + let expos = List.map (function P_expo e -> e | _ -> assert false) expos in + let is_mstrat elt = match elt with P_mstrat _ -> true | _ -> false in + let mstrats, opaqs = List.partition is_mstrat non_expos in + let mstrats = + List.map (function P_mstrat s -> s | _ -> assert false) mstrats in + (* we ignore private symbols *) + let expos = List.filter (function Privat -> false | _ -> true) expos in + props, expos, mstrats, opaqs + +(* check Stdlib.compare on modifiers. *) +let _ = + assert (Stdlib.compare Commu (Assoc true) < 0) + ;assert (Stdlib.compare Commu (Assoc false) < 0) + +let modifiers : p_term option -> p_modifier list pp = fun p_sym_typ ppf ms -> + match partition_modifiers ms with + | [], [], [], [] -> out ppf "def " + | [], [], [], [P_opaq] when p_sym_typ <> None -> out ppf "thm " + (*https://github.com/Deducteam/Dedukti/issues/319*) + | [Commu;Assoc _], [Protec], [], [] -> out ppf "defac " + | [Injec], [Protec], [], [] -> out ppf "private injective " + | [Injec], [], [], [] -> out ppf "injective " + | [], [Protec], [], [] -> out ppf "private " + | [Const], [], [], [] -> () + | _ -> + match ms with + | [] -> assert false + | {pos;_}::_ -> fatal pos "Cannot translate: %a.@." Pretty.modifiers ms + +let command : p_command pp = fun ppf ({elt; pos} as c) -> + match elt with + | P_query q -> query ppf q + | P_require(false,ps) -> + List.iter (fun {elt;_} -> out ppf "#REQUIRE %a@." Dk.path elt) ps + | P_symbol{p_sym_mod; p_sym_nam=n; p_sym_arg=xs; p_sym_typ; + p_sym_trm; p_sym_prf=None; p_sym_def=_;} -> + begin match p_sym_trm, p_sym_typ with + | Some t, _ -> + let dfn ppf = out ppf " := %a" term in + out ppf "%a%a%a%a%a.@." (modifiers p_sym_typ) p_sym_mod ident n + arg xs (Option.pp typ) p_sym_typ dfn t + | None, Some a -> + (*https://github.com/Deducteam/Dedukti/issues/322*) + out ppf "%a%a : %a%a.@." (modifiers p_sym_typ) p_sym_mod ident n + prod xs term a + | _ -> assert false + end + | P_rules rs -> List.iter (rule ppf) rs + | P_builtin _ + | P_unif_rule _ + | P_coercion _ + -> () (*FIXME?*) + | P_inductive _ + | P_open _ + | P_require_as _ + | P_notation _ (* FIXME: accept quantifier notations *) + | P_opaque _ + | P_require(true,_) + | P_symbol{p_sym_prf=Some _; _} + -> fatal pos "Cannot be translated: %a" Pretty.command c + +let ast : ast pp = fun ppf -> Stream.iter (command ppf) + +let print : ast -> unit = ast std_formatter diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml index f3265a471..045c8e045 100644 --- a/src/parsing/lpLexer.ml +++ b/src/parsing/lpLexer.ml @@ -173,7 +173,7 @@ let escid = [%sedlex.regexp? (** [escape s] converts a string [s] into an escaped identifier if it is not regular. We do not check whether [s] contains ["|}"]. FIXME? *) -let escape s = if is_regid s then s else "{|" ^ s ^ "|}" +let escape s = if is_regid s then s else Escape.escape s (** [remove_useless_escape s] replaces escaped regular identifiers by their unescape form. *) diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml index 935e7cd75..5aee6f1fd 100644 --- a/src/parsing/pretty.ml +++ b/src/parsing/pretty.ml @@ -77,8 +77,7 @@ let _ = let open LpLexer in ; "with", WITH ] let raw_ident : string pp = fun ppf s -> - if is_keyword s then out ppf "{|%s|}" s - else string ppf s + string ppf (if is_keyword s then Escape.escape s else s) let ident : p_ident pp = fun ppf {elt;_} -> raw_ident ppf elt diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index a0a8c63ee..e15f69a97 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -648,7 +648,8 @@ let scope_rule : "Symbol %s has been declared constant, it cannot be used as the \ head of a rewrite rule LHS." pr_sym.sym_name; if Timed.(!(pr_sym.sym_opaq) || (!(pr_sym.sym_def) <> None)) then - fatal p_lhs.pos "No rewriting rule can be added on an opaque symbol or a symbol already defined with ≔"; + fatal p_lhs.pos "No rewriting rule can be added on an opaque symbol \ + or a symbol already defined with ≔"; if pr_sym.sym_expo = Protec && ss.signature.sign_path <> pr_sym.sym_path then fatal p_lhs.pos "Cannot define rules on foreign protected symbols."; diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index b87d279dd..3da081297 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -107,6 +107,30 @@ let p_get_args : p_term -> p_term * p_term list = fun t -> | _ -> t, acc in p_get_args t [] +(** [pvars_lhs t] computes the set of pattern variable names in [t], assuming + that [t] is a rule LHS. *) +let rec pvars_lhs : p_term -> StrSet.t = fun {elt;pos} -> + match elt with + | P_Type + | P_Iden _ + | P_Wild + | P_Patt(None,_) + | P_NLit _ + -> StrSet.empty + | P_Meta _ + | P_LLet _ + | P_Arro _ + | P_Prod _ + -> assert false + | P_Patt(Some{elt;_},_) -> + StrSet.singleton elt + | P_Appl(u,v) -> + StrSet.union (pvars_lhs u) (pvars_lhs v) + | P_Abst(_,u) (*FIXME: get pattern variables in types?*) + | P_Wrap u + | P_Expl u + -> pvars_lhs u + (** Parser-level rewriting rule representation. *) type p_rule_aux = p_term * p_term type p_rule = p_rule_aux loc diff --git a/tests/OK/stricly_positive_1.lp b/tests/OK/strictly_positive_1.lp similarity index 100% rename from tests/OK/stricly_positive_1.lp rename to tests/OK/strictly_positive_1.lp diff --git a/tests/OK/stricly_positive_2.lp b/tests/OK/strictly_positive_2.lp similarity index 100% rename from tests/OK/stricly_positive_2.lp rename to tests/OK/strictly_positive_2.lp diff --git a/tests/export_dk.sh b/tests/export_dk.sh index c6c67d483..66a6de4c8 100755 --- a/tests/export_dk.sh +++ b/tests/export_dk.sh @@ -1,15 +1,17 @@ #!/bin/bash +set -e + echo '############ test export -o dk ############' -lambdapi=${LAMBDAPI:-_build/install/default/bin/lambdapi} +root=`pwd` + +lambdapi=${LAMBDAPI:-$root/_build/install/default/bin/lambdapi} dkcheck=${DKCHECK:-dk check} dkdep=${DKDEP:-dk dep} TIMEFORMAT="%Es" -root=`pwd` - outdir=/tmp/export_dk reset_outdir() { @@ -18,59 +20,55 @@ reset_outdir() { } reset_outdir -# compute lp files to test -for f in tests/OK/*.lp +translate() { + f=tests/OK/${1%.lp} + out=$outdir/`echo $f | sed -e 's/\//_/g'` + echo "$f.lp --> $out.dk ..." + $lambdapi export -w -v 0 -o dk $1 > $out.dk + if test $? -ne 0; then echo KO; exit 1; fi +} + +echo translate files ... +cd tests/OK +for f in *.lp do f=${f%.lp} case $f in - tests/OK/ac);; # because dedukti does not handle commutative and non associative symbols - tests/OK/π/utf_path);; # because dedukti does not accept unicode characters in module names - tests/OK/escape_path|'tests/OK/a b/escape file');; # because dedukti does not accept spaces in module names - tests/OK/262_private_in_lhs);; # because dedukti does not accept protected symbols in rule LHS arguments - tests/OK/273|tests/OK/813);; # because dedukti SR algorithm fails - tests/OK/file.with.dot|tests/OK/req.file.with.dot);; #FIXME - tests/OK/indind);; #FIXME - tests/OK/why3*);; #FIXME - *) lp_files="$f.lp $lp_files"; - f=`echo $f | sed -e 's/\//_/g'`; - dk_files="$f.dk $dk_files";; + # commutative and non associative symbol + ac);; + # protected symbol in rule LHS arguments + 262_private_in_lhs);; + # dedukti SR algorithm fails + 273|813);; + # FIXME + file.with.dot|req.file.with.dot);; + indind);; + why3*);; + # require escaped module name + π/utf_path|escape_path|'a b/escape file'|require_nondkmident);; + + # default case + *) translate $f.lp;; esac done +cd ../.. -# compile lp files -compile() { - echo 'compile lp files ...' - #$lambdapi check -w -c $lp_files # does not work because of #802 - for f in $lp_files - do - echo "compile $f ..." - $lambdapi check -w -v 0 -c $f - done -} -#time compile - -# translate lp files to dk files -translate() { - echo 'translate lp files ...' - for f in $lp_files - do - f=${f%.lp} - out=$outdir/`echo $f | sed -e 's/\//_/g'` - echo "$f.lp --> $out.dk ..." - $lambdapi export -w -v 0 -o dk $f.lp > $out.dk - if test $? -ne 0; then echo KO; exit 1; fi - done -} -time translate - -# check dk files check() { + echo + echo check translated files ... cd $outdir - echo 'remove #REQUIRE commands (to be removed when https://github.com/Deducteam/Dedukti/issues/262 is fixed) ...' - sed -i -e 's/#REQUIRE.*$//' $dk_files - dk_files=`$dkdep -q -s $dk_files` - echo $dkcheck -q -e $dk_files ... - $dkcheck -q -e $dk_files + #https://github.com/Deducteam/Dedukti/issues/321 + #dk_files=`$dkdep -q -s $dk_files` + echo > Makefile <<__END__ +FILES := \$(wildcard *.dk) +default: \$(FILES:%.dk=%.dko) +%.dko: %.dk + dk check -e \$< +__END__ + $dkdep -q *.dk >> Makefile + #echo $dkcheck -q -e $dk_files ... + #$dkcheck -q -e $dk_files + make res=$? cd $root if test $res -ne 0; then echo KO; else echo OK; fi diff --git a/tests/export_lp.sh b/tests/export_lp.sh index 835796c83..eb5cbdcd1 100755 --- a/tests/export_lp.sh +++ b/tests/export_lp.sh @@ -1,5 +1,7 @@ #!/bin/bash +set -e + echo '############ test export -o lp ############' lambdapi=${lambdapi:-_build/install/default/bin/lambdapi} diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh new file mode 100755 index 000000000..bf3541bd4 --- /dev/null +++ b/tests/export_raw_dk.sh @@ -0,0 +1,102 @@ +#!/bin/bash + +set -e + +echo '############ test export -o raw_dk ############' + +root=`pwd` + +lambdapi=${LAMBDAPI:-$root/_build/install/default/bin/lambdapi} +dkcheck=${DKCHECK:-dk check} +dkdep=${DKDEP:-dk dep} + +TIMEFORMAT="%Es" + +outdir=/tmp/export_raw_dk + +reset_outdir() { + rm -rf $outdir + mkdir -p $outdir +} +reset_outdir + +translate() { + f=tests/OK/${1%.lp} + out=$outdir/`echo $f | sed -e 's/\//_/g'` + echo "$f.lp --> $out.dk ..." + $lambdapi export -w -v 0 -o raw_dk $1 > $out.dk + if test $? -ne 0; then echo KO; exit 1; fi +} + +echo translate files ... +cd tests/OK +for f in *.lp +do + f=${f%.lp} + case $f in + # commutative and non associative symbol + ac);; + # unicode character in module name + π/utf_path);; + # space in module name + escape_path|'tests/OK/a b/escape file');; + # protected symbol in rule LHS argument + 262_private_in_lhs);; + # dedukti SR algorithm fails + 273|tests/OK/813);; + # FIXME + file.with.dot|req.file.with.dot);; + indind);; + # "sequential" + rule_order|813|1033);; + # "as" + 729);; + # "notation" + xor|Set|quant*|Prop|prefix|parametricCoercions|opaque|nat_id*|michael|max-suc-alg|lpparse|iss861|infix|infer|indrec|implicitArgs[34]|group|cr_qu|cp*|coercions|builtin_zero_succ|plus_ac|693|693_assume|679|665|655|655b|649_fo_27|595_and_elim|584_c_slow|579_or_elim_long|579_long_no_duplicate|359|328|245|245b|244|1026);; + # "quantifier" + 683|650|573|565|430);; + # nested module name + require_nondkmident);; + # proofs + why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit);; + # "open" + triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215);; + # "inductive" + strictly_positive_*|inductive|989|904|830|341);; + # underscore in query + unif_hint|patterns|let|767);; + # abstracted variable type in rule LHS + 573-2);; + # domain-free lambda/product + 298_lp|262_parsing|tail|698_abst_impl|330|330b|1035|varmatch|patt|freevars-constraints|eta_equality|declared|boolean|abstractions|303|301|292|225);; + # opaque definition with no type (https://github.com/Deducteam/Dedukti/issues/319) + 547);; + + # default case: + *) translate $f.lp;; + esac +done +cd ../.. + +check() { + echo + echo check translated files ... + cd $outdir + #https://github.com/Deducteam/Dedukti/issues/321 + #dk_files=`$dkdep -q -s $dk_files` + cat > Makefile <<__END__ +FILES := \$(wildcard *.dk) +default: \$(FILES:%.dk=%.dko) +%.dko: %.dk + dk check -e \$< +__END__ + $dkdep -q *.dk >> Makefile + #echo $dkcheck -q -e $dk_files ... + #$dkcheck -q -e $dk_files + make + res=$? + cd $root + if test $res -ne 0; then echo KO; else echo OK; fi + exit $res +} +check diff --git a/tests/runtests.sh b/tests/runtests.sh index 69fb6d09e..57b2a0569 100755 --- a/tests/runtests.sh +++ b/tests/runtests.sh @@ -1,5 +1,7 @@ #!/bin/bash +set -e + lambdapi='dune exec -- lambdapi check' TIMEFORMAT="%Es"