From 8569fe1ba26b92c9e32db331e4436e2a1fe1ef85 Mon Sep 17 00:00:00 2001
From: augustin64 <me.git@augustin64.fr>
Date: Sat, 11 May 2024 11:44:43 +0200
Subject: [PATCH] Add Undo command

---
 lexer.mll       |  1 +
 main.ml         | 17 +++++++++--------
 parser.mly      |  3 ++-
 parser_entry.ml |  1 +
 proof.ml        | 36 +++++++++++++++++++++++++++++++++---
 5 files changed, 46 insertions(+), 12 deletions(-)

diff --git a/lexer.mll b/lexer.mll
index 1824b09..4f48dbe 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -31,6 +31,7 @@ rule token = parse
   | "\\/"           { OR }
 
   | "Goal"          { GOAL }
+  | "Undo"          { UNDO }
   | "exact"         { EXACT }
   | "assumption"    { ASSUMPTION }
   | "intros"        { INTROS }
diff --git a/main.ml b/main.ml
index 10e8485..3990882 100644
--- a/main.ml
+++ b/main.ml
@@ -43,7 +43,7 @@ let alpha_get_lam where_from =
         )
     | _ -> failwith "Alpha-equivalence: nombre de delimiteurs incorrect"
 
-let rec interactive ((g, gs) : proof) : proof =
+let rec interactive ((g, gs)::gq : proof list) : proof =
   begin
     let fresh_proof (ty : ty) =
       (Some (Ref (ref Hole), ty, []), [])
@@ -56,18 +56,19 @@ let rec interactive ((g, gs) : proof) : proof =
 
     try
       match parse_cmd (Lexing.from_string ((read_line ())^"\n")) with
-      Goal ty -> fresh_proof ty |> interactive
-      | Tact t -> apply_tactic (g, gs) t |> interactive
+      Goal ty -> [fresh_proof ty] |> interactive
+      | Undo -> interactive gq
+      | Tact t -> (apply_tactic (g, gs) t)::(clean_proof (g, gs))::gq |> interactive
     with
       Parser.Error ->
         print_error "Invalid input" "";
-        interactive (g, gs)
+        (g, gs)::gq |> interactive
+      | TacticFailed arg ->
+        print_error "Tactic failed" arg;
+        (g, gs)::gq |> interactive
       | End_of_file ->
         print_string "Bye!\n";
         (g, gs)
-      | TacticFailed arg ->
-        print_error "Tactic failed" arg;
-        interactive (g, gs)
   end
 
 let interpret e =
@@ -76,7 +77,7 @@ let interpret e =
     print_newline();
     print_ty (typeinfer [] e);
     print_newline();
-    let _ = interactive (None, []) in ()
+    let _ = interactive [(None, [])] in ()
   end
 
 let nom_fichier = ref ""
diff --git a/parser.mly b/parser.mly
index 47c5710..2adade6 100644
--- a/parser.mly
+++ b/parser.mly
@@ -14,7 +14,7 @@ open Parser_entry
 %token <string> VARID
 %token <string> TYID
 
-%token GOAL EXACT ASSUMPTION INTRO INTROS CUT APPLY
+%token GOAL UNDO EXACT ASSUMPTION INTRO INTROS CUT APPLY
 %token LEFT RIGHT SPLIT
 
 %token EOL
@@ -36,6 +36,7 @@ tactic:
 
 command:
   | GOAL t=ty             { Goal t }
+  | UNDO                  { Undo }
   | EXACT e=expression    { Tact (Exact_term e) }
   | EXACT s=TYID          { Tact (Exact_proof s) }
   | ASSUMPTION            { Tact (Assumption) }
diff --git a/parser_entry.ml b/parser_entry.ml
index 7906515..fcd8066 100644
--- a/parser_entry.ml
+++ b/parser_entry.ml
@@ -4,6 +4,7 @@ open Proof
 
 type cmd =
   | Goal of ty
+  | Undo
   | Tact of tactic
 
 type parser_entry =
diff --git a/proof.ml b/proof.ml
index ae9ceba..4dd531f 100644
--- a/proof.ml
+++ b/proof.ml
@@ -27,14 +27,44 @@ type tactic =
   | Right
   | Left
 
-let count = ref 0
+let hyp_count = ref 0
 let get_fresh_hyp () =
-  let n = string_of_int !count in
-  incr count;
+  let n = string_of_int !hyp_count in
+  incr hyp_count;
   let hyp_id = "H" ^ n in
   let var_id = "x_" ^ n in
   (hyp_id, var_id)
 
+(** replace ref's in a proof *)
+let clean_proof ((g, gs) : proof) : proof =
+  let assoc = ref [] in
+  let clean_hlam (h : hlam) : hlam =
+    let rec clean (h : hlam) : hlam= match h with
+      HFun ((s, t), h) -> HFun ((s, t), clean h)
+      | Hole -> Hole
+      | HApp (h1, h2) -> HApp (clean h1, clean h2)
+      | HVar s -> HVar s
+      | HExf (h, t) -> HExf (clean h, t)
+      | Ref (hr) ->
+        match List.assq_opt hr !assoc with
+          None -> let new_h = ref (clean !hr)
+            in (assoc := (hr, new_h)::!assoc;
+            Ref new_h)
+          | Some new_h -> Ref new_h
+    in clean h
+  in
+  let rec clean_context (c : context) : context = match c with
+    [] -> []
+    | (s1, s2, h, t)::q -> (s1, s2, clean_hlam h, t)::(clean_context q)
+  in
+  let clean_goal ((h, t, c) : goal) : goal =
+    (clean_hlam h, t, clean_context c)
+  in
+  let g' = match g with 
+    | Some g -> Some (clean_goal g)
+    | None -> None
+  in (g', List.map clean_goal gs)
+
 let goal_is_over ((g, _) : proof) : bool =
   match g with
   None -> true