Add interactive proofs

affichage.ml

@@ -1,5 +1,6 @@
 open Lam
 open Types
+open Proof
 
 (* fonction d'affichage *)
 let rec string_of_ty = function
@@ -30,5 +31,12 @@ let print_ty t =
 let print_expr e =
   print_string (string_of_expr e)
 
+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;
+  print_ty ty;
+  print_string "\n==========\n"
 
 let affiche_val _ = print_string "TODO"

lexer.mll

@@ -14,6 +14,7 @@ let ty_id = uppercase uppercase* digit*
 rule token = parse
   | [' ' '\t']     { token lexbuf }
   | '\n'            { EOL }
+  | '.'             { DOT }
   | '+'             { PLUS }
   | '*'             { TIMES }
   | "True"          { TOP }
@@ -26,6 +27,14 @@ rule token = parse
   | "->"            { TARR }
   | '~'             { TILDE }
   | "exf"           { EXFALSO }
+
+  | "Goal"          { GOAL }
+  | "exact"         { EXACT }
+  | "assumption"    { ASSUMPTION }
+  | "intro"         { INTRO }
+  | "cut"           { CUT }
+  | "apply"         { APPLY }
+
   | var_id as s     { VARID(s) }
   | ty_id as s      { TYID(s) }
   | eof             { raise Eof }

main.ml

@@ -1,5 +1,8 @@
+open Parser_entry
 open Affichage
 open Typing
+open Proof
+open Types
 
 type entry =
   Simple of Lam.lam
@@ -7,6 +10,16 @@ type entry =
   | AlphaEquiv of Lam.lam * Lam.lam
 
 
+let parse_lam t =
+  match Parser.main Lexer.token t with
+  | Lam l -> l
+  | Cmd _ -> failwith "entry must be a lam"
+
+let parse_cmd t =
+  match Parser.main Lexer.token t with
+  | Cmd c -> c
+  | Lam _ -> failwith "entry must be a cmd"
+
 let beta_reduce e =
   let rec aux = function
     Some e ->
@@ -25,17 +38,46 @@ 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 (
-          Parser.main Lexer.token (Lexing.from_string (s1^"\n")),
+          parse_lam (Lexing.from_string (s1^"\n")),
-          Parser.main Lexer.token (Lexing.from_string s2)
+          parse_lam (Lexing.from_string s2)
         )
     | _ -> failwith "Alpha-equivalence: nombre de delimiteurs incorrect"
 
+let rec interactive ((g, gs) : proof) : proof =
+  begin
+    let fresh_proof (ty : ty) =
+      (Some (Ref (ref Hole), ty, []), [])
+    in
+
+    let _ = match g with
+    None -> print_string "No more goals.\n"
+    | Some g' -> print_goal g'
+    in
+
+    match parse_cmd (Lexing.from_string ((read_line ())^"\n")) with
+    Goal ty -> fresh_proof ty |> interactive
+    | Tact t ->
+      begin match t with
+        Exact e ->
+          tact_exact (g, gs) e |> interactive
+        | Assumption ->
+          tact_assumption (g, gs) |> interactive
+        | Intro ->
+          tact_intro (g, gs) |> interactive
+        | Cut ty ->
+          tact_cut (g, gs) ty |> interactive
+        | Apply id ->
+          tact_apply (g, gs) id |> interactive
+      end
+  end
+
 let interpret e =
   begin
     print_expr e;
     print_newline();
     print_ty (typeinfer [] e);
-    print_newline()
+    print_newline();
+    let _ = interactive (None, []) in ()
   end
 
 let nom_fichier = ref ""
@@ -43,9 +85,9 @@ let reduce = ref false
 let alpha = ref false
 let equiv_fichier = ref ""
 
-let parse_channel c =
+let parse_channel_lam c =
   let lexbuf = Lexing.from_channel c in
-  Parser.main Lexer.token lexbuf
+  parse_lam lexbuf
 
 let recupere_entree () =
   let optlist = [
@@ -72,8 +114,8 @@ let recupere_entree () =
     if !alpha
     then alpha_get_lam where_from
     else if !reduce
-    then Reduce (parse_channel where_from)
+    then Reduce (parse_channel_lam where_from)
-    else Simple (parse_channel where_from)
+    else Simple (parse_channel_lam where_from)
   with e -> (Printf.printf "problème de saisie\n"; raise e)
 
 (* la fonction principale *)

parser.mly

@@ -1,8 +1,11 @@
 %{
 open Lam
 open Types
+open Proof
+open Parser_entry
 %}
 
+%token DOT
 %token PLUS TIMES
 %token TOP BOT EXFALSO TILDE
 %token LPAREN RPAREN
@@ -10,17 +13,32 @@ open Types
 %token <string> VARID
 %token <string> TYID
 
+%token GOAL EXACT ASSUMPTION INTRO CUT APPLY
+
 %token EOL
 
 %right TARR
 %right TILDE
 
 %start main
-%type <Lam.lam> main
+%type <parser_entry> main
                                                          
 %%
 main:
-e=expression EOL { e }
+  | e=expression EOL { Lam e }
+  | t=tactic EOL { Cmd t }
+
+tactic:
+  | c=command DOT { c }
+
+command:
+  | GOAL t=ty             { Goal t }
+  | EXACT e=expression    { Tact (Exact e) }
+  | ASSUMPTION            { Tact (Assumption) }
+  | INTRO                 { Tact (Intro) }
+  | CUT t=ty              { Tact (Cut t) }
+  | APPLY s=TYID          { Tact (Apply s) }
+
 
 ty_annot:
   | id=VARID COLON t=ty     { (id, t) }

parser_entry.ml

@@ -0,0 +1,11 @@
+open Lam
+open Types
+open Proof
+
+type cmd =
+  | Goal of ty
+  | Tact of tactic
+
+type parser_entry =
+  | Lam of lam
+  | Cmd of cmd

proof.ml

@@ -13,9 +13,17 @@ type context = (id * hlam * Types.ty) list
 type goal = hlam * Types.ty * context
 type proof = goal option * goal list
 
+type tactic =
+  Exact of lam
+  | Assumption
+  | Intro
+  | Cut of ty
+  | Apply of id
+
 let count = ref 0
 let get_fresh_hyp () =
   let n = string_of_int !count in
+  incr count;
   let hyp_id = "H" ^ n in
   let var_id = "x_" ^ n in
   (hyp_id, var_id)