278 lines
8.4 KiB
OCaml
278 lines
8.4 KiB
OCaml
open Structs;;
|
||
open Pieuvre;;
|
||
|
||
let fail () =
|
||
failwith "Unknown error";;
|
||
|
||
(* Parsage des arguments*)
|
||
let filename = ref "" in
|
||
|
||
let reduce_option = ref false in
|
||
let alpha_option = ref false in
|
||
let typecheck_option = ref false in
|
||
|
||
Arg.parse
|
||
[("-reduce", Arg.Set reduce_option, "Show the step-by-step reduction of a lambda-term");
|
||
("-alpha", Arg.Set alpha_option, "Check is two lambda-terms separated by '&' are alpha-convertible");
|
||
("-typecheck", Arg.Set typecheck_option, "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
|
||
|
||
if !reduce_option then (
|
||
let lexbuf = Lexing.from_channel (match file with
|
||
| None -> stdin
|
||
| Some file -> file
|
||
)
|
||
in
|
||
let lambda_term =
|
||
try
|
||
Parser.main_lambda Lexer.token lexbuf
|
||
with e -> (
|
||
Printf.printf "Can't read lambda term\n";
|
||
raise e
|
||
)
|
||
in
|
||
reduce lambda_term;
|
||
exit 0
|
||
);
|
||
|
||
if !alpha_option then (
|
||
let lexbuf = Lexing.from_channel (match file with
|
||
| None -> stdin
|
||
| Some file -> file
|
||
)
|
||
in
|
||
let lam1, lam2 =
|
||
try
|
||
Parser.main_two_lambda Lexer.token lexbuf
|
||
with e -> (
|
||
Printf.printf "Can't read lambda terms\n";
|
||
raise e
|
||
)
|
||
in
|
||
if alpha lam1 lam2 then (
|
||
Printf.printf "%s and %s are α-equivalent\n" (string_of_lam lam1) (string_of_lam lam2)
|
||
) else (
|
||
Printf.printf "%s and %s are not α-equivalent\n" (string_of_lam lam1) (string_of_lam lam2)
|
||
);
|
||
exit 0
|
||
);
|
||
|
||
if !typecheck_option then (
|
||
let lexbuf = Lexing.from_channel (match file with
|
||
| None -> stdin
|
||
| Some file -> file
|
||
)
|
||
in
|
||
let lambda_term =
|
||
try
|
||
Parser.main_lambda Lexer.token lexbuf
|
||
with e -> (
|
||
Printf.printf "Can't read lambda term\n";
|
||
raise e
|
||
)
|
||
in
|
||
Printf.printf "The type of %s is " (string_of_lam lambda_term);
|
||
if typecheck lambda_term then (
|
||
Printf.printf "correct\n"
|
||
) else (
|
||
Printf.printf "incorrect\n"
|
||
);
|
||
exit 0
|
||
);
|
||
|
||
(* 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 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;
|
||
|
||
let find_hyp (var: var_lambda) : ty option =
|
||
let rec explore = function
|
||
| [] -> None
|
||
| (var_hyp, hyp) :: hyps when var_hyp = var -> Some hyp
|
||
| _ :: hyps -> explore hyps
|
||
in
|
||
explore hyps
|
||
in
|
||
|
||
|
||
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);
|
||
List.iter (fun (ty, _) ->
|
||
Printf.printf "%s\n" (string_of_ty ty)
|
||
) !subgoals;
|
||
|
||
(* 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 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
|
||
)
|
||
| Apply var -> (
|
||
match find_hyp var with
|
||
| Some (TImpl (t1, t2)) when t2 = ty -> (
|
||
subgoals := (t1, hyps) :: !subgoals;
|
||
fill_holes := function
|
||
| hole :: holes -> f ((LApp (LVar var, hole)) :: holes)
|
||
| [] -> fail ()
|
||
)
|
||
| None -> failwith ("Hypothesis " ^ var ^ " not found")
|
||
| _ -> failwith ("Hypothesis " ^ var ^ " unusable")
|
||
)
|
||
| Elim var -> (
|
||
match find_hyp var with
|
||
| Some TFalse -> fill_holes := fun holes -> f ((LExf (LVar var, ty)) :: holes)
|
||
| Some TAnd(tl,tr) -> (
|
||
subgoals := (TImpl(tl,TImpl(tr,ty)),hyps)::!subgoals;
|
||
fill_holes := fun holes -> match holes with
|
||
| h::r -> f ((LApp(LApp(h,LFst(LVar(var))),LSnd(LVar(var))))::r)
|
||
| _ -> fail ()
|
||
)
|
||
| Some TOr(tl,tr) -> (
|
||
subgoals := (TImpl(tl,ty),hyps)::(TImpl(tr,ty),hyps)::!subgoals;
|
||
fill_holes := fun holes -> match holes with
|
||
| hl::hr::r -> f (LCase(LVar(var),hl,hr)::r)
|
||
| _ -> fail ()
|
||
)
|
||
| None -> failwith ("Hypothesis " ^ var ^ " not found")
|
||
| _ -> failwith ("Hypothesis " ^ var ^ " unusable")
|
||
)
|
||
(* Pour montrer A, on montre B -> A et B *)
|
||
| Cut tint -> (
|
||
subgoals := (TImpl (tint, ty), hyps) :: (tint, hyps) :: !subgoals;
|
||
fill_holes := function
|
||
| pf :: px :: s -> f ((LApp (pf, px)) :: s)
|
||
| _ -> fail ()
|
||
)
|
||
|
||
| Split ovar -> (
|
||
match ty with
|
||
| TAnd(t1,t2) -> (
|
||
subgoals := (t1, hyps) :: (t2, hyps) :: !subgoals;
|
||
fill_holes := fun holes -> match holes with
|
||
| h1 :: h2 :: hs -> f (LCouple(h1,h2) :: hs)
|
||
| _ -> fail ()
|
||
)
|
||
| _ -> failwith "Target not a and clause"
|
||
)
|
||
| Left -> (
|
||
match ty with
|
||
| TOr(tl,tr) -> (
|
||
subgoals := (tl, hyps) :: !subgoals;
|
||
fill_holes := fun holes -> match holes with
|
||
| hl :: hs -> f (LIg(hl,tr) :: hs)
|
||
| _ -> fail ()
|
||
)
|
||
| _ -> failwith "Target not a or clause"
|
||
)
|
||
| Right -> (
|
||
match ty with
|
||
| TOr(tl,tr) -> (
|
||
subgoals := (tr, hyps) :: !subgoals;
|
||
fill_holes := fun holes -> match holes with
|
||
| hr :: hs -> f (LId(hr,tl) :: hs)
|
||
| _ -> fail ()
|
||
)
|
||
| _ -> failwith "Target not a or clause"
|
||
)
|
||
done;
|
||
|
||
let finalLam = !fill_holes [] in
|
||
if (typecheck [] finalLam ty) then (
|
||
Printf.printf "Final proof :\n";
|
||
reduce finalLam
|
||
)
|
||
else (
|
||
Printf.printf "Invalid proof constructed!\n";
|
||
Printf.printf "%s can't be typed with %s.\n" (string_of_lam finalLam) (string_of_ty ty);
|
||
Printf.printf "The whole development team of pieuvre is sorry for the damage eventually done by this error.\n"
|
||
)
|
||
;;
|