diff --git a/compiler/global/location.ml b/compiler/global/location.ml index e694276..4c5ca03 100644 --- a/compiler/global/location.ml +++ b/compiler/global/location.ml @@ -1,154 +1,128 @@ (* Printing a location in the source program *) -(* taken from the source of the Caml Light 0.73 compiler *) +(* inspired from the source of the Caml Light 0.73 compiler *) open Lexing open Parsing (* two important global variables: [input_name] and [input_chan] *) type location = - Loc of int (* Position of the first character *) - * int (* Position of the next character following the last one *) + Loc of position (* Position of the first character *) + * position (* Position of the next character following the last one *) let input_name = ref "" (* Input file name. *) -let input_chan = ref stdin (* The channel opened on the input. *) +let input_chan = ref stdin (* The channel opened on the input. *) let initialize iname ic = input_name := iname; input_chan := ic -let no_location = Loc(0,0) - +let no_location = Loc (dummy_pos, dummy_pos) let error_prompt = ">" -let current_loc () = - Loc(symbol_start(), symbol_end()) +(** Prints [n] times char [c] on [oc]. *) +let prints_n_chars oc n c = for i = 1 to n do output_char oc c done -let output_lines oc char1 char2 charline1 line1 line2 = - let n1 = char1 - charline1 - and n2 = char2 - charline1 in - if line2 > line1 then - Printf.fprintf oc - ", line %d-%d, characters %d-%d:\n" line1 line2 n1 n2 - else - Printf.fprintf oc ", line %d, characters %d-%d:\n" line1 n1 n2; - () - - -let output_loc oc input seek line_flag (Loc(pos1, pos2)) = - let pr_chars n c = - for i = 1 to n do output_char oc c done in - let skip_line () = - try - while input() != '\n' do () done - with End_of_file -> () in - let copy_line () = - let c = ref ' ' in - begin try - while c := input(); !c != '\n' do output_char oc !c done - with End_of_file -> - output_string oc "" - end; - output_char oc '\n' in - let pr_line first len ch = - let c = ref ' ' - and f = ref first - and l = ref len in - try - while c := input (); !c != '\n' do - if !f > 0 then begin - f := !f - 1; - output_char oc (if !c == '\t' then !c else ' ') - end - else if !l > 0 then begin - l := !l - 1; - output_char oc (if !c == '\t' then !c else ch) - end - else () - done - with End_of_file -> - if !f = 0 && !l > 0 then pr_chars 5 ch in - let pos = ref 0 - and line1 = ref 1 - and line1_pos = ref 0 - and line2 = ref 1 - and line2_pos = ref 0 in - seek 0; - begin try - while !pos < pos1 do - incr pos; - if input() == '\n' then begin incr line1; line1_pos := !pos; () end +(** Prints out to [oc] a line designed to be printed under [line] from file [ic] + underlining from char [first] to char [last] with char [ch]. + [line] is the index of the first char of line. *) +let underline_line ic oc ch line first last = + let c = ref ' ' + and f = ref first + and l = ref (last-first) in + ( try + seek_in ic line; + output_string oc error_prompt; + while c := input_char ic; !c != '\n' do + if !f > 0 then begin + f := !f - 1; + output_char oc (if !c == '\t' then !c else ' ') + end + else if !l > 0 then begin + l := !l - 1; + output_char oc (if !c == '\t' then !c else ch) + end + else () done - with End_of_file -> () - end; - line2 := !line1; - line2_pos := !line1_pos; - begin try - while !pos < pos2 do - incr pos; - if input() == '\n' then - begin incr line2; line2_pos := !pos; () end + with End_of_file -> + if !f = 0 && !l > 0 then prints_n_chars oc 5 ch ) + + +let copy_lines nl ic oc prompt = + for i = 1 to nl do + output_string oc prompt; + (try output_string oc (input_line ic) + with End_of_file -> output_string oc ""); + output_char oc '\n' + done + +let copy_chunk p1 p2 ic oc = + try for i = p1 to p2 - 1 do output_char oc (input_char ic) done + with End_of_file -> output_string oc "" + + + +let skip_lines n ic = + try for i = 1 to n do + let _ = input_line ic in () done with End_of_file -> () - end; - if line_flag then output_lines oc pos1 pos2 !line1_pos !line1 !line2; - if !line1 == !line2 then begin - seek !line1_pos; - output_string oc error_prompt; - copy_line (); - seek !line1_pos; - output_string oc error_prompt; - pr_line (pos1 - !line1_pos) (pos2 - pos1) '^'; - output_char oc '\n' - end else begin - seek !line1_pos; - output_string oc error_prompt; - pr_line 0 (pos1 - !line1_pos) '.'; - seek pos1; - copy_line(); - if !line2 - !line1 <= 8 then - for i = !line1 + 1 to !line2 - 1 do - output_string oc error_prompt; - copy_line() - done - else - begin - for i = !line1 + 1 to !line1 + 3 do - output_string oc error_prompt; - copy_line() - done; - output_string oc error_prompt; output_string oc "..........\n"; - for i = !line1 + 4 to !line2 - 4 do skip_line() done; - for i = !line2 - 3 to !line2 - 1 do - output_string oc error_prompt; - copy_line() - done - end; - begin try - output_string oc error_prompt; - for i = !line2_pos to pos2 - 1 do - output_char oc (input()) - done; - pr_line 0 100 '.' - with End_of_file -> output_string oc "" - end; - output_char oc '\n' - end -let output_location oc loc = - let p = pos_in !input_chan in - Printf.fprintf oc "File \"%s\"" !input_name; - output_loc - oc (fun () -> input_char !input_chan) (seek_in !input_chan) true - loc; - seek_in !input_chan p +let output_location oc (Loc(p1,p2)) = + let n1 = p1.pos_cnum - p1.pos_bol in (* character number *) + let n2 = p2.pos_cnum - p2.pos_bol in + let np1 = p1.pos_cnum in (* character position *) + let np2 = p2.pos_cnum in + let l1 = p1.pos_lnum in (* line number *) + let l2 = p2.pos_lnum in + let lp1 = p1.pos_bol in (* line position *) + let lp2 = p2.pos_bol in + let f1 = p1.pos_fname in (* file name *) + let f2 = p2.pos_fname in + + if f1 != f2 then (* Strange case *) + Printf.fprintf oc + "File \"%s\" line %d, character %d, to file \"%s\" line %d, character %d\n" + f1 l1 n1 f2 l2 n2 -let output_input_name oc = - Printf.fprintf oc "File \"%s\", line 1:\n" !input_name + else begin + if l2 > l1 then + Printf.fprintf oc + "File \"%s\", line %d-%d, characters %d-%d:\n" f1 l1 l2 n1 n2 + else + Printf.fprintf oc "File \"%s\", line %d, characters %d-%d:\n" f1 l1 n1 n2; + (* Output source code *) + let ic = open_in f1 in + + if l1 == l2 then ( + (* Only one line : copy full line and underline *) + seek_in ic lp1; + copy_lines 1 ic oc ">"; + underline_line ic oc '^' lp1 n1 n2 ) + else ( + underline_line ic oc '.' lp1 0 n1; (* dots until n1 *) + seek_in ic np1; + (* copy the end of the line l1 after the dots *) + copy_lines 1 ic oc ""; + if l2 - l1 <= 8 then + (* copy the 6 or less middle lines *) + copy_lines (l2-l1-1) ic oc ">" + else ( + (* sum up the middle lines to 6 *) + copy_lines 3 ic oc ">"; + output_string oc "..........\n"; + skip_lines (l2-l1-7) ic; (* skip middle lines *) + copy_lines 3 ic oc ">" + ); + output_string oc ">"; + copy_chunk lp2 np2 ic oc; (* copy interesting begining of l2 *) + ); + output_char oc '\n' + end; diff --git a/compiler/heptagon/analysis/causal.ml b/compiler/heptagon/analysis/causal.ml index cfe06c6..bae3fc8 100644 --- a/compiler/heptagon/analysis/causal.ml +++ b/compiler/heptagon/analysis/causal.ml @@ -55,7 +55,7 @@ and nc = | Aac of ac | Aempty -let output_ac ff ac = +let output_ac ff ac = (*TODO LG fix breaks*) let rec print priority ff ac = fprintf ff "@["; begin match ac with diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index 2167516..3df36a0 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/compiler/heptagon/main/hept_compiler.ml @@ -18,11 +18,11 @@ let parse parsing_fun lexing_fun lexbuf = try parsing_fun lexing_fun lexbuf with - | Hept_lexer.Lexical_error(err, pos1, pos2) -> - lexical_error err (Loc(pos1, pos2)) + | Hept_lexer.Lexical_error(err, l) -> + lexical_error err l | Hept_parser.Error -> - let pos1 = Lexing.lexeme_start lexbuf - and pos2 = Lexing.lexeme_end lexbuf in + let pos1 = Lexing.lexeme_start_p lexbuf + and pos2 = Lexing.lexeme_end_p lexbuf in let l = Loc(pos1,pos2) in syntax_error l @@ -76,17 +76,16 @@ let compile_interface modname filename = let source_name = filename ^ ".epi" in let obj_interf_name = filename ^ ".epci" in - let ic = open_in source_name in + let ic, lexbuf = lexbuf_from_file source_name in let itc = open_out_bin obj_interf_name in let close_all_files () = close_in ic; close_out itc in try - init_compiler modname source_name ic; + init_compiler modname; (* Parsing of the file *) - let lexbuf = Lexing.from_channel ic in let l = parse_interface lexbuf in (* Convert the parse tree to Heptagon AST *) diff --git a/compiler/heptagon/main/heptcheck.ml b/compiler/heptagon/main/heptcheck.ml index 8517cf2..5a649db 100644 --- a/compiler/heptagon/main/heptcheck.ml +++ b/compiler/heptagon/main/heptcheck.ml @@ -19,16 +19,15 @@ let check_implementation modname filename = (* input and output files *) let source_name = filename ^ ".ept" in - let ic = open_in source_name in + let ic, lexbuf = lexbuf_from_file source_name in let close_all_files () = close_in ic in try - init_compiler modname source_name ic; + init_compiler modname; (* Parsing of the file *) - let lexbuf = Lexing.from_channel ic in let p = parse_implementation lexbuf in (* Convert the parse tree to Heptagon AST *) diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index fd34c89..9f78891 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -3,15 +3,17 @@ { open Lexing +open Location open Hept_parser + type lexical_error = Illegal_character | Unterminated_comment | Bad_char_constant | Unterminated_string;; -exception Lexical_error of lexical_error * int * int;; +exception Lexical_error of lexical_error * location;; let comment_depth = ref 0 @@ -80,14 +82,6 @@ let reset_string_buffer () = string_index := 0; () -(* -let incr_linenum lexbuf = - let pos = lexbuf.Lexing.lex_curr_p in - lexbuf.Lexing.lex_curr_p <- { pos with - Lexing.pos_lnum = pos.Lexing.pos_lnum + 1; - Lexing.pos_bol = pos.Lexing.pos_cnum; - } -*) let store_string_char c = if !string_index >= String.length (!string_buff) then begin @@ -118,11 +112,14 @@ let char_for_decimal_code lexbuf i = (int_of_char(Lexing.lexeme_char lexbuf (i+2)) - 48) in char_of_int(c land 0xFF) - } + +let newline = '\n' | '\r' '\n' + rule token = parse - | [' ' '\010' '\013' '\009' '\012'] + { token lexbuf } + | newline { new_line lexbuf; token lexbuf } + | [' ' '\t'] + { token lexbuf } | "." {DOT} | "(" {LPAREN} | ")" {RPAREN} @@ -168,23 +165,22 @@ rule token = parse | "(*@ " (['A'-'Z' 'a'-'z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id) { reset_string_buffer(); - let pragma_start = lexbuf.lex_start_pos + lexbuf.lex_abs_pos in + let l1 = lexbuf.lex_curr_p in begin try pragma lexbuf - with Lexical_error(Unterminated_comment, _, pragma_end) -> - raise(Lexical_error(Unterminated_comment, pragma_start, pragma_end)) + with Lexical_error(Unterminated_comment, Loc(_, l2)) -> + raise(Lexical_error(Unterminated_comment, Loc (l1, l2))) end; - lexbuf.lex_start_pos <- pragma_start - lexbuf.lex_abs_pos; PRAGMA(id,get_stored_string()) } | "(*" - { let comment_start = lexbuf.lex_start_pos + lexbuf.lex_abs_pos in + { let comment_start = lexbuf.lex_curr_p in comment_depth := 1; begin try comment lexbuf - with Lexical_error(Unterminated_comment, _, comment_end) -> + with Lexical_error(Unterminated_comment, (Loc (_, comment_end))) -> raise(Lexical_error(Unterminated_comment, - comment_start, comment_end)) + Loc (comment_start, comment_end))) end; token lexbuf } | ['!' '?' '~'] @@ -213,43 +209,46 @@ rule token = parse { INFIX3(Lexing.lexeme lexbuf) } | eof {EOF} | _ {raise (Lexical_error (Illegal_character, - Lexing.lexeme_start lexbuf, - Lexing.lexeme_end lexbuf))} + Loc (Lexing.lexeme_start_p lexbuf, + Lexing.lexeme_end_p lexbuf)))} and pragma = parse - "(*" - { let comment_start = lexbuf.lex_start_pos + lexbuf.lex_abs_pos in + | newline { new_line lexbuf; pragma lexbuf } + | "(*" + { let comment_start = lexbuf.lex_curr_p in comment_depth := 1; begin try comment lexbuf - with Lexical_error(Unterminated_comment, _, comment_end) -> + with Lexical_error(Unterminated_comment, Loc (_, comment_end)) -> raise(Lexical_error(Unterminated_comment, - comment_start, comment_end)) + Loc (comment_start, comment_end))) end; pragma lexbuf } | "@*)" { } | eof - { raise(Lexical_error(Unterminated_comment,0, - Lexing.lexeme_start lexbuf)) } + { raise(Lexical_error(Unterminated_comment, Loc (dummy_pos, + Lexing.lexeme_start_p lexbuf))) } | _ { store_string_char(Lexing.lexeme_char lexbuf 0); pragma lexbuf } and comment = parse - "(*" + | newline { new_line lexbuf; comment lexbuf } + | "(*" { comment_depth := succ !comment_depth; comment lexbuf } | "*)" { comment_depth := pred !comment_depth; if !comment_depth > 0 then comment lexbuf } | "\"" { reset_string_buffer(); - let string_start = lexbuf.lex_start_pos + lexbuf.lex_abs_pos in + let string_start = lexbuf.lex_curr_p in begin try string lexbuf - with Lexical_error(Unterminated_string, _, string_end) -> - raise(Lexical_error(Unterminated_string, string_start, string_end)) + with Lexical_error(Unterminated_string, Loc (_, string_end)) -> + raise(Lexical_error + (Unterminated_string, Loc (string_start, string_end))) end; comment lexbuf } | "''" @@ -261,13 +260,14 @@ and comment = parse | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'" { comment lexbuf } | eof - { raise(Lexical_error(Unterminated_comment,0, - Lexing.lexeme_start lexbuf)) } + { raise(Lexical_error(Unterminated_comment, Loc(dummy_pos, + Lexing.lexeme_start_p lexbuf))) } | _ { comment lexbuf } and string = parse - '"' + | newline { new_line lexbuf; string lexbuf } + | '"' { () } | '\\' ("\010" | "\013" | "\013\010") [' ' '\009'] * { string lexbuf } @@ -278,8 +278,8 @@ and string = parse { store_string_char(char_for_decimal_code lexbuf 1); string lexbuf } | eof - { raise (Lexical_error - (Unterminated_string, 0, Lexing.lexeme_start lexbuf)) } + { raise (Lexical_error(Unterminated_string, Loc (dummy_pos, + Lexing.lexeme_start_p lexbuf))) } | _ { store_string_char(Lexing.lexeme_char lexbuf 0); string lexbuf } diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index f10c86f..506209e 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -6,7 +6,6 @@ open Names open Types open Hept_parsetree -let mk_static_exp = mk_static_exp ~loc:(current_loc()) %} @@ -111,7 +110,7 @@ const_decs: const_dec: | CONST IDENT COLON ty_ident EQUAL exp - { mk_const_dec $2 $4 $6 } + { mk_const_dec $2 $4 $6 (Loc($startpos,$endpos)) } ; type_decs: @@ -120,9 +119,12 @@ type_decs: ; type_dec: - | TYPE IDENT { mk_type_dec $2 Type_abs } - | TYPE IDENT EQUAL enum_ty_desc { mk_type_dec $2 (Type_enum ($4)) } - | TYPE IDENT EQUAL struct_ty_desc { mk_type_dec $2 (Type_struct ($4)) } + | TYPE IDENT + { mk_type_dec $2 Type_abs (Loc($startpos,$endpos)) } + | TYPE IDENT EQUAL enum_ty_desc + { mk_type_dec $2 (Type_enum ($4)) (Loc($startpos,$endpos)) } + | TYPE IDENT EQUAL struct_ty_desc + { mk_type_dec $2 (Type_struct ($4)) (Loc($startpos,$endpos)) } ; enum_ty_desc: @@ -153,15 +155,15 @@ node_decs: node_dec: | node_or_fun ident node_params LPAREN in_params RPAREN RETURNS LPAREN out_params RPAREN - contract loc_vars LET equs TEL + contract b=block(LET) TEL {{ n_name = $2; n_statefull = $1; n_input = $5; n_output = $9; n_contract = $11; - n_block = mk_block $12 $14; + n_block = b; n_params = $3; - n_loc = Location.current_loc () }} + n_loc = (Loc($startpos,$endpos)) }} ; node_or_fun: @@ -185,7 +187,7 @@ nonmt_params: param: | ident_list COLON ty_ident - { List.map (fun id -> mk_var_dec id $3 Var) $1 } + { List.map (fun id -> mk_var_dec id $3 Var (Loc($startpos,$endpos))) $1 } ; out_params: @@ -205,19 +207,14 @@ node_params: contract: | /* empty */ {None} - | CONTRACT loc_vars opt_equs opt_assume enforce - { Some{ c_block = mk_block $2 $3; + | CONTRACT b=block(LET) TEL? opt_assume enforce + { Some{ c_block = b; c_assume = $4; c_enforce = $5 } } ; -opt_equs: - | /* empty */ { [] } - | LET equs TEL { $2 } -; - opt_assume: - | /* empty */ { mk_exp (Econst (mk_static_exp (Sconstructor Initial.ptrue))) } + | /* empty */ { mk_constructor_exp Initial.ptrue (Loc($startpos,$endpos)) } | ASSUME exp { $2 } ; @@ -235,13 +232,14 @@ loc_params: | var_last SEMICOL loc_params { $1 @ $3 } ; + var_last: | ident_list COLON ty_ident - { List.map (fun id -> mk_var_dec id $3 Var) $1 } + { List.map (fun id -> mk_var_dec id $3 Var (Loc($startpos,$endpos))) $1 } | LAST IDENT COLON ty_ident EQUAL exp - { [ mk_var_dec $2 $4 (Last(Some($6))) ] } + { [ mk_var_dec $2 $4 (Last(Some($6))) (Loc($startpos,$endpos)) ] } | LAST IDENT COLON ty_ident - { [ mk_var_dec $2 $4 (Last(None)) ] } + { [ mk_var_dec $2 $4 (Last(None)) (Loc($startpos,$endpos)) ] } ; ident_list: @@ -276,28 +274,32 @@ opt_bar: | BAR {} ; -equ: - | pat EQUAL exp { mk_equation (Eeq($1, $3)) } +block(S): + | l=loc_vars S eq=equs { mk_block l eq (Loc($startpos,$endpos)) } + | l=loc_vars { mk_block l [] (Loc($startpos,$endpos)) } + +equ: eq=_equ { mk_equation eq (Loc($startpos,$endpos)) } +_equ: + | pat EQUAL exp { Eeq($1, $3) } | AUTOMATON automaton_handlers END - { mk_equation (Eautomaton(List.rev $2)) } + { Eautomaton(List.rev $2) } | SWITCH exp opt_bar switch_handlers END - { mk_equation (Eswitch($2, List.rev $4)) } + { Eswitch($2, List.rev $4) } | PRESENT opt_bar present_handlers END - { mk_equation (Epresent(List.rev $3, mk_block [] [])) } - | PRESENT opt_bar present_handlers DEFAULT loc_vars DO equs END - { mk_equation (Epresent(List.rev $3, mk_block $5 $7)) } - | IF exp THEN loc_vars DO equs ELSE loc_vars DO equs END - { mk_equation (Eswitch($2, - [{ w_name = Name("true"); w_block = mk_block $4 $6}; - { w_name = Name("false"); w_block = mk_block $8 $10 }])) } + { Epresent(List.rev $3, mk_block [] [] (Loc($startpos,$endpos))) } + | PRESENT opt_bar present_handlers DEFAULT b=block(DO) END + { Epresent(List.rev $3, b) } + | IF exp THEN tb=block(DO) ELSE fb=block(DO) END + { Eswitch($2, + [{ w_name = Name("true"); w_block = tb }; + { w_name = Name("false"); w_block = fb }]) } | RESET equs EVERY exp - { mk_equation (Ereset($2, $4)) } + { Ereset($2, $4) } ; automaton_handler: - | STATE Constructor loc_vars DO equs opt_until_escapes opt_unless_escapes - { { s_state = $2; s_block = mk_block $3 $5; - s_until = $6; s_unless = $7 } } + | STATE Constructor b=block(DO) ut=opt_until_escapes ul=opt_unless_escapes + { { s_state = $2; s_block = b; s_until = ut; s_unless = ul } } ; automaton_handlers: @@ -334,8 +336,8 @@ escapes: ; switch_handler: - | constructor_or_bool loc_vars DO equs - { { w_name = $1; w_block = mk_block $2 $4 } } + | constructor_or_bool b=block(DO) + { { w_name = $1; w_block = b } } ; constructor_or_bool: @@ -350,8 +352,8 @@ switch_handlers: ; present_handler: - | exp loc_vars DO equs - { { p_cond = $1; p_block = mk_block $2 $4 } } + | exp b=block(DO) + { { p_cond = $1; p_block = b } } ; present_handlers: @@ -381,88 +383,88 @@ exps: | nonmtexps {$1} ; -simple_exp: - | IDENT { mk_exp (Evar $1) } - | const { mk_exp (Econst $1) } - | LBRACE field_exp_list RBRACE - { mk_exp (Estruct $2) } - | LBRACKET array_exp_list RBRACKET - { mk_exp (mk_call Earray $2) } - | LPAREN tuple_exp RPAREN - { mk_exp (mk_call Etuple $2) } - | LPAREN exp RPAREN - { $2 } +simple_exp: e=_simple_exp { mk_exp e (Loc($startpos,$endpos)) } +_simple_exp: + | IDENT { Evar $1 } + | const { Econst $1 } + | LBRACE field_exp_list RBRACE { Estruct $2 } + | LBRACKET array_exp_list RBRACKET { mk_call Earray $2 } + | LPAREN tuple_exp RPAREN { mk_call Etuple $2 } + | LPAREN _exp RPAREN { $2 } ; node_name: - | longname call_params - { mk_app (Enode $1) $2 } + | longname call_params { mk_app (Enode $1) $2 } + exp: - | simple_exp { $1 } + | e=simple_exp { e } + | e=_exp { mk_exp e (Loc($startpos,$endpos)) } +_exp: | simple_exp FBY exp - { mk_exp (Efby ($1, $3)) } + { Efby ($1, $3) } | PRE exp - { mk_exp (Epre (None, $2)) } + { Epre (None, $2) } | node_name LPAREN exps RPAREN - { mk_exp (Eapp($1, $3)) } + { Eapp($1, $3) } | NOT exp - { mk_exp (mk_op_call "not" [$2]) } + { mk_op_call "not" [$2] } | exp INFIX4 exp - { mk_exp (mk_op_call $2 [$1; $3]) } + { mk_op_call $2 [$1; $3] } | exp INFIX3 exp - { mk_exp (mk_op_call $2 [$1; $3]) } + { mk_op_call $2 [$1; $3] } | exp INFIX2 exp - { mk_exp (mk_op_call $2 [$1; $3]) } + { mk_op_call $2 [$1; $3] } | exp INFIX1 exp - { mk_exp (mk_op_call $2 [$1; $3]) } + { mk_op_call $2 [$1; $3] } | exp INFIX0 exp - { mk_exp (mk_op_call $2 [$1; $3]) } + { mk_op_call $2 [$1; $3] } | exp EQUAL exp - { mk_exp (mk_op_call "=" [$1; $3]) } + { mk_op_call "=" [$1; $3] } | exp OR exp - { mk_exp (mk_op_call "or" [$1; $3]) } + { mk_op_call "or" [$1; $3] } | exp STAR exp - { mk_exp (mk_op_call "*" [$1; $3]) } + { mk_op_call "*" [$1; $3] } | exp AMPERSAND exp - { mk_exp (mk_op_call "&" [$1; $3]) } + { mk_op_call "&" [$1; $3] } | exp SUBTRACTIVE exp - { mk_exp (mk_op_call $2 [$1; $3]) } + { mk_op_call $2 [$1; $3] } | PREFIX exp - { mk_exp (mk_op_call $1 [$2]) } + { mk_op_call $1 [$2] } | SUBTRACTIVE exp %prec prec_uminus - { mk_exp (mk_op_call ("~"^$1) [$2]) } + { mk_op_call ("~"^$1) [$2] } | IF exp THEN exp ELSE exp - { mk_exp (mk_call Eifthenelse [$2; $4; $6]) } + { mk_call Eifthenelse [$2; $4; $6] } | simple_exp ARROW exp - { mk_exp (mk_call Earrow [$1; $3]) } + { mk_call Earrow [$1; $3] } | LAST IDENT - { mk_exp (Elast $2) } + { Elast $2 } /*Array operations*/ | exp POWER simple_exp - { mk_exp (mk_call ~params:[$3] Earray_fill [$1]) } + { mk_call ~params:[$3] Earray_fill [$1] } | simple_exp indexes - { mk_exp (mk_call ~params:$2 Eselect [$1]) } + { mk_call ~params:$2 Eselect [$1] } | simple_exp DOT indexes DEFAULT exp - { mk_exp (mk_call Eselect_dyn ([$1; $5]@$3)) } + { mk_call Eselect_dyn ([$1; $5]@$3) } | LBRACKET exp WITH indexes EQUAL exp RBRACKET - { mk_exp (mk_call ~params:$4 Eupdate [$2; $6]) } + { mk_call ~params:$4 Eupdate [$2; $6] } | simple_exp LBRACKET exp DOUBLE_DOT exp RBRACKET - { mk_exp (mk_call ~params:[$3; $5] Eselect_slice [$1]) } + { mk_call ~params:[$3; $5] Eselect_slice [$1] } | exp AROBASE exp - { mk_exp (mk_call Econcat [$1; $3]) } + { mk_call Econcat [$1; $3] } /*Iterators*/ | iterator longname DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN - { mk_exp (mk_iterator_call $1 $2 [] $4 $7) } + { mk_iterator_call $1 $2 [] $4 $7 } | iterator LPAREN longname DOUBLE_LESS array_exp_list DOUBLE_GREATER RPAREN DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN - { mk_exp (mk_iterator_call $1 $3 $5 $9 $12) } + { mk_iterator_call $1 $3 $5 $9 $12 } /*Records operators */ - | simple_exp DOT longname - { mk_exp (mk_call ~params:[mk_constructor_exp $3] Efield [$1]) } - | LBRACE simple_exp WITH DOT longname EQUAL exp RBRACE - { mk_exp (mk_call ~params:[mk_constructor_exp $5] - Efield_update [$2; $7]) } + | simple_exp DOT c=longname + { mk_call ~params:[mk_constructor_exp c (Loc($startpos(c),$endpos(c)))] + Efield [$1] } + | LBRACE simple_exp WITH DOT c=longname EQUAL exp RBRACE + { mk_call ~params:[mk_constructor_exp c (Loc($startpos(c),$endpos(c)))] + Efield_update [$2; $7] } ; call_params: @@ -491,11 +493,13 @@ longname: | Constructor DOT ident { Modname({qual = $1; id = $3}) } ; -const: - | INT { mk_static_exp (Sint $1) } - | FLOAT { mk_static_exp (Sfloat $1) } - | BOOL { mk_static_exp (Sbool $1) } - | constructor { mk_static_exp (Sconstructor $1) } + +const: c=_const { mk_static_exp c ~loc:(Loc($startpos,$endpos)) } +_const: + | INT { Sint $1 } + | FLOAT { Sfloat $1 } + | BOOL { Sbool $1 } + | constructor { Sconstructor $1 } ; tuple_exp: @@ -548,16 +552,18 @@ interface_decls: ; interface_decl: - | type_dec { mk_interface_decl (Itypedef $1) } - | const_dec { mk_interface_decl (Iconstdef $1) } - | OPEN Constructor { mk_interface_decl (Iopen $2) } + | id=_interface_decl { mk_interface_decl id (Loc($startpos,$endpos)) } +_interface_decl: + | type_dec { Itypedef $1 } + | const_dec { Iconstdef $1 } + | OPEN Constructor { Iopen $2 } | VAL node_or_fun ident node_params LPAREN params_signature RPAREN RETURNS LPAREN params_signature RPAREN - { mk_interface_decl (Isignature({ sig_name = $3; + { Isignature({ sig_name = $3; sig_inputs = $6; sig_statefull = $2; sig_outputs = $10; - sig_params = $4; })) } + sig_params = $4; }) } ; params_signature: diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 176f938..58313c7 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -164,8 +164,8 @@ and interface_desc = | Isignature of signature (* Helper functions to create AST. *) -let mk_exp desc = - { e_desc = desc; e_loc = Location.current_loc () } +let mk_exp desc loc = + { e_desc = desc; e_loc = loc } let mk_app op params = { a_op = op; a_params = params } @@ -180,29 +180,29 @@ let mk_op_call ?(params=[]) s exps = let mk_iterator_call it ln params n exps = Eiterator (it, mk_app (Enode ln) params, n, exps) -let mk_constructor_exp f = - mk_exp (Econst (mk_static_exp (Sconstructor f))) +let mk_constructor_exp f loc = + mk_exp (Econst (mk_static_exp (Sconstructor f))) loc -let mk_type_dec name desc = - { t_name = name; t_desc = desc; t_loc = Location.current_loc () } +let mk_type_dec name desc loc = + { t_name = name; t_desc = desc; t_loc = loc } -let mk_equation desc = - { eq_desc = desc; eq_loc = Location.current_loc () } +let mk_equation desc loc = + { eq_desc = desc; eq_loc = loc } -let mk_interface_decl desc = - { interf_desc = desc; interf_loc = Location.current_loc () } +let mk_interface_decl desc loc = + { interf_desc = desc; interf_loc = loc } -let mk_var_dec name ty last = +let mk_var_dec name ty last loc = { v_name = name; v_type = ty; - v_last = last; v_loc = Location.current_loc () } + v_last = last; v_loc = loc } -let mk_block locals eqs = +let mk_block locals eqs loc = { b_local = locals; b_equs = eqs; - b_loc = Location.current_loc () } + b_loc = loc } -let mk_const_dec id ty e = +let mk_const_dec id ty e loc = { c_name = id; c_type = ty; c_value = e; - c_loc = Location.current_loc (); } + c_loc = loc } let mk_arg name ty = { a_type = ty; a_name = name } diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index 77c65a6..6cfbf12 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -21,7 +21,7 @@ let compile_impl modname filename = and obj_interf_name = filename ^ ".epci" and mls_name = filename ^ ".mls" in - let ic = open_in source_name + let ic, lexbuf = lexbuf_from_file source_name and itc = open_out_bin obj_interf_name and mlsc = open_out mls_name in @@ -31,10 +31,9 @@ let compile_impl modname filename = close_out mlsc in try - init_compiler modname source_name ic; + init_compiler modname; (* Parsing of the file *) - let lexbuf = Lexing.from_channel ic in let p = parse_implementation lexbuf in let p = { p with Hept_parsetree.p_modname = modname } in diff --git a/compiler/minils/main/mlsc.ml b/compiler/minils/main/mlsc.ml index aeeecd5..808a0a4 100644 --- a/compiler/minils/main/mlsc.ml +++ b/compiler/minils/main/mlsc.ml @@ -38,7 +38,7 @@ let compile_impl modname filename = and mls_norm_name = filename ^ "_norm.mls" and obc_name = filename ^ ".obc" in - let ic = open_in source_name + let ic, lexbuf = lexbuf_from_file source_name in and mlsnc = open_out mls_norm_name and obc = open_out obc_name in @@ -49,10 +49,9 @@ let compile_impl modname filename = in try - init_compiler modname source_name ic; + init_compiler modname; (* Parsing of the file *) - let lexbuf = Lexing.from_channel ic in let p = parse_implementation lexbuf in if !verbose then begin diff --git a/compiler/minils/parsing/mls_parser.mly b/compiler/minils/parsing/mls_parser.mly index be107df..cd66629 100644 --- a/compiler/minils/parsing/mls_parser.mly +++ b/compiler/minils/parsing/mls_parser.mly @@ -8,12 +8,6 @@ open Location open Minils open Mls_utils -let mk_exp = mk_exp ~loc:(current_loc()) -let mk_node = mk_node ~loc:(current_loc()) -let mk_equation p e = mk_equation ~loc:(current_loc()) p e -let mk_type name desc = mk_type_dec ~loc:(current_loc()) ~type_desc: desc name -let mk_var name ty = mk_var_dec name ty - %} @@ -84,6 +78,8 @@ qualified(x) : | m=CONSTRUCTOR DOT n=x { Modname({ qual = m; id = n }) } structure(field): LBRACE s=snlist(SEMICOL,field) RBRACE {s} + +localize(x): y=x { y, (Loc($startpos(y),$endpos(y))) } program: @@ -108,15 +104,19 @@ type_ident: NAME { Tid(Name($1)) } type_decs: t=list(type_dec) {t} type_dec: - | TYPE n=NAME { mk_type n Type_abs } - | TYPE n=NAME EQUAL e=snlist(BAR,NAME) { mk_type n (Type_enum e) } - | TYPE n=NAME EQUAL s=structure(field_type) { mk_type n (Type_struct s) } + | TYPE n=NAME + { mk_type_dec ~loc:(Loc ($startpos,$endpos)) ~type_desc:Type_abs n } + | TYPE n=NAME EQUAL e=snlist(BAR,NAME) + { mk_type_dec ~loc:(Loc ($startpos,$endpos)) ~type_desc:(Type_enum e) n } + | TYPE n=NAME EQUAL s=structure(field_type) + { mk_type_dec ~loc:(Loc ($startpos,$endpos)) ~type_desc:(Type_struct s) n } node_decs: ns=list(node_dec) {ns} node_dec: NODE n=name p=params(n_param) LPAREN args=args RPAREN RETURNS LPAREN out=args RPAREN vars=loc_vars eqs=equs - { mk_node ~input:args ~output:out ~local:vars ~eq:eqs n } + { mk_node ~input:args ~output:out ~local:vars + ~eq:eqs ~loc:(Loc ($startpos,$endpos)) n } args_t: SEMICOL p=args {p} @@ -130,10 +130,10 @@ loc_vars: l=loption(loc_vars_h) {l} var: | ns=snlist(COMMA, NAME) COLON t=type_ident - { List.map (fun id -> mk_var (ident_of_name id) t) ns } + { List.map (fun id -> mk_var_dec (ident_of_name id) t) ns } equs: LET e=slist(SEMICOL, equ) TEL { e } -equ: p=pat EQUAL e=exp { mk_equation p e } +equ: p=pat EQUAL e=exp { mk_equation ~loc:(Loc ($startpos,$endpos)) p e } pat: | n=NAME {Evarpat (ident_of_name n)} @@ -155,30 +155,36 @@ exps: LPAREN e=slist(COMMA, exp) RPAREN {e} field_exp: longname EQUAL exp { ($1, $3) } simple_exp: - | NAME { mk_exp (Evar (ident_of_name $1)) } - | s=structure(field_exp) { mk_exp (Estruct s) } - | t=tuple(exp) { mk_exp (Etuple t) } - | LPAREN e=exp RPAREN { e } + | e=_simple_exp {mk_exp e ~loc:(Loc ($startpos,$endpos)) } +_simple_exp: + | NAME { Evar (ident_of_name $1) } + | s=structure(field_exp) { Estruct s } + | t=tuple(exp) { Eapp(mk_op ~op_kind:Etuple, t, None) } + | LPAREN e=_exp RPAREN { e } + exp: + | e=simple_exp { e } + | e=_exp { mk_exp e ~loc:(Loc ($startpos,$endpos)) } +_exp: | e=simple_exp { e } - | c=const { mk_exp (Econst c) } - | const FBY exp { mk_exp (Efby(Some($1),$3)) } - | PRE exp { mk_exp (Efby(None,$2)) } - | op=funop a=exps r=reset { mk_exp (Ecall(op, a, r)) } + | c=const { Econst c } + | const FBY exp { Efby(Some($1),$3) } + | PRE exp { Efby(None,$2) } + | op=funop a=exps r=reset { Ecall(op, a, r) } | e1=exp i_op=infix e2=exp - { mk_exp (Ecall(mk_op ~op_kind:Efun i_op, [e1; e2], None)) } + { Eapp(mk_op ~op_kind:Efun i_op, [e1; e2], None) } | p_op=prefix e=exp %prec prefixs - { mk_exp (Ecall(mk_op ~op_kind:Efun p_op, [e], None)) } - | IF e1=exp THEN e2=exp ELSE e3=exp { mk_exp (Eifthenelse(e1, e2, e3)) } - | e=simple_exp DOT m=longname { mk_exp (Efield(e, m)) } + { Eapp(mk_op ~op_kind:Efun p_op, [e], None) } + | IF e1=exp THEN e2=exp ELSE e3=exp { Eifthenelse(e1, e2, e3) } + | e=simple_exp DOT m=longname { Efield(e, m) } | e=exp WHEN c=constructor LPAREN n=ident RPAREN - { mk_exp (Ewhen(e, c, n)) } - | MERGE n=ident h=handlers { mk_exp (Emerge(n, h)) } - | LPAREN r=exp WITH DOT ln=longname EQUAL nv=exp /*ordre louche...*/ - { mk_exp (Efield_update(ln, r, nv)) } - | op=array_op { mk_exp (Earray_op op) } - | LBRACKET es=slist(COMMA, exp) RBRACKET { mk_exp (Earray es) } + { Ewhen(e, c, n) } + | MERGE n=ident h=handlers { Emerge(n, h) } + | LPAREN r=exp WITH DOT ln=longname EQUAL nv=exp + { Efield_update(ln, r, nv) } + | op=array_op { Earray_op op } + | LBRACKET es=slist(COMMA, exp) RBRACKET { Earray es } array_op: | e=exp POWER p=e_param { Erepeat(p, e) } @@ -186,7 +192,7 @@ array_op: | e=exp i=indexes(exp) DEFAULT d=exp { Eselect_dyn(i, e ,d) } | LPAREN e=exp WITH i=indexes(e_param) EQUAL nv=exp { Eupdate(i, e, nv) } | e=simple_exp LBRACKET i1=e_param DOTDOT i2=e_param RBRACKET - { Eselect_slice(i1, i2, e) } + { Eselect_slice(i1, i2, e) } | e1=exp AROBASE e2=exp { Econcat(e1,e2) } | LPAREN f=iterator LPAREN op=funop RPAREN DOUBLE_LESS p=e_param DOUBLE_GREATER diff --git a/compiler/utilities/global/compiler_utils.ml b/compiler/utilities/global/compiler_utils.ml index f358c70..3362d3e 100644 --- a/compiler/utilities/global/compiler_utils.ml +++ b/compiler/utilities/global/compiler_utils.ml @@ -61,11 +61,19 @@ let clean_dir dir = end else Unix.mkdir dir 0o740; dir -let init_compiler modname source_name ic = - Location.initialize source_name ic; +let init_compiler modname = Modules.initialize modname; Initial.initialize () +let lexbuf_from_file file_name = + let ic = open_in file_name in + let lexbuf = Lexing.from_channel ic in + lexbuf.Lexing.lex_curr_p <- + { lexbuf.Lexing.lex_curr_p with Lexing.pos_fname = file_name }; + ic, lexbuf + + + let doc_verbose = "\t\t\tSet verbose mode" and doc_version = "\t\tThe version of the compiler" and doc_print_types = "\t\t\tPrint types" diff --git a/heptc b/heptc index 1809b12..09ced57 100755 --- a/heptc +++ b/heptc @@ -4,7 +4,7 @@ SCRIPT_DIR=`dirname $0` COMPILER_DIR=compiler #relative to the script_dir -COMPILER=heptc.byte +COMPILER=heptc.native HEPTC=$COMPILER_DIR/$COMPILER cd $SCRIPT_DIR diff --git a/test/check b/test/check index 413ddd9..3caec2e 100755 --- a/test/check +++ b/test/check @@ -8,7 +8,7 @@ shopt -s nullglob # script de test -compilo=../compiler/heptc.native +compilo=../heptc coption= # compilateurs utilises pour les tests de gen. de code