Refactoring and organisation.

Separate parser, lexer and printer of hpetagon (Hetp_*) from the minils ones (Mls_*)
ident_of_var -> ident_of_name
get_current_location -> current_loc
This commit is contained in:
Léonard Gérard 2010-06-21 18:19:58 +02:00 committed by Léonard Gérard
parent 12251f960e
commit 9fff8e4ad8
22 changed files with 746 additions and 132 deletions

View File

@ -32,7 +32,7 @@ let fresh s =
num := !num + 1;
{ num = !num; source = s; is_generated = true }
let ident_of_var s =
let ident_of_name s =
num := !num + 1;
{ num = !num; source = s; is_generated = false }

View File

@ -16,9 +16,9 @@ val set_sourcename : ident -> string -> ident
(** [fresh n] returns a fresh identifier with source name n *)
val fresh : string -> ident
(** [ident_of_var n] returns an identifier corresponding
(** [ident_of_name n] returns an identifier corresponding
to a _source_ variable (do not use it for generated variables). *)
val ident_of_var : string -> ident
val ident_of_name : string -> ident
(** Maps taking an identifier as a key. *)
module Env :

View File

@ -25,7 +25,7 @@ let no_location = Loc(0,0)
let error_prompt = ">"
let get_current_location () =
let current_loc () =
Loc(symbol_start(), symbol_end())

View File

@ -45,7 +45,7 @@ module Type =
module Printer =
struct
open Format
open Printer
open Hept_printer
let deftype ff name tdesc =
match tdesc with

View File

@ -78,8 +78,8 @@ let message loc kind =
Printf.eprintf "%aType Clash: this expression has type %a, \n\
but is expected to have type %a.\n"
output_location loc
Printer.ptype actual_ty
Printer.ptype expected_ty
Hept_printer.ptype actual_ty
Hept_printer.ptype expected_ty
| Earity_clash(actual_arit, expected_arit) ->
Printf.eprintf "%aType Clash: this expression expects %d arguments,\n\
but is expected to have %d.\n"
@ -118,7 +118,7 @@ let message loc kind =
Printf.eprintf
"%aSubscript used on a non array type : %a.\n"
output_location loc
Printer.ptype ty
Hept_printer.ptype ty
| Earray_subscript_should_be_const ->
Printf.eprintf
"%aSubscript has to be a static value.\n"
@ -137,17 +137,17 @@ let message loc kind =
Printf.eprintf
"%aThis type should be static : %a.\n"
output_location loc
Printer.ptype ty
Hept_printer.ptype ty
| Erecord_type_expected ty ->
Printf.eprintf
"%aA record was expected (found %a).\n"
output_location loc
Printer.ptype ty
Hept_printer.ptype ty
| Eno_such_field (ty, f) ->
Printf.eprintf
"%aThe record type '%a' does not have a '%s' field.\n"
output_location loc
Printer.ptype ty
Hept_printer.ptype ty
(shortname f)
| Eempty_record ->
Printf.eprintf

View File

@ -167,7 +167,7 @@ let mk_equation ?(statefull = true) desc =
let mk_var_dec ?(last = Var) name ty =
{ v_name = name; v_type = ty;
v_last = last; v_loc = Location.get_current_location () }
v_last = last; v_loc = Location.current_loc () }
let mk_block ?(statefull = true) defnames eqs =
{ b_local = []; b_equs = eqs; b_defnames = defnames;

View File

@ -1,10 +1,9 @@
(* lexer.mll *)
(* $Id$ *)
{
open Lexing
open Parser
open Hept_parser
type lexical_error =
Illegal_character

View File

@ -24,7 +24,6 @@ open Parsetree
%token AMPERSAND
%token AMPERAMPER
%token AUTOMATON
%token SWITCH
%token PRESENT
%token RESET
%token STATE
@ -47,7 +46,7 @@ open Parsetree
%token POWER
%token LBRACKET
%token RBRACKET
%token WITH DOUBLE_DOT
%token DOUBLE_DOT
%token AROBASE
%token DOUBLE_LESS DOUBLE_GREATER
%token MAP FOLD MAPFOLD
@ -168,7 +167,7 @@ node_dec:
n_local = $12;
n_equs = $14;
n_params = $3;
n_loc = Location.get_current_location () }}
n_loc = Location.current_loc () }}
;
node_or_fun:

View File

