pieuvre/main.ml

open Parser_entry
open Affichage
open Proof
open Types
open Hlam
open Lam


type entry =
  Simple of (unit -> instr)
  | Reduce of Lam.lam
  | AlphaEquiv of Lam.lam * Lam.lam

type interactive_state = (hlam * ty) option * proof

module StringMap = Map.Make(String)

let parse_lam t =
  match Parser.main Lexer.token t with
  | Lam l -> l
  | Instr _ -> failwith "entry must be a lam"

let parse_cmd t =
  match Parser.main Lexer.token t with
  | Instr is -> is
  | Lam _ -> failwith "entry must be a cmd"

let show_beta_reduction e =
  let rec aux = function
    Some e ->
      print_expr e;
      print_newline ();
      aux (Lam.betastep e);
    | None -> ()
  in print_expr e;
  print_newline ();
  let e = Lam.alpha_convert ~readable:true e in
  print_expr e;
  print_newline ();
  aux (Lam.betastep e)

let rec beta_reduce (l : Lam.lam) =
  match Lam.betastep l with
  | None -> l
  | Some l' -> beta_reduce l'

let clean_state ((s, p) : interactive_state) =
  let assoc, new_p = clean_proof p in
  match s with
  | None -> None, new_p
  | Some (hl, ty) -> Some (clean_hlam assoc hl, ty), new_p

let alpha_get_lam where_from =
  let input_str = In_channel.input_all where_from in
  match Str.split (Str.regexp "&") input_str with
    [s1; s2] -> AlphaEquiv (
          parse_lam (Lexing.from_string (s1^"\n")),
          parse_lam (Lexing.from_string s2)
        )
    | _ -> failwith "Alpha-equivalence: nombre de delimiteurs incorrect"

let check_via_coq (e : lam) (t : ty) : unit =
  (* fill a map to track all types used in the proof *)
  let rec fill_ty_map (m : int StringMap.t) = function
    TVar x -> StringMap.add x 0 m
    | Arr(t1, t2) | Or(t1, t2) | And(t1, t2) ->
      let m1 = fill_ty_map m t1 in
      fill_ty_map m1 t2
    | Bot -> m
  (* generate the "forall A B.." *)
  in let intro_of_ty (m : int StringMap.t) : string * int =
    let tys = StringMap.to_list m in
    let n = List.length tys in
    let s = List.fold_left (fun acc x -> (fst x ^ " ") ^ acc) "" tys in
    if n = 0
    then ("", 0)
    else ("forall " ^ s ^ ", ", n)
  (* generate the right amount of intro. to introduce type variables*)
  in let rec repeat_intro n =
    if n = 0
    then ""
    else "intro. " ^ repeat_intro (n-1)
  in
  (* build checker.v *)
  let m = fill_ty_map StringMap.empty t in
  let (ty_vars, intro_n) = intro_of_ty m in
  let goal_ty = string_of_ty t in
  let proof_term = "(" ^ string_of_expr e ^ ")" in
  let checker_file = open_out "checker.v" in
  let _ =
  Printf.fprintf checker_file "Goal %s%s.\n%s\n exact %s.\n"
  ty_vars goal_ty (repeat_intro intro_n) proof_term;
  close_out checker_file in
  (* start Coq in interactive mode and send it the proof term
     while blocking coqtop to print on stdout *)
  let r = Unix.system "coqtop < checker.v > log 2>&1" in
  match r with
  Unix.WEXITED x ->
    if x = 0
    then print_error "Validated by Coq." ""
    else print_error "Couldn't not validate proof." ""
  | _ -> print_error "Coq failed." ""



