'
- block += '\n'
- file.write(block)
-
index += 1
def find(path):
diff --git a/elpi_REPL.ml b/elpi_REPL.ml
index 60f5371fb..b6844acbb 100644
--- a/elpi_REPL.ml
+++ b/elpi_REPL.ml
@@ -16,25 +16,30 @@ open Elpi
module Str = Re.Str
-let print_solution time = function
+let print_solution print_time time = function
| API.Execute.NoMoreSteps ->
- Format.eprintf "Interrupted (no more steps)@\n%!"
-| API.Execute.Failure -> Format.eprintf "Failure@\n%!"
+ Format.printf "Interrupted (no more steps)@\n%!"
+| API.Execute.Failure -> Format.printf "Failure@\n%!"
| API.Execute.Success {
API.Data.assignments; constraints; state; pp_ctx; _ } ->
- Format.eprintf "@\nSuccess:@\n%!" ;
- API.Data.StrMap.iter (fun name v ->
- Format.eprintf " @[%s = %a@]@\n%!" name
- (API.Pp.term pp_ctx) v) assignments;
- Format.eprintf "@\nTime: %5.3f@\n%!" time;
- Format.eprintf "@\nConstraints:@\n%a@\n%!"
- (API.Pp.constraints pp_ctx) constraints;
- Format.eprintf "@\nState:@\n%a@\n%!"
- API.Pp.state state;
+ if not (API.Data.StrMap.is_empty assignments) then begin
+ Format.printf "@\nSuccess:@\n%!" ;
+ API.Data.StrMap.iter (fun name v ->
+ Format.printf " @[%s = %a@]@\n%!" name
+ (API.Pp.term pp_ctx) v) assignments;
+ end;
+ if print_time then
+ Format.eprintf "@\nTime: %5.3f@\n%!" time;
+ if API.RawData.constraints constraints != [] then
+ Format.printf "@\nConstraints:@\n%a@\n%!"
+ (API.Pp.constraints pp_ctx) constraints;
+ if not(API.State.is_empty state) then
+ Format.printf "@\nState:@\n%a@\n%!"
+ API.Pp.state state;
;;
let more () =
- prerr_endline "\nMore? (Y/n)";
+ print_endline "\nMore? (Y/n)";
read_line() <> "n"
;;
@@ -54,7 +59,8 @@ let set_terminal_width ?(max_w=
let usage =
"\nUsage: elpi [OPTION].. [FILE].. [-- ARGS..] \n" ^
"\nMain options:\n" ^
- "\t-test runs the query \"main\"\n" ^
+ "\t-main runs the query \"main\"\n" ^
+ "\t-test runs the query \"main\" (deprecated)\n" ^
"\t-exec pred runs the query \"pred ARGS\"\n" ^
"\t-D var Define variable (conditional compilation)\n" ^
"\t-document-builtins Print documentation for built-in predicates\n" ^
@@ -72,7 +78,8 @@ let usage =
"\t-print-ast prints files as parsed, then exit\n" ^
"\t-print prints files after most compilation passes, then exit\n" ^
"\t-print-passes prints intermediate data during compilation, then exit\n" ^
- "\t-print-units prints compilation units data, then exit\n"
+ "\t-print-units prints compilation units data, then exit\n" ^
+ "\t-print-time prints parsing, compilation, checking and esecution time\n"
;;
(* For testing purposes we declare an identity quotation *)
@@ -81,7 +88,7 @@ let _ =
API.Quotation.lp
let _ =
- let test = ref false in
+ let main = ref false in
let exec = ref "" in
let print_lprolog = ref false in
let print_ast = ref false in
@@ -89,6 +96,7 @@ let _ =
let batch = ref false in
let doc_builtins = ref false in
let delay_outside_fragment = ref false in
+ let print_time = ref false in
let print_passes = ref false in
let print_units = ref false in
let extra_paths = ref [] in
@@ -102,9 +110,11 @@ let _ =
| "-legacy-parser" :: rest -> legacy_parser := true; eat_options rest
| "-legacy-parser-available" :: _ ->
if API.Setup.legacy_parser_available then exit 0 else exit 1
- | "-test" :: rest -> batch := true; test := true; eat_options rest
+ | "-main" :: rest -> batch := true; main := true; eat_options rest
+ | "-test" :: rest -> batch := true; main := true; eat_options rest
| "-exec" :: goal :: rest -> batch := true; exec := goal; eat_options rest
| "-print" :: rest -> print_lprolog := true; eat_options rest
+ | "-print-time" :: rest -> print_time := true; eat_options rest
| "-print-ast" :: rest -> print_ast := true; eat_options rest
| "-print-passes" :: rest -> print_passes := true; eat_options rest
| "-print-units" :: rest -> print_units := true; eat_options rest
@@ -176,8 +186,8 @@ let _ =
exit 1;
in
let g =
- if !test then
- API.Parse.goal ~elpi ~loc:(API.Ast.Loc.initial "(-test)") ~text:"main."
+ if !main then
+ API.Parse.goal ~elpi ~loc:(API.Ast.Loc.initial "(-main)") ~text:"main."
else if !exec <> "" then
begin API.Parse.goal ~elpi
~loc:(API.Ast.Loc.initial "(-exec)")
@@ -186,8 +196,9 @@ let _ =
end
else begin
Printf.printf "goal> %!";
- let buff = Lexing.from_channel stdin in
- try API.Parse.goal_from ~elpi ~loc:(API.Ast.Loc.initial "(stdin)") buff
+ let buff = Lexing.from_function (fun b n -> try let c = input_char stdin in Bytes.set b 0 c; 1 with End_of_file -> 0) in
+ try
+ API.Parse.goal_from ~elpi ~loc:(API.Ast.Loc.initial "(stdin)") buff
with API.Parse.ParseError(loc,err) ->
Printf.eprintf "%s:\n%s\n" (API.Ast.Loc.show loc) err;
exit 1;
@@ -198,14 +209,17 @@ let _ =
exit 0;
end;
- Format.eprintf "@\nParsing time: %5.3f@\n%!" (Unix.gettimeofday () -. t0_parsing);
+ if !print_time then
+ Format.eprintf "@\nParsing time: %5.3f@\n%!" (Unix.gettimeofday () -. t0_parsing);
+
let query, exec =
let t0_compilation = Unix.gettimeofday () in
try
let prog = API.Compile.program ~flags ~elpi [p] in
let query = API.Compile.query prog g in
let exec = API.Compile.optimize query in
- Format.eprintf "@\nCompilation time: %5.3f@\n%!" (Unix.gettimeofday () -. t0_compilation);
+ if !print_time then
+ Format.eprintf "@\nCompilation time: %5.3f@\n%!" (Unix.gettimeofday () -. t0_compilation);
query, exec
with API.Compile.CompileError(loc,msg) ->
API.Utils.error ?loc msg
@@ -213,7 +227,8 @@ let _ =
if !typecheck then begin
let t0 = Unix.gettimeofday () in
let b = API.Compile.static_check ~checker:(Builtin.default_checker ()) query in
- Format.eprintf "@\nTypechecking time: %5.3f@\n%!" (Unix.gettimeofday () -. t0);
+ if !print_time then
+ Format.eprintf "@\nTypechecking time: %5.3f@\n%!" (Unix.gettimeofday () -. t0);
if not b then begin
Format.eprintf "Type error. To ignore it, pass -no-tc.\n";
exit 1
@@ -230,7 +245,7 @@ let _ =
end;
if not !batch then
API.Execute.loop
- ~delay_outside_fragment:!delay_outside_fragment ~more ~pp:print_solution
+ ~delay_outside_fragment:!delay_outside_fragment ~more ~pp:(print_solution !print_time)
exec
else begin
Gc.compact ();
@@ -240,7 +255,7 @@ let _ =
~delay_outside_fragment:!delay_outside_fragment exec in
let t1 = Unix.gettimeofday () in
match b with
- | API.Execute.Success _ -> print_solution (t1 -. t0) b; true
+ | API.Execute.Success _ -> print_solution !print_time (t1 -. t0) b; true
| (API.Execute.Failure | API.Execute.NoMoreSteps) -> false
then exit 0
else exit 1
diff --git a/src/API.mli b/src/API.mli
index bad958cd3..a15ef0e01 100644
--- a/src/API.mli
+++ b/src/API.mli
@@ -750,6 +750,8 @@ module State : sig
val update : 'a component -> t -> ('a -> 'a) -> t
val update_return : 'a component -> t -> ('a -> 'a * 'b) -> t * 'b
+ val is_empty : t -> bool
+
end
(** Flexible data is for unification variables. One can use Elpi's unification
diff --git a/src/data.ml b/src/data.ml
index 1b69964c1..85cc78116 100644
--- a/src/data.ml
+++ b/src/data.ml
@@ -266,6 +266,7 @@ module State : sig
val update : 'a component -> t -> ('a -> 'a) -> t
val update_return : 'a component -> t -> ('a -> 'a * 'b) -> t * 'b
val pp : Format.formatter -> t -> unit
+ val is_empty : t -> bool
end = struct
@@ -360,6 +361,18 @@ end = struct
with Not_found -> ())
!extensions
+ let is_empty (t,s) =
+ let reserved_prefix = "elpi:" in
+ let len_reserved = String.length reserved_prefix in
+ StrMap.fold (fun name { pp } acc ->
+ if String.length name > len_reserved && String.sub name 0 len_reserved = reserved_prefix then
+ acc
+ else
+ try acc && (ignore(StrMap.find name t);Printf.eprintf "%s\n%!" name; false)
+ with Not_found -> acc)
+ !extensions true
+
+
end
(* This module contains the symbols reserved by Elpi and the ones
diff --git a/tests/suite/suite.ml b/tests/suite/suite.ml
index e9c9d798f..ad42dfa5f 100644
--- a/tests/suite/suite.ml
+++ b/tests/suite/suite.ml
@@ -388,7 +388,7 @@ let () = Runner.declare
let { Test.expectation; input; outside_llam ; typecheck; trace; legacy_parser; _ } = test in
let input = Util.option_map (fun x -> sources^x) input in
- let args = ["-test";"-I";executable_stuff;"-I";sources;source] @ trace in
+ let args = ["-print-time";"-main";"-I";executable_stuff;"-I";sources;source] @ trace in
let args =
if typecheck then args
else "-no-tc" :: args in