@ -171,7 +171,7 @@ and interface_desc =
(* Helper functions to create AST. *)
let mk_exp desc =
{ e_desc = desc; e_loc = Location.get_current_location () }
{ e_desc = desc; e_loc = Location.current_loc () }
let mk_app op =
{ a_op = op; }
@ -192,25 +192,25 @@ let mk_iterator_call it ln params exps =
mk_array_op_call (Eiterator (it, mk_op_desc ln params Enode)) exps
let mk_type_dec name desc =
{ t_name = name; t_desc = desc; t_loc = Location.get_current_location () }
{ t_name = name; t_desc = desc; t_loc = Location.current_loc () }
let mk_equation desc =
{ eq_desc = desc; eq_loc = Location.get_current_location () }
{ eq_desc = desc; eq_loc = Location.current_loc () }
let mk_interface_decl desc =
{ interf_desc = desc; interf_loc = Location.get_current_location () }
{ interf_desc = desc; interf_loc = Location.current_loc () }
let mk_var_dec name ty last =
{ v_name = name; v_type = ty;
v_last = last; v_loc = Location.get_current_location () }
v_last = last; v_loc = Location.current_loc () }
let mk_block locals eqs =
{ b_local = locals; b_equs = eqs;
b_loc = Location.get_current_location () }
b_loc = Location.current_loc () }
let mk_const_dec id ty e =
{ c_name = id; c_type = ty; c_value = e;
c_loc = Location.get_current_location (); }
c_loc = Location.current_loc (); }
let mk_arg name ty =
{ a_type = ty; a_name = name }

View File

@ -62,13 +62,13 @@ let add_var loc x env =
if Rename.mem x env then
Error.message loc (Error.Evariable_already_defined x)
else (* create a new id for this var and add it to the env *)
Rename.add x (ident_of_var x) env
Rename.add x (ident_of_name x) env
let add_const_var loc x env =
if NamesEnv.mem x env then
Error.message loc (Error.Econst_variable_already_defined x)
else (* create a new id for this var and add it to the env *)
NamesEnv.add x (ident_of_var x) env
NamesEnv.add x (ident_of_name x) env
let rec build_pat loc env = function
| Evarpat x -> add_var loc x env

View File

@ -18,8 +18,6 @@ open Types
open Format
open Printf
module HeptPrinter = Printer
open Minils
open Signature

View File

@ -9,13 +9,27 @@
(* the main *)
open Misc
open Location
open Compiler_utils
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))
| Parsing.Parse_error ->
let pos1 = Lexing.lexeme_start lexbuf
and pos2 = Lexing.lexeme_end lexbuf in
let l = Loc(pos1,pos2) in
syntax_error l
let parse_implementation lexbuf =
parse Parser.program Lexer.token lexbuf
parse Hept_parser.program Hept_lexer.token lexbuf
let parse_interface lexbuf =
parse Parser.interface Lexer.token lexbuf
parse Hept_parser.interface Hept_lexer.token lexbuf
let interface modname filename =
(* input and output files *)
@ -71,7 +85,7 @@ let compile modname filename =
try
init_compiler modname source_name ic;
let pp = Printer.print stdout in
let pp = Hept_printer.print stdout in
(* Parsing of the file *)
let lexbuf = Lexing.from_channel ic in
@ -91,9 +105,9 @@ let compile modname filename =
(* Compile Heptagon to MiniLS *)
let p = Hept2mls.program p in
let pp = Minils_printer.print stdout in
let pp = Mls_printer.print stdout in
if !verbose then comment "Translation into MiniLs";
Minils_printer.print mlsc p;
Mls_printer.print mlsc p;
(* Process the MiniLS AST *)
let p = Mls_compiler.compile pp p in

View File

