nettoyage lexer et parser

parent 71043a58
......@@ -148,6 +148,9 @@ test: bin/why.byte
bin/why.byte --driver lib/drivers/alt_ergo.drv -I lib/prelude/ src/test.why > ergo.why
timeout 3 alt-ergo ergo.why
testl: bin/whyl.byte
ocamlrun -bt bin/whyl.byte src/programs/test.mlw
# programs
##########
......
......@@ -81,17 +81,12 @@
/* Precedences */
%nonassoc prec_recfun
%nonassoc prec_fun
%left LEFTB LEFTBLEFTB
%left prec_simple
%left LEFTB
%left COLON
%left prec_letrec
%left IN
%left prec_no_else
%left ELSE
%right prec_named
......@@ -106,8 +101,6 @@
%left OP2
%left OP3
%right unary_op
%left prec_app
%left prec_ident
%left LEFTSQ
%nonassoc prec_decls
......
(* main module for whyl *)
open Format
let files = ref []
let parse_only = ref false
let type_only = ref false
let debug = ref false
let loadpath = ref []
let () =
Arg.parse
["--parse-only", Arg.Set parse_only, "stops after parsing";
"--type-only", Arg.Set type_only, "stops after type-checking";
"--debug", Arg.Set debug, "sets the debug flag";
"-I", Arg.String (fun s -> loadpath := s :: !loadpath),
"<dir> adds dir to the loadpath";
]
(fun f -> files := f :: !files)
"usage: whyl [options] files..."
let rec report fmt = function
| Lexer.Error e ->
fprintf fmt "lexical error: %a" Lexer.report e;
| Loc.Located (loc, e) ->
fprintf fmt "%a%a" Loc.report_position loc report e
| Parsing.Parse_error ->
fprintf fmt "syntax error"
| Typing.Error e ->
Typing.report fmt e
| e ->
fprintf fmt "anomaly: %s" (Printexc.to_string e)
let type_file file =
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let _ = Pgm_lexer.parse_file lb in
close_in c;
if !parse_only then raise Exit;
()
let handle_file file =
try
(* let env = create_env (Typing.retrieve !loadpath) in *)
type_file file
with Exit ->
()
let () =
try
List.iter handle_file !files
with e when not !debug ->
eprintf "%a@." report e;
exit 1
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
......@@ -85,21 +85,19 @@
%token <string> OP0 OP1 OP2 OP3
%token <Ptree.real_constant> FLOAT
%token <string> STRING
%token ABSURD AMPAMP AND ARROW AS ASSERT AT AXIOM
%token BANG BAR BARBAR BEGIN
%token BIGARROW CHECK CLONE COLON COLONEQUAL COMMA DO
%token DONE DOT ELSE END EOF EQUAL
%token EXCEPTION EXISTS EXPORT FOR FORALL FPI
%token FUN GOAL
%token IF IMPORT IN INCLUDE INDUCTIVE INVARIANT
%token LEFTB LEFTBLEFTB LEFTPAR LEFTSQ LEMMA
%token LET LOGIC LRARROW MATCH
%token NAMESPACE NOT OF OR PARAMETER PROP
%token QUOTE RAISE RAISES READS REC REF RETURNS RIGHTB RIGHTBRIGHTB
%token RIGHTPAR RIGHTSQ
%token SEMICOLON
%token THEN THEORY TRUE TRY TYPE UNDERSCORE
%token UNIT USE VARIANT VOID WHILE WITH WRITES
/* keywords */
%token ABSURD AND AS ASSERT BEGIN CHECK DO DONE ELSE END EXCEPTION FOR
%token FUN IF IN INVARIANT LET MATCH NOT RAISE RAISES READS REC REF
%token RETURNS THEN TRY TYPE VARIANT VOID WHILE WITH WRITES
/* symbols */
%token UNDERSCORE QUOTE COMMA LEFTPAR RIGHTPAR BANG COLON SEMICOLON
%token COLONEQUAL ARROW EQUAL AT DOT LEFTSQ RIGHTSQ LEFTB RIGHTB
%token LEFTBLEFTB RIGHTBRIGHTB BAR BARBAR AMPAMP BIGARROW
%token EOF
/* Precedences */
......@@ -118,13 +116,10 @@
%left prec_no_else
%left ELSE
%right prec_named
%left COLONEQUAL
%right prec_quant
%right ARROW LRARROW
%right OR BARBAR
%right AND AMPAMP
%right NOT
%right BARBAR
%right AMPAMP
%right prec_if
%left EQUAL OP0
%left OP1
......@@ -165,7 +160,7 @@ list1_decl:
decl:
| LIDENT
{ () }
{ LogicDecl [] }
;
/*****
......
type ident = Ptree.ident
type file = unit list
type decl =
| LogicDecl of Ptree.decl list
type file = decl list
(* test file for ML-why *)
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment