From a42a34d3071201d19ed2a132f3b18cccbf8a5f1e Mon Sep 17 00:00:00 2001 From: augustin64 Date: Tue, 14 May 2024 11:43:57 +0200 Subject: [PATCH] Read .8pus files --- lexer.mll | 5 ++-- main.ml | 75 ++++++++++++++++++++++++++++++------------------- parser.mly | 7 +++-- parser_entry.ml | 2 +- 4 files changed, 53 insertions(+), 36 deletions(-) diff --git a/lexer.mll b/lexer.mll index 25a0352..af507a8 100644 --- a/lexer.mll +++ b/lexer.mll @@ -12,8 +12,7 @@ let var_id = lowercase lowercase* digit* let ty_id = uppercase uppercase* digit* rule token = parse - | [' ' '\t'] { token lexbuf } - | '\n' { EOL } + | [' ' '\t' '\n'] { token lexbuf } | '.' { 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 } diff --git a/main.ml b/main.ml index a1ea649..3a00e01 100644 --- a/main.ml +++ b/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, []), [])] - | Undo -> interactive sq + [Some (rh, ty), (Some (rh, ty, []), [])] |> interactive get_cmd + | 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 - | End_of_file -> + (cg, (g, gs))::sq |> interactive get_cmd + | 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) - else Simple (parse_channel_lam where_from) + then Reduce (Lexing.from_channel where_from |> parse_lam) + 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 () - | Reduce l -> let _ = show_beta_reduction l in () + Simple get_cmd -> + 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" diff --git a/parser.mly b/parser.mly index 9fc9133..0d802ae 100644 --- a/parser.mly +++ b/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 } - | t=tactic EOL { Cmd t } + | e=expression EOF { Lam e } + | ts=nonempty_list(tactic) EOF { Cmd ts } tactic: | c=command DOT { c } diff --git a/parser_entry.ml b/parser_entry.ml index cb89ff5..407bd8c 100644 --- a/parser_entry.ml +++ b/parser_entry.ml @@ -10,4 +10,4 @@ type cmd = type parser_entry = | Lam of lam - | Cmd of cmd + | Cmd of cmd list