@ -7,69 +7,88 @@
(* *)
(**************************************************************************)
let generate_targets p =
(* Producing Object-based code *)
let o = Translate.program p in
if !verbose then comment "Translation into Object-based code";
Obc.Printer.print obc o;
open Misc
open Location
open Compiler_utils
open Mls2seq
let pp = Obc.Printer.print stdout in
if !verbose then pp o;
(* Translation into dataflow and sequential languages *)
targets filename p o !target_languages
let pp = Mls_printer.print stdout
let parse parsing_fun lexing_fun lexbuf =
try
parsing_fun lexing_fun lexbuf
with
| Mls_lexer.Lexical_error(err, pos1, pos2) ->
lexical_error err (Loc(pos1, pos2))
| Parsing.Parse_error ->
let pos1 = Lexing.lexeme_start lexbuf
and pos2 = Lexing.lexeme_end lexbuf in
let l = Loc(pos1,pos2) in
syntax_error l
let parse_implementation lexbuf =
parse Parser.program Lexer.token lexbuf
parse Mls_parser.program Mls_lexer.token lexbuf
let compile_impl modname filename =
let compile_impl modname filename =
(* input and output files *)
(* input and output files *)
let mls_name = filename ^ ".mls"
let source_name = filename ^ ".mls"
and mls_norm_name = filename ^ "_norm.mls"
and obc_name = filename ^ ".obc" in
let mlsc = open_out mls_name
let ic = open_in source_name
and mlsnc = open_out mls_norm_name
and obc = open_out obc_name in
let close_all_files () =
close_out mlsc;
close_in ic;
close_out obc;
close_out mlsnc
in
try
init_compiler modname source_name ic;
(* Parsing of the file *)
let lexbuf = Lexing.from_channel ic in
let p = parse_implementation lexbuf in
(* Convert the parse tree to Heptagon AST *)
let p = Scoping.translate_program p in
if !verbose
then begin
comment "Parsing";
pp p
end;
(* Call the compiler*)
Hept_compiler.compile_impl pp p;
if !verbose
then begin
comment "Checking"
end;
close_all_files ()
with x -> close_all_files (); raise x
try
init_compiler modname source_name ic;
(* Parsing of the file *)
let lexbuf = Lexing.from_channel ic in
let p = parse_implementation lexbuf in
if !verbose
then begin
comment "Parsing";
pp p
end;
(* Call the compiler*)
let p = Mls_compiler.compile pp p in
if !verbose
then begin
comment "Checking"
end;
(* Producing Object-based code *)
let o = Mls2obc.program p in
if !verbose then comment "Translation into Object-based code";
Obc.Printer.print obc o;
let pp = Obc.Printer.print stdout in
if !verbose then pp o;
(* Translation into dataflow and sequential languages *)
targets filename p o !target_languages;
close_all_files ()
with x -> close_all_files (); raise x
let compile file =
if Filename.check_suffix file ".mls" then
let filename = Filename.chop_suffix file ".ept" in
let filename = Filename.chop_suffix file ".mls" in
let modname = String.capitalize(Filename.basename filename) in
compile_impl modname filename
compile_impl modname filename
else
raise (Arg.Bad ("Unknow file type: " ^ file))
@ -79,22 +98,22 @@ let main () =
try
Arg.parse
[
"-v",Arg.Set verbose, doc_verbose;
"-version", Arg.Unit show_version, doc_version;
"-i", Arg.Set print_types, doc_print_types;
"-I", Arg.String add_include, doc_include;
"-where", Arg.Unit locate_stdlib, doc_locate_stdlib;
"-stdlib", Arg.String set_stdlib, doc_stdlib;
"-s", Arg.String set_simulation_node, doc_sim;
"-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives;
"-target", Arg.String add_target_language, doc_target;
"-targetpath", Arg.String set_target_path, doc_target_path;
"-noinit", Arg.Clear init, doc_noinit;
"-fti", Arg.Set full_type_info, doc_full_type_info;
"-v", Arg.Set verbose, doc_verbose;
"-version", Arg.Unit show_version, doc_version;
"-i", Arg.Set print_types, doc_print_types;
"-I", Arg.String add_include, doc_include;
"-where", Arg.Unit locate_stdlib, doc_locate_stdlib;
"-stdlib", Arg.String set_stdlib, doc_stdlib;
"-s", Arg.String set_simulation_node, doc_sim;
"-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives;
"-target", Arg.String add_target_language, doc_target;
"-targetpath", Arg.String set_target_path, doc_target_path;
"-noinit", Arg.Clear init, doc_noinit;
"-fti", Arg.Set full_type_info, doc_full_type_info;
]
compile
errmsg;
with
| Misc.Error -> exit 2;;
| Misc.Error -> exit 2;;
main ()

View File

