open Parser_entry open Affichage open Proof open Types open Hlam open Lam exception InputError of string 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 _ -> raise (InputError "entry must be a lam") let parse_cmd t = match Parser.main Lexer.token t with | Instr is -> is | Lam _ -> raise (InputError "entry must be an instruction") 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' (* copier l'entièreté de l'état d'une preuve avec de nouvelles références pour le Undo *) let clean_state ((s, p) : interactive_state) = (* assoc fait le lien entre les anciennes et nouvelles ref, doit être commun au terme et aux différents composants de la preuve *) 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 (* affichage de l'état de la preuve *) None -> print_string "\n\027[1mNo more goals.\027[0m\n" | Some g' -> print_newline (); print_goal g' in try match get_instr () with (* get_instr récupère l'instruction suivante depuis un fichier ou stdin (garde en buffer les lignes doubles notamment) *) 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 (* pour Undo, on appelle juste interactive en supprimant le dernier état *) | 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 -> (* on applique la tactique et on copie l'état actuel de la preuve pour un futur Undo Comme OCaml évalue de la droite vers la gauche, on fait bien la copie avant de modifier les références dans la preuve *) (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 | InputError arg -> print_error "Invalid input" 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 ((* récupérer les commandes depuis stdin, les lignes vides sont considérées comme des erreurs *) 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 ((* récupérer les commandes depuis un fichier *) 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 ()