pieuvre/main.ml

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
);

(* 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)
              | 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 ()
        )
done;

let finalLam = !fill_holes [] in
    if (typecheck [] finalLam ty) then
        Printf.printf "Final proof :\n%s\n" (string_of_lam 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"
    )
;;