From 8a72ef55c74d31d6d0c6d6b436eefea972ece397 Mon Sep 17 00:00:00 2001
From: Romain Tetley <rtetley@inria.fr>
Date: Tue, 13 Jun 2023 14:21:16 +0200
Subject: [PATCH 1/2] Turned the files in src into a lib called core.

---
 src/dune  | 10 +++++++++-
 src/ec.ml | 31 ++++++++++++++++---------------
 2 files changed, 25 insertions(+), 16 deletions(-)

diff --git a/src/dune b/src/dune
index 89cdf5ee3d..a4cfa599bc 100644
--- a/src/dune
+++ b/src/dune
@@ -5,11 +5,19 @@
 
 (include_subdirs unqualified)
 
+(library 
+ (name core)
+ (public_name easycrypt.core)
+ (modules :standard \ ec ecCoreHiPhl)
+ (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)
 
diff --git a/src/ec.ml b/src/ec.ml
index c794382ea9..7a74a4c485 100644
--- a/src/ec.ml
+++ b/src/ec.ml
@@ -1,4 +1,5 @@
 (* -------------------------------------------------------------------- *)
+open Core
 open EcUtils
 open EcOptions
 
@@ -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
@@ -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)
@@ -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
@@ -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;
@@ -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
@@ -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)
@@ -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
@@ -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
 
 (* -------------------------------------------------------------------- *)

From a497d83859c92311de6ea1b37f9e14a0e5e7a975 Mon Sep 17 00:00:00 2001
From: Romain Tetley <rtetley@inria.fr>
Date: Thu, 15 Jun 2023 16:24:02 +0200
Subject: [PATCH 2/2] Removed reference to dead code in dune file

The file ecCoreHiPhl was removed as dead code, no need
to exclude it in the dune file anymore.
---
 src/dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/dune b/src/dune
index a4cfa599bc..5df618448c 100644
--- a/src/dune
+++ b/src/dune
@@ -8,7 +8,7 @@
 (library 
  (name core)
  (public_name easycrypt.core)
- (modules :standard \ ec ecCoreHiPhl)
+ (modules :standard \ ec)
  (libraries batteries camlp-streams dune-build-info inifiles why3 yojson zarith)
 )