Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Turned the files in src into a lib called Core. #397

Merged
merged 2 commits into from
Jun 15, 2023
Merged

Turned the files in src into a lib called Core. #397

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8a72ef5
Turned the files in src into a lib called core.
Jun 13, 2023
a497d83
Removed reference to dead code in dune file
Jun 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion src/dune
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,11 +5,19 @@

(include_subdirs unqualified)

(library
(name core)
(public_name easycrypt.core)
(modules :standard \ ec)
(libraries batteries camlp-streams dune-build-info inifiles why3 yojson zarith)
)

(executable
(public_name easycrypt)
(name ec)
(modules ec)
(promote (until-clean))
(libraries batteries camlp-streams dune-build-info inifiles why3 yojson zarith))
(libraries batteries camlp-streams dune-build-info inifiles why3 yojson zarith core))

(ocamllex ecLexer)

Expand Down
31 changes: 16 additions & 15 deletions src/ec.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
(* -------------------------------------------------------------------- *)
open Core
open EcUtils
open EcOptions

Expand Down Expand Up @@ -258,8 +259,8 @@ let main () =
| `Cli cliopts -> begin
let terminal =
if cliopts.clio_emacs
then lazy (EcTerminal.from_emacs ())
else lazy (EcTerminal.from_tty ())
then lazy (T.from_emacs ())
else lazy (T.from_tty ())

in (cliopts.clio_provers, None, terminal, true, false)
end
Expand All @@ -279,7 +280,7 @@ let main () =
let gcstats = cmpopts.cmpo_gcstats in
let progress = if cmpopts.cmpo_script then `Script else `Human in
let terminal =
lazy (EcTerminal.from_channel ~name ~gcstats ~progress (open_in name))
lazy (T.from_channel ~name ~gcstats ~progress (open_in name))
in
({cmpopts.cmpo_provers with prvo_iterate = true},
Some name, terminal, false, cmpopts.cmpo_noeco)
Expand Down Expand Up @@ -365,11 +366,11 @@ let main () =
exit 1);

(* Display Copyright *)
if EcTerminal.interactive terminal then
EcTerminal.notice ~immediate:true `Warning copyright terminal;
if T.interactive terminal then
T.notice ~immediate:true `Warning copyright terminal;

try
if EcTerminal.interactive terminal then Sys.catch_break true;
if T.interactive terminal then Sys.catch_break true;

(* Interaction loop *)
let first = ref `Init in
Expand Down Expand Up @@ -401,7 +402,7 @@ let main () =
EcScope.hierror "invalid pragma: `%s'\n%!" x);

let notifier (lvl : EcGState.loglevel) (lazy msg) =
EcTerminal.notice ~immediate:true lvl msg terminal
T.notice ~immediate:true lvl msg terminal
in

EcCommands.addnotifier notifier;
Expand All @@ -414,13 +415,13 @@ let main () =
| `Loop -> ()
end;

oiter (EcTerminal.setwidth terminal)
oiter (T.setwidth terminal)
(let gs = EcEnv.gstate (EcScope.env (EcCommands.current ())) in
match EcGState.getvalue "PP:width" gs with
| Some (`Int i) -> Some i | _ -> None);

begin
match EcLocation.unloc (EcTerminal.next terminal) with
match EcLocation.unloc (T.next terminal) with
| EP.P_Prog (commands, locterm) ->
terminate := locterm;
List.iter
Expand All @@ -437,7 +438,7 @@ let main () =
raise EcCommands.Restart
| e -> begin
if Printexc.backtrace_status () then begin
if not (EcTerminal.interactive terminal) then
if not (T.interactive terminal) then
Printf.fprintf stderr "%t\n%!" Printexc.print_backtrace
end;
raise (EcScope.toperror_of_exn ~gloc:loc e)
Expand All @@ -449,9 +450,9 @@ let main () =
| EP.P_Exit ->
terminate := true
end;
EcTerminal.finish `ST_Ok terminal;
T.finish `ST_Ok terminal;
if !terminate then begin
EcTerminal.finalize terminal;
T.finalize terminal;
if not eco then
finalize_input input (EcCommands.current ());
exit 0
Expand All @@ -461,15 +462,15 @@ let main () =
first := `Restart

| e -> begin
EcTerminal.finish
T.finish
(`ST_Failure (EcScope.toperror_of_exn e))
terminal;
if (!first = `Init) || not (EcTerminal.interactive terminal) then
if (!first = `Init) || not (T.interactive terminal) then
exit 1
end
done
with e ->
(try EcTerminal.finalize terminal with _ -> ());
(try T.finalize terminal with _ -> ());
raise e

(* -------------------------------------------------------------------- *)
Expand Down