Interractive mode

main.ml

@@ -3,6 +3,7 @@ open Pieuvre;;
 
 (* Parsage des arguments*)
 let filename = ref "" in
+
 let reduce = ref false in
 let alpha = ref false in
 let typecheck = ref false in
@@ -19,6 +20,10 @@ let file = match !filename with
   | "" -> None
   | fn -> Some (open_in fn)
 in
+let is_interactive = match file with
+  | None -> true
+  | _ -> false
+in
 
 let readline () = match file with
   | None -> (
@@ -47,4 +52,23 @@ let ty =
     )
 in
 
-Printf.printf "%s\n" (string_of_ty ty);;
+while true do
+    if is_interactive then (
+        (* Nettoyage du terminal *)
+        let _ = Sys.command("clear -x") in
+
+        (* Affichage des hypothèses *)
+
+        (* Affichage des sous-buts *)
+        Printf.printf "================\n";
+        Printf.printf "%s\n" (string_of_ty ty);
+
+        (* Lecture d'une tactique *)
+        Printf.printf "What do you want to do?\n";
+
+        let line = read_line () in
+        ()
+    )
+done;
+
+();;