125 lines
3.4 KiB
OCaml
125 lines
3.4 KiB
OCaml
open Structs;;
|
|
open Pieuvre;;
|
|
|
|
let fail () =
|
|
failwith "Unknown error";;
|
|
|
|
(* 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
|
|
|
|
let subgoals: (ty * (var_lambda * ty) list) list ref = ref [(ty, [])] in
|
|
|
|
(* On donne en paramètre une liste contenant un lambda-terme par trou (ie subgoal),
|
|
* et elle renvoie le lambda-terme complet (en remplaçant les trous) *)
|
|
let fill_holes = ref (fun holes -> List.hd holes) in
|
|
|
|
while !subgoals <> [] do
|
|
let (ty, hyps) = List.hd !subgoals in
|
|
subgoals := List.tl !subgoals;
|
|
|
|
if is_interactive then (
|
|
(* Nettoyage du terminal *)
|
|
let _ = Sys.command("clear -x") in
|
|
|
|
(* Affichage des hypothèses *)
|
|
List.iter (fun (var, h) -> Printf.printf "%s: %s\n" var (string_of_ty h)) hyps;
|
|
|
|
(* 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
|
|
|
|
let f = !fill_holes in
|
|
|
|
match tactic with
|
|
| Intro var -> (
|
|
match ty with
|
|
| TImpl (ty1, ty2) -> (
|
|
subgoals := (ty2, (var, ty1) :: hyps) :: !subgoals;
|
|
fill_holes := fun holes -> match holes with
|
|
| h :: hs -> f (LFun (var, ty1, h) :: hs)
|
|
| _ -> fail ()
|
|
)
|
|
| _ -> failwith "Can't intro"
|
|
)
|
|
| Assumption -> (
|
|
let rec explore = function
|
|
| (var, hyp) :: _ when hyp = ty -> (
|
|
fill_holes := fun holes -> f ((LVar var) :: holes)
|
|
)
|
|
| [] -> failwith "No such hypothesis"
|
|
| _ :: hyps -> explore hyps
|
|
in
|
|
explore hyps
|
|
)
|
|
done;
|
|
|
|
Printf.printf "Final proof :\n%s\n" (string_of_lam (!fill_holes []));;
|