Read .8pus files

lexer.mll

@@ -12,8 +12,7 @@ let var_id = lowercase lowercase* digit*
 let ty_id = uppercase uppercase* digit*
 
 rule token = parse
-  | [' ' '\t']     { token lexbuf }
+  | [' ' '\t' '\n']      { token lexbuf }
-  | '\n'            { EOL }
   | '.'             { DOT }
   | '+'             { PLUS }
   | '*'             { TIMES }
@@ -45,4 +44,4 @@ rule token = parse
 
   | var_id as s     { VARID(s) }
   | ty_id as s      { TYID(s) }
-  | eof             { raise Eof }
+  | eof             { EOF }

main.ml

@@ -1,11 +1,10 @@
 open Parser_entry
 open Affichage
-open Typing
 open Proof
 open Types
 
 type entry =
-  Simple of Lam.lam
+  Simple of (unit -> cmd)
   | Reduce of Lam.lam
   | AlphaEquiv of Lam.lam * Lam.lam
 
@@ -60,7 +59,7 @@ let alpha_get_lam where_from =
   - g, gs : next goals
   - sq : previous states of the interactive loop
 *)
-let rec interactive (sl : (interactive_state) list) : proof =
+let rec interactive (get_cmd : unit -> cmd) (sl : (interactive_state) list) : proof =
   let (cg, (g, gs)), sq = match sl with
     [] -> (None, (None, [])), []
     | s::sq -> s, sq
@@ -72,60 +71,48 @@ let rec interactive (sl : (interactive_state) list) : proof =
     in
 
     try
-      match parse_cmd (Lexing.from_string ((read_line ())^"\n")) with
+      match get_cmd () with
       Goal ty ->
         let rh = Ref (ref Hole) in
-        interactive [Some (rh, ty), (Some (rh, ty, []), [])]
+        [Some (rh, ty), (Some (rh, ty, []), [])] |> interactive get_cmd
-      | Undo -> interactive sq
+      | Undo -> interactive get_cmd sq
       | Qed -> begin match cg with
         None ->
           print_error "No current goal" "";
-          (cg, (g, gs))::sq |> interactive
+          (cg, (g, gs))::sq |> interactive get_cmd
         | 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, [])]
+            [None, (None, [])] |> interactive get_cmd
           end else begin
             print_error "Typing failed" "";
             (* print_expr l;
             print_newline ();
             print_ty t; *)
-            (cg, (g, gs))::sq |> interactive
+            (cg, (g, gs))::sq |> interactive get_cmd
           end
         end
       | Tact t ->
-        (cg, (apply_tactic (g, gs) t))::(clean_state (cg, (g, gs)))::sq |> interactive
+        (cg, (apply_tactic (g, gs) t))::(clean_state (cg, (g, gs)))::sq |> interactive get_cmd
     with
       Parser.Error ->
         print_error "Invalid input" "";
-        (cg, (g, gs))::sq |> interactive
+        (cg, (g, gs))::sq |> interactive get_cmd
       | TacticFailed arg ->
         print_error "Tactic failed" arg;
-        (cg, (g, gs))::sq |> interactive
+        (cg, (g, gs))::sq |> interactive get_cmd
-      | End_of_file ->
+      | End_of_file | Lexer.Eof ->
         print_string "Bye!\n";
         (g, gs)
   end
 
-let interpret e =
-  begin
-    print_expr e;
-    print_newline();
-    print_ty (typeinfer [] e);
-    print_newline();
-    let _ = interactive [None, (None, [])] in ()
-  end
-
 let nom_fichier = ref ""
 let reduce = ref false
 let alpha = ref false
 let equiv_fichier = ref ""
 
-let parse_channel_lam c =
-  let lexbuf = Lexing.from_channel c in
-  parse_lam lexbuf
 
 let recupere_entree () =
   let optlist = [
@@ -152,16 +139,46 @@ let recupere_entree () =
     if !alpha
     then alpha_get_lam where_from
     else if !reduce
-    then Reduce (parse_channel_lam where_from)
+    then Reduce (Lexing.from_channel where_from |> parse_lam)
-    else Simple (parse_channel_lam where_from)
+    else Simple begin
+    let cmd_buff = ref [] in
+      if !nom_fichier = "" then
+        (
+          fun () ->
+          match !cmd_buff with
+          | [] ->
+            begin match (read_line ())^"\n"
+            |> Lexing.from_string
+            |> parse_cmd with
+              [] -> raise Parser.Error
+              | e::q -> cmd_buff := q; e
+            end
+          | e::q -> cmd_buff := q; e
+        )
+      else
+        (
+          fun () ->
+          match !cmd_buff with
+          | [] ->
+            begin match (input_line where_from)^"\n"
+            |> Lexing.from_string
+            |> parse_cmd with
+              [] -> raise End_of_file
+              | e::q -> cmd_buff := q; e
+              end
+          | e::q -> cmd_buff := q; e
+        )
+    end
   with e -> (print_error "problème de saisie" ""; raise e)
 
 (* la fonction principale *)
 let run () =
   try
     match recupere_entree () with
-     Simple l -> let _ = interpret l in ()
+     Simple get_cmd ->
-    | Reduce l -> let _ = show_beta_reduction l in ()
+      let _ = interactive get_cmd [None, (None, [])] in ()
+    | Reduce l ->
+      let _ = show_beta_reduction l in ()
     | AlphaEquiv (l1, l2) -> begin
         if ((Lam.(=~)) l1 l2) then
           print_string "true\n"

parser.mly

@@ -5,6 +5,8 @@ open Proof
 open Parser_entry
 %}
 
+%token EOF
+
 %token DOT
 %token PLUS TIMES
 %token TOP BOT EXFALSO TILDE
@@ -18,7 +20,6 @@ open Parser_entry
 %token EXACT ASSUMPTION INTRO INTROS CUT APPLY
 %token LEFT RIGHT SPLIT
 
-%token EOL
 %right TARR
 %right OR
 %right AND
@@ -29,8 +30,8 @@ open Parser_entry
                                                          
 %%
 main:
-  | e=expression EOL { Lam e }
+  | e=expression EOF { Lam e }
-  | t=tactic EOL { Cmd t }
+  | ts=nonempty_list(tactic) EOF { Cmd ts }
 
 tactic:
   | c=command DOT { c }

parser_entry.ml

@@ -10,4 +10,4 @@ type cmd =
 
 type parser_entry =
   | Lam of lam
-  | Cmd of cmd
+  | Cmd of cmd list