X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Ftest_parser.ml;h=31bcdad054e19763f646e09527a5455c63ee80f5;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=4937f4ca41bded6e6d2116da541017df1341a8ee;hpb=b82fbbf4eebebe40f6e4557c191b177a696b0e2c;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index 4937f4ca4..31bcdad05 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -23,51 +23,69 @@ * http://helm.cs.unibo.it/ *) -let default_mode = `Term +open Printf -let mode = ref default_mode +let pp_tactical = TacticAst2Box.tacticalPp -let _ = +let mode = try match Sys.argv.(1) with - | "alias" -> mode := `Alias - | "term" -> mode := `Term - | "tactic" -> mode := `Tactic - | "tactical" -> mode := `Tactical + | "term" -> prerr_endline "Term"; `Term + | "statement" -> prerr_endline "Statement"; `Statement +(* | "script" -> prerr_endline "Script"; `Script *) | _ -> prerr_endline "What???????"; exit 1 - with Invalid_argument _ -> () + with Invalid_argument _ -> prerr_endline "Term"; `Term let _ = - let ic = stdin in - try - while true do - try +(* + if mode = `Script then + let ic = open_in Sys.argv.(2) in + let istream = Stream.of_channel ic in + let (loc, script) = CicTextualParser2.parse_script istream in + List.iter + (function + | DisambiguateTypes.Command cmd -> print_endline (pp_tactical cmd) + | DisambiguateTypes.Comment (loc, s) -> print_endline s) + script + else +*) + let ic = stdin in + try + while true do let line = input_line ic in let istream = Stream.of_string line in - (match !mode with - | `Term -> - let term = CicTextualParser2.parse_term istream in - print_endline (BoxPp.pp_term term) - | `Tactic -> - let term = CicTextualParser2.parse_tactic istream in - print_endline (TacticAstPp.pp_tactic term) - | `Tactical -> - let term = CicTextualParser2.parse_tactical istream in - print_endline (TacticAstPp.pp_tactical term) - | `Alias -> - let env = CicTextualParser2.EnvironmentP3.of_string line in - print_endline (CicTextualParser2.EnvironmentP3.to_string env)); - flush stdout - with - | CicTextualParser2.Parse_error msg -> prerr_endline msg + try + (match mode with + | `Term -> + let term = CicTextualParser2.parse_term istream in + print_endline (BoxPp.pp_term term) + | `Statement -> + (match CicTextualParser2.parse_statement istream with + | TacticAst.Command (_, cmd) -> + print_endline (TacticAstPp.pp_command cmd) + | TacticAst.Tactical (_, tac) -> + print_endline (TacticAstPp.pp_tactical tac)) (* - | Stdpp.Exc_located ((p_start, p_end), exn) -> - prerr_endline (Printf.sprintf "Exception at character %d-%d: %s" - p_start p_end (Printexc.to_string exn)) + | `Tactical -> + let tac = CicTextualParser2.parse_tactical istream in + print_endline (pp_tactical tac) *) - done - with End_of_file -> - close_in ic + | `Alias -> + let env = CicTextualParser2.EnvironmentP3.of_string line in + print_endline (CicTextualParser2.EnvironmentP3.to_string env) + | _ -> assert false); + flush stdout + with + | CicTextualParser2.Parse_error (floc, msg) -> + let (x, y) = CicAst.loc_of_floc floc in + let before = String.sub line 0 x in + let error = String.sub line x (y - x) in + let after = String.sub line y (String.length line - y) in + eprintf "%s%s%s\n" before error after; + prerr_endline (sprintf "at character %d-%d: %s" x y msg) + done + with End_of_file -> + close_in ic