@ -65,8 +65,8 @@ and array_op =
| Eupdate of size_exp list * exp * exp (*indices, array, value*)
| Eselect_slice of size_exp * size_exp * exp (*lower bound, upper bound, array*)
| Econcat of exp * exp
| Eiterator of iterator_type * op_desc * size_exp * exp list * ident option
(** [op_desc] is the function iterated,
| Eiterator of iterator_type * op_desc * size_exp * exp list * ident option (**
[op_desc] is the function iterated,
[size_exp] is the size of the iteration,
[exp list] is the passed arguments,
[ident option] is the optional reset condition *)
@ -153,6 +153,24 @@ let mk_var_dec ?(ck = Cbase) name ty =
let mk_equation ?(loc = no_location) pat exp =
{ eq_lhs = pat; eq_rhs = exp; eq_loc = loc }
let mk_node
?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = [])
?(loc = no_location) ?(param = []) ?(constraints = []) ?(pinst = []) name =
{ n_name = name;
n_input = input;
n_output = output;
n_contract = contract;
n_local = local;
n_equs = eq;
n_loc = loc;
n_params = param;
n_params_constraints = constraints;
n_params_instances = pinst; }
let mk_type_dec ?(type_desc = Type_abs) ?(loc = no_location) name =
{ t_name = name; t_desc = type_desc; t_loc = loc }
let rec size_exp_of_exp e =
match e.e_desc with

View File