(** Interactive loop
  - cg : current top goal : type and reference to lambda-term
  - g, gs : next goals
  - sq : previous states of the interactive loop
*)
let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list) : proof =
  let (cg, (g, gs)), sq = match sl with
    [] -> (None, (None, [])), []
    | s::sq -> s, sq
  in
  begin
    let _ = match g with
    None -> print_string "\n\027[1mNo more goals.\027[0m\n"
    | Some g' -> print_newline (); print_goal g'
    in

    try
      match get_instr () with
      Cmd c ->
        begin match c with
        Goal ty ->
          let rh = Ref (ref Hole) in
          [Some (rh, ty), (Some (rh, ty, []), [])] |> interactive get_instr
        | Undo -> interactive get_instr sq
        | Qed -> begin match cg with
          None ->
            print_error "No current goal" "";
            (cg, (g, gs))::sq |> interactive get_instr
          | Some (h, t) ->
            let l = lam_of_hlam h
            |> beta_reduce in
            (* uncaught Could_not_infer but won't happened
               because exact only allow typable terms *)
            if Typing.typecheck [] l t then begin
              print_string "Ok";
              (cg, (g, gs))::sq |> interactive get_instr
            end else begin
              print_error "Typing failed" "";
              print_expr l;
              print_newline ();
              print_ty t;
              (cg, (g, gs))::sq |> interactive get_instr
            end
          end
        | Check -> begin match cg with
          (* !! Doesn't work with terms containing exfalso
                and Left / Right !! *)
          None ->
            print_error "No current goal" "";
            (cg, (g, gs))::sq |> interactive get_instr
          | Some (h, t) ->
            begin try
              let l = lam_of_hlam h in
              check_via_coq l t
            with _ -> print_error "Proof is not over" "";
            end;
            (cg, (g, gs))::sq |> interactive get_instr;
          end
        end
      | Tact t ->
        (cg, (apply_tactic (g, gs) t))::(clean_state (cg, (g, gs)))::sq |> interactive get_instr
    with
      Parser.Error ->
        print_error "Invalid input" "";
        (cg, (g, gs))::sq |> interactive get_instr
      | TacticFailed arg ->
        print_error "Tactic failed" arg;
        (cg, (g, gs))::sq |> interactive get_instr
      | End_of_file | Lexer.Eof ->
        print_string "Bye!\n";
        (g, gs)
  end

let nom_fichier = ref ""
let reduce = ref false
let alpha = ref false
let equiv_fichier = ref ""


let recupere_entree () =
  let optlist = [
   ("-alpha",
   Arg.Set alpha,
   "Vérifie l'alpha équivalence de deux termes séparés par &");
   ("-reduce",
   Arg.Set reduce,
   "Affiche les réductions successives du lambda-terme")
  ] in

  let usage = "Bienvenue à bord." in  (* message d'accueil, option -help *)

  Arg.parse (* ci-dessous les 3 arguments de Arg.parse : *)
    optlist (* la liste des options definie plus haut *)

    (fun s -> nom_fichier := s) (* la fonction a declencher lorsqu'on recupere un string qui n'est pas une option : ici c'est le nom du fichier, et on stocke cette information dans la reference nom_fichier *)
    usage; (* le message d'accueil *)

  try
    let where_from = match !nom_fichier with
      | "" -> stdin
      | s -> open_in s in
    if !alpha
    then alpha_get_lam where_from
    else if !reduce
    then Reduce (Lexing.from_channel where_from |> parse_lam)
    else Simple begin
    let cmd_buff = ref [] in
      if !nom_fichier = "" then
        (
          fun () ->
          match !cmd_buff with
          | [] ->
            begin match (read_line ())^"\n"
            |> Lexing.from_string
            |> parse_cmd with
              [] -> raise Parser.Error
              | e::q -> cmd_buff := q; e
            end
          | e::q -> cmd_buff := q; e
        )
      else
        (
          fun () ->
          match !cmd_buff with
          | [] ->
            begin match (input_line where_from)^"\n"
            |> Lexing.from_string
            |> parse_cmd with
              [] -> raise End_of_file
              | e::q -> cmd_buff := q; e
              end
          | e::q -> cmd_buff := q; e
        )
    end
  with e -> (print_error "problème de saisie" ""; raise e)

(* la fonction principale *)
let run () =
  try
    match recupere_entree () with
     Simple get_instr ->
      let _ = interactive get_instr [None, (None, [])] in ()
    | Reduce l ->
      let _ = show_beta_reduction l in ()
    | AlphaEquiv (l1, l2) -> begin
        if ((Lam.(=~)) l1 l2) then
          print_string "true\n"
        else
          print_string "false\n"
      end;
    flush stdout
  with e -> raise e

let _ = run ()