Add Qed.

lexer.mll

@@ -32,6 +32,7 @@ rule token = parse
 
   | "Goal"          { GOAL }
   | "Undo"          { UNDO }
+  | "Qed"           { QED }
   | "exact"         { EXACT }
   | "assumption"    { ASSUMPTION }
   | "intros"        { INTROS }

main.ml

@@ -9,6 +9,7 @@ type entry =
   | Reduce of Lam.lam
   | AlphaEquiv of Lam.lam * Lam.lam
 
+type interactive_state = (hlam * ty) option * proof
 
 let parse_lam t =
   match Parser.main Lexer.token t with
@@ -20,7 +21,7 @@ let parse_cmd t =
   | Cmd c -> c
   | Lam _ -> failwith "entry must be a cmd"
 
-let beta_reduce e =
+let show_beta_reduction e =
   let rec aux = function
     Some e ->
       print_expr e;
@@ -34,6 +35,17 @@ let beta_reduce 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
@@ -43,12 +55,13 @@ let alpha_get_lam where_from =
         )
     | _ -> failwith "Alpha-equivalence: nombre de delimiteurs incorrect"
 
-let rec interactive ((g, gs)::gq : proof list) : proof =
+(** 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 ((cg, (g, gs))::sq : (interactive_state) list) : proof =
   begin
-    let fresh_proof (ty : ty) =
-      (Some (Ref (ref Hole), ty, []), [])
-    in
-
     let _ = match g with
     None -> print_string "\n\027[1mNo more goals.\027[0m\n"
     | Some g' -> print_newline (); print_goal g'
@@ -56,16 +69,34 @@ let rec interactive ((g, gs)::gq : proof list) : proof =
 
     try
       match parse_cmd (Lexing.from_string ((read_line ())^"\n")) with
-      Goal ty -> [fresh_proof ty] |> interactive
-      | Undo -> interactive gq
-      | Tact t -> (apply_tactic (g, gs) t)::(clean_proof (g, gs))::gq |> interactive
+      Goal ty ->
+        let rh = Ref (ref Hole) in
+        interactive [Some (rh, ty), (Some (rh, ty, []), [])]
+      | Undo -> interactive sq
+      | Qed -> begin match cg with
+        None ->
+          print_error "No current goal" "";
+          (cg, (g, gs))::sq |> interactive
+        | Some (h, t) ->
+          let l = lam_of_hlam h
+          |> beta_reduce in
+          if Typing.typecheck [] l t then begin
+            print_string "Ok";
+            interactive [None, (None, [])]
+          end else begin
+            print_error "Typing failed" "";
+            (cg, (g, gs))::sq |> interactive
+          end
+        end
+      | Tact t ->
+        (cg, (apply_tactic (g, gs) t))::(clean_state (cg, (g, gs)))::sq |> interactive
     with
       Parser.Error ->
         print_error "Invalid input" "";
-        (g, gs)::gq |> interactive
+        (cg, (g, gs))::sq |> interactive
       | TacticFailed arg ->
         print_error "Tactic failed" arg;
-        (g, gs)::gq |> interactive
+        (cg, (g, gs))::sq |> interactive
       | End_of_file ->
         print_string "Bye!\n";
         (g, gs)
@@ -77,7 +108,7 @@ let interpret e =
     print_newline();
     print_ty (typeinfer [] e);
     print_newline();
-    let _ = interactive [(None, [])] in ()
+    let _ = interactive [None, (None, [])] in ()
   end
 
 let nom_fichier = ref ""
@@ -123,7 +154,7 @@ let run () =
   try
     match recupere_entree () with
      Simple l -> let _ = interpret l in ()
-    | Reduce l -> let _ = beta_reduce l in ()
+    | Reduce l -> let _ = show_beta_reduction l in ()
     | AlphaEquiv (l1, l2) -> begin
         if ((Lam.(=~)) l1 l2) then
           print_string "true\n"

parser.mly

@@ -14,7 +14,8 @@ open Parser_entry
 %token <string> VARID
 %token <string> TYID
 
-%token GOAL UNDO EXACT ASSUMPTION INTRO INTROS CUT APPLY
+%token GOAL UNDO QED
+%token EXACT ASSUMPTION INTRO INTROS CUT APPLY
 %token LEFT RIGHT SPLIT
 
 %token EOL
@@ -37,6 +38,7 @@ tactic:
 command:
   | GOAL t=ty             { Goal t }
   | UNDO                  { Undo }
+  | QED                   { Qed }
   | EXACT e=expression    { Tact (Exact_term e) }
   | EXACT s=TYID          { Tact (Exact_proof s) }
   | ASSUMPTION            { Tact (Assumption) }

parser_entry.ml

@@ -5,8 +5,9 @@ open Proof
 type cmd =
   | Goal of ty
   | Undo
+  | Qed
   | Tact of tactic
 
 type parser_entry =
   | Lam of lam
-  | Cmd of cmd
+  | Cmd of cmd

proof.ml

@@ -36,34 +36,31 @@ let get_fresh_hyp () =
   (hyp_id, var_id)
 
 (** replace ref's in a proof *)
-let clean_proof ((g, gs) : proof) : proof =
+let clean_hlam assoc (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
+let rec clean_context assoc (c : context) : context = match c with
+  [] -> []
+  | (s1, s2, h, t)::q -> (s1, s2, clean_hlam assoc h, t)::(clean_context assoc q)
+let clean_goal assoc ((h, t, c) : goal) : goal =
+  (clean_hlam assoc h, t, clean_context assoc c)
+let clean_proof ((g, gs) : proof) : (hlam ref * hlam ref) list ref * 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)
+    | Some g -> Some (clean_goal assoc g)
     | None -> None
-  in (g', List.map clean_goal gs)
+  in assoc, (g', List.map (clean_goal assoc) gs)
 
 let goal_is_over ((g, _) : proof) : bool =
   match g with