@ -0,0 +1,295 @@
(* lexer.mll *)
{
open Lexing
open Mls_parser
type lexical_error =
Illegal_character
| Unterminated_comment
| Bad_char_constant
| Unterminated_string;;
exception Lexical_error of lexical_error * int * int;;
let comment_depth = ref 0
let keyword_table = ((Hashtbl.create 149) : (string, token) Hashtbl.t);;
List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [
"node", NODE;
"fun", FUN;
"safe", SAFE;
"returns", RETURNS;
"var", VAR;
"val", VAL;
"unsafe", UNSAFE;
"let", LET;
"tel", TEL;
"end", END;
"fby", FBY;
"switch", SWITCH;
"when", WHEN;
"type", TYPE;
"every", EVERY;
"true", BOOL(true);
"false", BOOL(false);
"pre", PRE;
"or", OR;
"not", NOT;
"open", OPEN;
"automaton", AUTOMATON;
"switch", SWITCH;
"present", PRESENT;
"reset", RESET;
"state", STATE;
"unless", UNLESS;
"until", UNTIL;
"emit", EMIT;
"last", LAST;
"if", IF;
"then", THEN;
"else", ELSE;
"default", DEFAULT;
"continue", CONTINUE;
"case", CASE;
"do", DO;
"contract", CONTRACT;
"assume", ASSUME;
"enforce", ENFORCE;
"with", WITH;
"inlined", INLINED;
"at", AT;
"quo", INFIX3("quo");
"mod", INFIX3("mod");
"land", INFIX3("land");
"lor", INFIX2("lor");
"lxor", INFIX2("lxor");
"lsl", INFIX4("lsl");
"lsr", INFIX4("lsr");
"asr", INFIX4("asr")
]
(* To buffer string literals *)
let initial_string_buffer = String.create 256
let string_buff = ref initial_string_buffer
let string_index = ref 0
let reset_string_buffer () =
string_buff := initial_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
let new_buff = String.create (String.length (!string_buff) * 2) in
String.blit (!string_buff) 0 new_buff 0 (String.length (!string_buff));
string_buff := new_buff
end;
String.set (!string_buff) (!string_index) c;
incr string_index
let get_stored_string () =
let s = String.sub (!string_buff) 0 (!string_index) in
string_buff := initial_string_buffer;
s
let char_for_backslash = function
'n' -> '\010'
| 'r' -> '\013'
| 'b' -> '\008'
| 't' -> '\009'
| c -> c
let char_for_decimal_code lexbuf i =
let c =
100 * (int_of_char(Lexing.lexeme_char lexbuf i) - 48) +
10 * (int_of_char(Lexing.lexeme_char lexbuf (i+1)) - 48) +
(int_of_char(Lexing.lexeme_char lexbuf (i+2)) - 48) in
char_of_int(c land 0xFF)
}
rule token = parse
| [' ' '\010' '\013' '\009' '\012'] + { token lexbuf }
| "." {DOT}
| "(" {LPAREN}
| ")" {RPAREN}
| "*" { STAR }
| "{" {LBRACE}
| "}" {RBRACE}
| ":" {COLON}
| ";" {SEMICOL}
| "=" {EQUAL}
| "==" {EQUALEQUAL}
| "&" {AMPERSAND}
| "&&" {AMPERAMPER}
| "||" {BARBAR}
| "," {COMMA}
| "->" {ARROW}
| "|" {BAR}
| "-" {SUBTRACTIVE "-"}
| "-." {SUBTRACTIVE "-."}
| (['A'-'Z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id)
{Constructor id}
| (['A'-'Z' 'a'-'z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id)
{ let s = Lexing.lexeme lexbuf in
try Hashtbl.find keyword_table s
with Not_found -> IDENT id }
| '-'? ['0'-'9']+
| '-'? '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
| '-'? '0' ['o' 'O'] ['0'-'7']+
| '-'? '0' ['b' 'B'] ['0'-'1']+
{ INT (int_of_string(Lexing.lexeme lexbuf)) }
| '-'? ['0'-'9']+ ('.' ['0'-'9']*)? (['e' 'E'] ['+' '-']? ['0'-'9']+)?
{ FLOAT (float_of_string(Lexing.lexeme lexbuf)) }
| "\""
{ reset_string_buffer();
let string_start = lexbuf.lex_start_pos + lexbuf.lex_abs_pos in
begin try
string lexbuf
with Lexical_error(Unterminated_string, _, string_end) ->
raise(Lexical_error(Unterminated_string, string_start, string_end))
end;
lexbuf.lex_start_pos <- string_start - lexbuf.lex_abs_pos;
STRING (get_stored_string()) }
| "'" [^ '\\' '\''] "'"
{ CHAR(Lexing.lexeme_char lexbuf 1) }
| "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'"
{ CHAR(char_for_backslash (Lexing.lexeme_char lexbuf 2)) }
| "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'"
{ CHAR(char_for_decimal_code lexbuf 2) }
| "(*@ " (['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
begin try
pragma lexbuf
with Lexical_error(Unterminated_comment, _, pragma_end) ->
raise(Lexical_error(Unterminated_comment, pragma_start, pragma_end))
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
comment_depth := 1;
begin try
comment lexbuf
with Lexical_error(Unterminated_comment, _, comment_end) ->
raise(Lexical_error(Unterminated_comment,
comment_start, comment_end))
end;
token lexbuf }
| ['!' '?' '~']
['!' '$' '%' '&' '*' '+' '-' '.' '/' ':'
'<' '=' '>' '?' '@' '^' '|' '~'] *
{ PREFIX(Lexing.lexeme lexbuf) }
| ['=' '<' '>' '&' '|' '&' '$']
['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>'
'?' '@' '^' '|' '~'] *
{ INFIX0(Lexing.lexeme lexbuf) }
| ['@' '^']
['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>'
'?' '@' '^' '|' '~'] *
{ INFIX1(Lexing.lexeme lexbuf) }
| ['+' '-']
['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>'
'?' '@' '^' '|' '~'] *
{ INFIX2(Lexing.lexeme lexbuf) }
| "**"
['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>'
'?' '@' '^' '|' '~'] *
{ INFIX4(Lexing.lexeme lexbuf) }
| ['*' '/' '%']
['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>'
'?' '@' '^' '|' '~'] *
{ INFIX3(Lexing.lexeme lexbuf) }
| eof {EOF}
| _ {raise (Lexical_error (Illegal_character,
Lexing.lexeme_start lexbuf,
Lexing.lexeme_end lexbuf))}
and pragma = parse
"(*"
{ let comment_start = lexbuf.lex_start_pos + lexbuf.lex_abs_pos in
comment_depth := 1;
begin try
comment lexbuf
with Lexical_error(Unterminated_comment, _, comment_end) ->
raise(Lexical_error(Unterminated_comment,
comment_start, comment_end))
end;
pragma lexbuf }
| "@*)"
{ }
| eof
{ raise(Lexical_error(Unterminated_comment,0,
Lexing.lexeme_start lexbuf)) }
| _
{ store_string_char(Lexing.lexeme_char lexbuf 0);
pragma lexbuf }
and comment = parse
"(*"
{ 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
begin try
string lexbuf
with Lexical_error(Unterminated_string, _, string_end) ->
raise(Lexical_error(Unterminated_string, string_start, string_end))
end;
comment lexbuf }
| "''"
{ comment lexbuf }
| "'" [^ '\\' '\''] "'"
{ comment lexbuf }
| "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'"
{ comment lexbuf }
| "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'"
{ comment lexbuf }
| eof
{ raise(Lexical_error(Unterminated_comment,0,
Lexing.lexeme_start lexbuf)) }
| _
{ comment lexbuf }
and string = parse
'"'
{ () }
| '\\' ("\010" | "\013" | "\013\010") [' ' '\009'] *
{ string lexbuf }
| '\\' ['\\' '"' 'n' 't' 'b' 'r']
{ store_string_char(char_for_backslash(Lexing.lexeme_char lexbuf 1));
string lexbuf }
| '\\' ['0'-'9'] ['0'-'9'] ['0'-'9']
{ store_string_char(char_for_decimal_code lexbuf 1);
string lexbuf }
| eof
{ raise (Lexical_error
(Unterminated_string, 0, Lexing.lexeme_start lexbuf)) }
| _
{ store_string_char(Lexing.lexeme_char lexbuf 0);
string lexbuf }
(* eof *)

View File

@ -0,0 +1,241 @@
%{
open Misc
open Signature
open Names
open Ident
open Types
open Location
open Minils
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
%}
%token DOT LPAREN RPAREN LBRACE RBRACE COLON SEMICOL
%token EQUAL EQUALEQUAL BARBAR COMMA BAR LET TEL
%token <string> CONSTRUCTOR
%token <string> NAME
%token <int> INT
%token <float> FLOAT
%token <bool> BOOL
%token <char> CHAR
%token <string> STRING
%token <string * string> PRAGMA
%token TYPE FUN NODE RETURNS VAR OPEN
%token FBY PRE SWITCH WHEN EVERY
%token OR STAR NOT
%token AMPERSAND
%token AMPERAMPER
%token AUTOMATON
%token PRESENT
%token RESET
%token STATE
%token UNLESS
%token UNTIL
%token EMIT
%token LAST
%token IF
%token THEN
%token ELSE
%token DEFAULT
%token DO
%token CONTINUE
%token CASE
%token CONTRACT
%token ASSUME
%token ENFORCE
%token WITH
%token INLINED
%token AT
%token <string> PREFIX
%token <string> INFIX0
%token <string> INFIX1
%token <string> INFIX2
%token <string> SUBTRACTIVE
%token <string> INFIX3
%token <string> INFIX4
%token EOF
%nonassoc prec_ident
%left IF ELSE
%right ARROW
%nonassoc EVERY
%left OR
%left AMPERSAND
%left INFIX0 EQUAL
%right INFIX1
%left INFIX2 SUBTRACTIVE
%left STAR INFIX3
%left INFIX4
%right prefixs
%right FBY
%right PRE
%right LAST
%right prec_apply
%left DOT
%start program
%type <Minils.program> program
%%
/** Tools **/
/* Redefinitions */
%inline option_list(x) : l=list(x) {l}
%inline list(x) : l=nonempty_list(x) {l}
%inline option_slist(S, x) : l=separated_list(S, x) {l}
%inline slist(S, x) : l=separated_nonempty_list(S, x) {l}
%inline nuple(L, R, S, x) : L h=x S t=slist(S,x) R { h::t }
%inline stuple(S, x) : LPAREN h=x S t=slist(S,x) RPAREN { h::t }
%inline tuple(x) : t=stuple(COMMA,x) { t }
%inline option2(P,x) : /* empty */ { None } | P v=x { Some(v)}
qualified(x) :
| n=x { Name(n) } %prec prec_ident
| m=CONSTRUCTOR DOT n=x { Modname({ qual = m; id = n }) }
structure(field): s=nuple(LBRACE, RBRACE, SEMICOL, field) {s}
program:
| pragma_headers open_modules type_decs node_decs EOF
{{ p_pragmas = List.rev $1;
p_opened = List.rev $2;
p_types = $3;
p_nodes = $4;
p_consts = []}} /*TODO consts dans program*/
pragma: p=PRAGMA {p}
pragma_headers: l=option_list(pragma) {l}
opens: OPEN c=CONSTRUCTOR {c}
open_modules: l=option_list(opens) {l}
field_type : n=NAME COLON t=type_ident { (n, t) }
type_ident: NAME { Tid(Name($1)) }
type_dec:
| TYPE n=NAME { mk_type n Type_abs }
| TYPE n=NAME EQUAL e=slist(BAR,NAME) { mk_type n (Type_enum e) }
| TYPE n=NAME EQUAL s=structure(field_type) { mk_type n (Type_struct s) }
type_decs: t=option_list(type_dec) {t}
node_dec:
NODE id=ident LPAREN args=params RPAREN RETURNS LPAREN out=params RPAREN
vars=loc_vars LET eqs=equs TEL
{ mk_node
~input: args
~output: out
~local: vars
~eq: eqs
id }
node_decs: ns=option_list(node_dec) {ns}
params: p=option_slist(SEMICOL, var) {p}
loc_vars:
| /* empty */ { [] }
| VAR vs=slist(SEMICOL, var) { vs }
var:
| ns=slist(COMMA, NAME) COLON t=type_ident
{ List.map (fun id -> mk_var id t) ns }
equ: p=pat EQUAL e=exp { mk_eq p e }
equs: e=option_slist(SEMICOL, equ) ?SEMICOL {e}
pat:
| n=NAME {Evarpat (ident_of_name n)}
| LPAREN p=slist(COMMA, pat) RPAREN {Etuplepat p}
longname: l=qualified(ident) {l}
constructor:
| ln=qualified(CONSTRUCTOR) {ln}
| b=BOOL { Name(if b then "true" else "false") }
const:
| INT { Cint($1) }
| FLOAT { Cfloat($1) }
| constructor { Cconstr($1) }
exps: LPAREN e=option_slist(COMMA, exp) RPAREN {e}
tuple_exp: LPAREN e=option_slist(COMMA, exp) RPAREN {e}
field_exp: longname EQUAL exp { ($1, $3) }
simple_exp:
| NAME { mk_exp (Evar (ident_of_name $1)) }
| c=const { mk_exp (Econst c) }
| s=structure(field_exp) { mk_exp (Estruct s) }
| t=tuple_exp { mk_exp (Etuple t) }
| LPAREN e=exp RPAREN { e }
exp:
| e=simple_exp { e }
| const FBY exp
{ make_exp (Efby(Some($1),$3)) }
| PRE exp
{ make_exp (Efby(None,$2)) }
| longname LPAREN exps RPAREN %prec prec_apply
{ make_exp (Eapp(make_app $1 Ino, $3)) }
| INLINED longname LPAREN exps RPAREN %prec prec_apply
{ make_exp (Eapp(make_app $2 Irec, $4)) }
| e1=exp op=infix e2=exp
{ make_exp (Eop(Name(op), [e1; e2])) }
| op=prefix e=exp %prec prefixs
{ make_exp (Eop(Name(op), [e])) }
| IF exp THEN exp ELSE exp
{ make_exp (Eifthenelse($2, $4, $6)) }
| exp DOT longname
{ make_exp (Efield($1, $3)) }
ident: n=NAME | LPAREN n=infix RPAREN | LPAREN n=prefix RPAREN { n }
%inline infix:
| op=INFIX0 | op=INFIX1 | op=INFIX2 | op=INFIX3 | op=INFIX4 { op }
| STAR { "*" }
| EQUAL { "=" }
| EQUALEQUAL { "==" }
| AMPERSAND { "&" } | AMPERAMPER { "&&" }
| OR { "or" } | BARBAR { "||" }
prefix:
| op = PREFIX { op }
| NOT { "not" }
| op = SUBTRACTIVE { "~" ^ op } /*TODO test 3 * -2 and co */
%%

View File

@ -7,13 +7,13 @@ open Format
open Signature
open Pp_tools
(* Every print_ function is boxed, that is it doesn't export break points,
(** Every print_ function is boxed, that is it doesn't export break points,
Exceptions are print_list* print_type_desc *)
(* Every print_ function is without heading white space,
(** Every print_ function is without heading white space,
except for print_type_desc *)
(* Every print_ function is without heading carry return *)
(** Every print_ function is without heading carry return *)
let iterator_to_string i =
match i with

View File

@ -7,7 +7,6 @@
(* *)
(**************************************************************************)
(* $Id$ *)
(** Abstract syntax tree for C programs. *)
(** {2 C abstract syntax tree } *)

View File

@ -20,19 +20,9 @@ let syntax_error loc =
let language_error lang =
Printf.eprintf "Unknown language: %s.\n" lang
let parse parsing_fun lexing_fun lexbuf =
try
parsing_fun lexing_fun lexbuf
with
| Lexer.Lexical_error(err, pos1, pos2) ->
lexical_error err (Loc(pos1, pos2))
| Parsing.Parse_error ->
let pos1 = Lexing.lexeme_start lexbuf
and pos2 = Lexing.lexeme_end lexbuf in
let l = Loc(pos1,pos2) in
syntax_error l
let comment s = Printf.printf "** %s done **\n" s; flush stdout
let comment s =
if !verbose then Printf.printf "** %s done **\n" s; flush stdout
let do_pass f d p pp enabled =
if enabled

View File

@ -10,13 +10,6 @@
open Format
(** {2 list couple and option generic functions} *)
(** Most of theses functions export breaks or breaking spaces
to the calling printer. *)
(** Print the list [x1...xn] as [lp x1 sep \@, x2 ... sep \@, xn rp]
and nothing if the list is empty,
no space is added, but a break right after every [sep]. *)
let rec print_list print lp sep rp ff = function
| [] -> ()
| x::l ->
@ -24,9 +17,7 @@ let rec print_list print lp sep rp ff = function
List.iter (fprintf ff "%s@,%a" sep print) l;
fprintf ff "%s" rp
(** Prints the list [x1...xn] : [lp x1 sep \@ x2 ... sep \@ xn rp]
and nothing if the list is empty
a breaking space is added after every [sep]. *)
let rec print_list_r print lp sep rp ff = function
| [] -> ()
| x :: l ->
@ -34,9 +25,7 @@ let rec print_list_r print lp sep rp ff = function
List.iter (fprintf ff "%s@ %a" sep print) l;
fprintf ff "%s" rp
(** Print the list [x1...xn] : [lp x1 \@ sep x2 ... \@ sep xn rp]
and nothing if the list is empty
a breaking space is added before every [sep]. *)
let rec print_list_l print lp sep rp ff = function
| [] -> ()
| x :: l ->
@ -44,28 +33,21 @@ let rec print_list_l print lp sep rp ff = function
List.iter (fprintf ff "@ %s%a" sep print) l;
fprintf ff "%s" rp
(** Print the couple [(c1,c2)] as [lp c1 sep \@, c2 rp]
no space is added, but a break right after [sep]. *)
let print_couple print1 print2 lp sep rp ff (c1, c2) =
fprintf ff "%s%a%s@,%a%s" lp print1 c1 sep print2 c2 rp
(** Print something only in the case of [Some] *)
let print_opt print ff = function
| None -> ()
| Some(s) -> print ff s
(** Print [sep][s] only when [Some(s)]. *)
let print_opt2 print sep ff = function
| None -> ()
| Some(s) -> fprintf ff "%s%a" sep print s
(** {2 Common and usual syntax} *)
(** Theses functions are not exporting breaks
and they assume the same from the print functions passed as arguments *)
(** Print a record as [{field1;\@ field2;\@ ...}] with an hv<2> box
@param print_field is the print function for a field
@param record is the list of fields. *)
let print_record print_field ff record =
fprintf ff "@[<hv2>%a@]" (print_list_r print_field "{ "";"" }") record

View File

@ -0,0 +1,60 @@
(**************************************************************************)
(* *)
(* Lucid Synchrone V4 *)
(* Copyright (C) 2008 Marc Pouzet *)
(* Organization : LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(** Useful stuff for printing *)
(** {2 list couple and option generic functions} *)
(** Most of theses functions export breaks or breaking spaces
to the calling printer. *)
(** Print the list [x1...xn] as [lp x1 sep \@, x2 ... sep \@, xn rp]
and nothing if the list is empty,
no space is added, but a break right after every [sep]. *)
val print_list :
(Format.formatter -> 'a -> unit) ->
string -> string -> string -> Format.formatter -> 'a list -> unit
(** Prints the list [x1...xn] : [lp x1 sep \@ x2 ... sep \@ xn rp]
and nothing if the list is empty
a breaking space is added after every [sep]. *)
val print_list_r :
(Format.formatter -> 'a -> unit) ->
string -> string -> string -> Format.formatter -> 'a list -> unit
(** Print the list [x1...xn] : [lp x1 \@ sep x2 ... \@ sep xn rp]
and nothing if the list is empty
a breaking space is added before every [sep]. *)
val print_list_l :
(Format.formatter -> 'a -> unit) ->
string -> string -> string -> Format.formatter -> 'a list -> unit
(** Print the couple [(c1,c2)] as [lp c1 sep \@, c2 rp]
no space is added, but a break right after [sep]. *)
val print_couple :
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
string -> string -> string -> Format.formatter -> 'a * 'b -> unit
(** Print something only in the case of [Some] *)
val print_opt : ('a -> 'b -> unit) -> 'a -> 'b option -> unit
(** Print [sep][s] only when [Some(s)]. *)
val print_opt2 :
(Format.formatter -> 'a -> unit) ->
string -> Format.formatter -> 'a option -> unit
(** {2 Common and usual syntax} *)
(** Theses functions are not exporting breaks
and they assume the same from the print functions passed as arguments *)
(** Print a record as [{field1;\@ field2;\@ ...}] with an hv<2> box *)
val print_record :
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
val print_type_params : Format.formatter -> string list -> unit