89 lines
2.1 KiB
OCaml
89 lines
2.1 KiB
OCaml
open Structs;;
|
|
open Pieuvre;;
|
|
|
|
(* Parsage des arguments*)
|
|
let filename = ref "" in
|
|
|
|
let reduce = ref false in
|
|
let alpha = ref false in
|
|
let typecheck = ref false in
|
|
|
|
Arg.parse
|
|
[("-reduce", Arg.Set reduce, "Show the step-by-step reduction of a lambda-term");
|
|
("-alpha", Arg.Set alpha, "Check is two lambda-terms separated by '&' are alpha-convertible");
|
|
("-typecheck", Arg.Set typecheck, "Check if a lambda term has a given type")]
|
|
(fun s -> filename := s)
|
|
"The available options are:";
|
|
|
|
(* Ouverture éventuelle du fichier *)
|
|
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 -> (
|
|
Printf.printf ">>> ";
|
|
flush stdout;
|
|
read_line ()
|
|
)
|
|
| Some f -> input_line f
|
|
in
|
|
|
|
(* Show a message only if the input is read from stdin *)
|
|
let show s = match file with
|
|
| None -> Printf.printf "%s" s
|
|
| _ -> ()
|
|
in
|
|
|
|
show "Please type the formula to prove\n";
|
|
|
|
let ty =
|
|
try
|
|
let lexbuf = Lexing.from_string (readline ()) in
|
|
Parser.main_type Lexer.token_ty lexbuf
|
|
with e -> (
|
|
Printf.printf "Can't parse type\n";
|
|
raise e
|
|
)
|
|
in
|
|
|
|
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 tactic =
|
|
let rec read_tactic () =
|
|
try
|
|
let lexbuf = Lexing.from_string (readline ()) in
|
|
Parser.main_tactic Lexer.token_tactic lexbuf
|
|
with e -> (
|
|
Printf.printf "Can't parse tactic\n";
|
|
if is_interactive then
|
|
read_tactic ()
|
|
else
|
|
raise e
|
|
)
|
|
in
|
|
read_tactic ()
|
|
in
|
|
()
|
|
)
|
|
done;
|
|
|
|
();;
|