From 0085a91251926fb9ba60dc7a89bd6d225475a1ac Mon Sep 17 00:00:00 2001 From: augustin64 Date: Wed, 1 May 2024 11:07:40 +0200 Subject: [PATCH] Better errors & add colors --- affichage.ml | 10 ++++++++-- main.ml | 10 +++++----- proof.ml | 28 ++++++++++++++-------------- 3 files changed, 27 insertions(+), 21 deletions(-) diff --git a/affichage.ml b/affichage.ml index 78c8638..bdedac4 100644 --- a/affichage.ml +++ b/affichage.ml @@ -35,8 +35,14 @@ let print_goal ((_, ty, c) : goal) : unit = let rec print_hyps (c : context) : unit = match c with [] -> () | (id, _, ty)::q -> print_string (id^" : "^(string_of_ty ty)^"\n"); print_hyps q - in print_hyps c; + in + print_string "\027[1m"; + print_hyps c; print_ty ty; - print_string "\n==========\n" + print_string "\n==========\027[0m\n" let affiche_val _ = print_string "TODO" + +let print_error (error_type : string) (details : string) = + output_string stderr ("\027[1;31mError:\027[0m \027[34m"^error_type^"\027[0m "^details^"\n"); + flush stderr \ No newline at end of file diff --git a/main.ml b/main.ml index f519bf7..10e8485 100644 --- a/main.ml +++ b/main.ml @@ -50,7 +50,7 @@ let rec interactive ((g, gs) : proof) : proof = in let _ = match g with - None -> print_string "\nNo more goals.\n" + None -> print_string "\n\027[1mNo more goals.\027[0m\n" | Some g' -> print_newline (); print_goal g' in @@ -60,13 +60,13 @@ let rec interactive ((g, gs) : proof) : proof = | Tact t -> apply_tactic (g, gs) t |> interactive with Parser.Error -> - print_string "Invalid input.\n"; + print_error "Invalid input" ""; interactive (g, gs) | End_of_file -> print_string "Bye!\n"; (g, gs) - | TacticFailed -> - print_string "Tactic failed.\n"; + | TacticFailed arg -> + print_error "Tactic failed" arg; interactive (g, gs) end @@ -115,7 +115,7 @@ let recupere_entree () = else if !reduce then Reduce (parse_channel_lam where_from) else Simple (parse_channel_lam where_from) - with e -> (Printf.printf "problème de saisie\n"; raise e) + with e -> (print_error "problème de saisie" ""; raise e) (* la fonction principale *) let run () = diff --git a/proof.ml b/proof.ml index 61bf00e..35185d3 100644 --- a/proof.ml +++ b/proof.ml @@ -1,7 +1,7 @@ open Lam open Types -exception TacticFailed +exception TacticFailed of string type hlam = (* hollow lam *) HFun of (id * Types.ty) * hlam @@ -40,7 +40,7 @@ let proof_is_over ((g, _) : proof) : bool = let fill (hole : hlam) (e : hlam) : unit = match hole with Ref h -> h := e - | _ -> failwith "not fillable" + | _ -> raise (TacticFailed "not fillable") let rec hlam_of_lam : lam -> hlam = function Fun ((x, t), e) -> @@ -68,7 +68,7 @@ let rec lam_of_hlam : hlam -> lam = function let e = lam_of_hlam e in Exf (e, t) | Ref e_ref -> lam_of_hlam !e_ref - | Hole -> failwith "can not translate unclosed terms" + | Hole -> raise (TacticFailed "can not translate unclosed terms") let rec get_term_by_id (hyp : id) : context -> hlam option = @@ -90,24 +90,24 @@ let next_goal (gs : goal list) : (goal option * goal list) = let tact_exact_term ((g, gs) : proof) (e : lam) : proof = match g with - None -> failwith "no current goal" + None -> raise (TacticFailed "no current goal") | Some (h, _, _) -> fill h (hlam_of_lam e); next_goal gs let tact_exact_proof ((g, gs) : proof) (hyp : id) : proof = match g with - None -> failwith "no current goal" + None -> raise (TacticFailed "no current goal") | Some (h, _, cs) -> match get_term_by_id hyp cs with Some h' -> fill h h'; next_goal gs - | None -> raise TacticFailed + | None -> raise (TacticFailed "") let tact_assumption ((g, gs) : proof) : proof = match g with - None -> failwith "no current goal" + None -> raise (TacticFailed "no current goal") | Some (h, goal_ty, cs) -> match get_term_by_type goal_ty cs with None -> (* failwith "assumption failed" *) (g, gs) @@ -117,7 +117,7 @@ let tact_assumption ((g, gs) : proof) : proof = let tact_intro ((g, gs) : proof) : proof = match g with - None -> failwith "no current goal" + None -> raise (TacticFailed "no current goal") | Some (h, goal_ty, cs) -> match goal_ty with Arr (t1, t2) -> @@ -127,11 +127,11 @@ let tact_intro ((g, gs) : proof) : proof = fill h (HFun ((var_id, t1), new_h)); Some (new_h, t2, cs), gs | _ -> (* failwith "expected function" *) (* (g, gs) *) - raise TacticFailed + raise (TacticFailed "expected function") let tact_cut ((g, gs) : proof) (new_t : Types.ty) : proof = match g with - None -> failwith "no current goal" + None -> raise (TacticFailed "no current goal") | Some (h, goal_ty, cs) -> (* subgoal 2 : new_t -> goal_ty *) let arrow_h = Ref (ref Hole) in @@ -144,12 +144,12 @@ let tact_cut ((g, gs) : proof) (new_t : Types.ty) : proof = let tact_apply ((g, gs) : proof) (hyp_id : id) : proof = let rec get_hyp = function - [] -> failwith "no such hypothesis in context" + [] -> raise (TacticFailed "no such hypothesis in context") | (hyp_id', h', t') :: _ when hyp_id = hyp_id' -> (h', t') | _ :: cs -> get_hyp cs in match g with - None -> failwith "no current goal" + None -> raise (TacticFailed "no current goal") | Some (h, goal_ty, cs) -> let h', t' = get_hyp cs in match t' with @@ -165,7 +165,7 @@ let tact_intros : proof -> proof = try let p = tact_intro p in push p - with TacticFailed -> p + with TacticFailed _ -> p in push let apply_tactic (p : proof) (t : tactic) : proof = @@ -181,4 +181,4 @@ let apply_tactic (p : proof) (t : tactic) : proof = let tact_try (p : proof) (t : tactic) : proof = try apply_tactic p t - with TacticFailed -> p + with TacticFailed _ -> p