Better errors & add colors

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

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 ->
+      | TacticFailed arg ->
-        print_string "Tactic failed.\n";
+        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 () =

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