diff --git a/main.ml b/main.ml index cb1a803..2a9f946 100644 --- a/main.ml +++ b/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; + +();;