Removed brocken and useless mlsc, cleaned heptc.

This commit is contained in:
Léonard Gérard 2011-01-07 17:16:50 +01:00 committed by Léonard Gérard
parent a832cc5c25
commit 0768babab7
12 changed files with 152 additions and 934 deletions

View file

@ -14,27 +14,7 @@ open Global_printer
let pp p = if !verbose then Hept_printer.print stdout p
let parse parsing_fun lexing_fun lexbuf =
try
parsing_fun lexing_fun lexbuf
with
| Hept_lexer.Lexical_error(err, l) ->
lexical_error err l
| Hept_parser.Error ->
let pos1 = Lexing.lexeme_start_p lexbuf
and pos2 = Lexing.lexeme_end_p lexbuf in
let l = Loc(pos1,pos2) in
syntax_error l
let parse_implementation modname lexbuf =
let p = parse Hept_parser.program Hept_lexer.token lexbuf in
{ p with Hept_parsetree.p_modname = modname }
let parse_interface lexbuf =
parse Hept_parser.interface Hept_lexer.token lexbuf
let compile_impl pp p =
let compile_program p =
(* Typing *)
let p = silent_pass "Statefullness check" true Statefull.program p in
let p = pass "Typing" true Typing.program p pp in
@ -79,45 +59,4 @@ let compile_impl pp p =
(* Return the transformed AST *)
p
let compile_interface modname filename =
(* input and output files *)
let source_name = filename ^ ".epi" in
let obj_interf_name = filename ^ ".epci" 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
Initial.initialize modname;
(* Parsing of the file *)
let l = do_silent_pass "Parsing" parse_interface lexbuf in
(* Convert the parse tree to Heptagon AST *)
let _ = do_silent_pass "Scoping" Hept_scoping.translate_interface l in
if !print_types then print_interface Format.std_formatter;
output_value itc (Modules.current_module ());
close_all_files ()
with
| x -> close_all_files (); raise x
let compile compile_implementation file =
if Filename.check_suffix file ".ept"
then
let filename = Filename.chop_suffix file ".ept" in
let modname = String.capitalize(Filename.basename filename) in
compile_implementation modname filename
else if Filename.check_suffix file ".epi"
then
let filename = Filename.chop_suffix file ".epi" in
let modname = String.capitalize(Filename.basename filename) in
compile_interface modname filename
else
raise (Arg.Bad ("Unknow file type: " ^ file))

View file

@ -0,0 +1,55 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
open Compiler_options
open Compiler_utils
open Location
open Global_printer
let pp p = if !verbose then Hept_printer.print stdout p
let parse parsing_fun lexbuf =
try
parsing_fun Hept_lexer.token lexbuf
with
| Hept_lexer.Lexical_error(err, l) ->
lexical_error err l
| Hept_parser.Error ->
let pos1 = Lexing.lexeme_start_p lexbuf
and pos2 = Lexing.lexeme_end_p lexbuf in
let l = Loc(pos1,pos2) in
syntax_error l
(** Parse an implementation [lexbuf] *)
let parse_program modname lexbuf =
(* Parsing of the file *)
let p = do_silent_pass "Parsing" (parse Hept_parser.program) lexbuf in
let p = { p with Hept_parsetree.p_modname = modname } in
(* Fuse static exps together *)
let p = do_silent_pass "Static Scoping" Hept_static_scoping.program p in
(* Convert the parse tree to Heptagon AST *)
let p = do_pass "Scoping" Hept_scoping.translate_program p pp in
p
(** Parse an interface [lexbuf] *)
let parse_interface modname lexbuf =
(* Parsing of the file *)
let i = do_silent_pass "Parsing" (parse Hept_parser.interface) lexbuf in
(* TODO ?
let i = { i with Hept_parsetree.=i_modname = modname } in *)
(* Fuse static exps together *) (* TODO cf Hept_static_scoping *)
(*let i = do_silent_pass "Static Scoping" Hept_static_scoping.interface i in *)
(* Convert the parse tree to Heptagon AST *)
let i = do_silent_pass "Scoping" Hept_scoping.translate_interface i in
i

View file

@ -58,11 +58,19 @@ let const_dec funs local_const cd =
let c_name = current_qual cd.c_name in
let c_type = Hept_scoping.translate_type cd.c_loc cd.c_type in
let c_value = Hept_scoping.expect_static_exp cd.c_value in
add_const c_name (Signature.mk_const_def c_type c_value);
cd, local_const
add_const c_name (Signature.mk_const_def c_type c_value);
cd, local_const
let program p =
let funs = { Hept_parsetree_mapfold.defaults
with node_dec = node; exp = exp; const_dec = const_dec } in
let p, _ = Hept_parsetree_mapfold.program_it funs Names.S.empty p in
p
p
(* (* TODO mapfold on interface *)
let interface i =
let funs = { Hept_parsetree_mapfold.defaults
with node_dec = node; exp = exp; const_dec = const_dec } in
let i, _ = Hept_parsetree_mapfold.interface_it funs Names.S.empty i in
i
*)

View file

@ -13,63 +13,79 @@ open Modules
open Location
open Compiler_utils
open Compiler_options
open Hept_compiler
let compile_interface modname source_f =
let compile_impl modname filename =
(* input and output files *)
let source_name = filename ^ ".ept" in
let filename = String.uncapitalize filename
and obj_interf_name = filename ^ ".epci"
and mls_name = filename ^ ".mls" in
(* output file names *)
let output = String.uncapitalize modname in
let epci_f = output ^ ".epci" in
let ic, lexbuf = lexbuf_from_file source_name
and itc = open_out_bin obj_interf_name
and mlsc = open_out mls_name in
let close_all_files () =
close_in ic;
close_out itc;
close_out mlsc in
(* input/output channels *)
let source_c, lexbuf = lexbuf_from_file source_f in
let epci_c = open_out_bin epci_f in
let close_all_files () = close_in source_c; close_out epci_c in
try
Initial.initialize modname;
add_include (Filename.dirname filename);
(* Parsing of the file *)
let p = do_silent_pass "Parsing" (parse_implementation modname) lexbuf in
(* Fuse static exps together *)
let p = do_silent_pass "Static Scoping"
Hept_static_scoping.program p in
(* Convert the parse tree to Heptagon AST *)
let p = do_pass "Scoping" Hept_scoping.translate_program p pp in
(* Process the Heptagon AST *)
let p = compile_impl pp p in
output_value itc (Modules.current_module ());
(* Set pretty printer to the Minils one *)
let pp = Mls_compiler.pp in
(* Compile Heptagon to MiniLS *)
let p = do_pass "Translation into MiniLs" Hept2mls.program p pp in
Mls_printer.print mlsc p;
(* Process the MiniLS AST *)
let p = Mls_compiler.compile pp p in
(* Generate the sequential code *)
Mls2seq.program p;
(* Process the [lexbuf] to an Heptagon AST *)
let _ = Hept_parser_scoper.parse_interface modname lexbuf in
if !print_types then Global_printer.print_interface Format.std_formatter;
(* Output the .epci *)
output_value epci_c (Modules.current_module ());
close_all_files ()
with
| x -> close_all_files (); raise x
(* [modname] is the module name, [source_f] is the source file *)
let compile_program modname source_f =
(* output file names *)
let output = String.uncapitalize modname in
let epci_f = output ^ ".epci" in
let mls_f = output ^ ".mls" in
(* input/output channels *)
let source_c, lexbuf = lexbuf_from_file source_f in
let epci_c = open_out_bin epci_f in
let mls_c = open_out mls_f in
let close_all_files () = close_in source_c; close_out epci_c; close_out mls_c in
try
(* Process the [lexbuf] to an Heptagon AST *)
let p = Hept_parser_scoper.parse_program modname lexbuf in
(* Process the Heptagon AST *)
let p = Hept_compiler.compile_program p in
(* Output the .epci *)
output_value epci_c (Modules.current_module ());
(* Compile Heptagon to MiniLS *)
let p = do_pass "Translation into MiniLs" Hept2mls.program p Mls_compiler.pp in
(* Output the .mls *)
Mls_printer.print mls_c p;
(* Process the MiniLS AST *)
let p = Mls_compiler.compile_program p in
(* Generate the sequential code *)
Mls2seq.program p;
close_all_files ()
with x -> close_all_files (); raise x
let read_qualname f = Arg.String (fun s -> f (Names.qualname_of_string s))
let compile source_f =
let modname = source_f |> Filename.basename |> Filename.chop_extension |> String.capitalize in
Initial.initialize modname;
source_f |> Filename.dirname |> add_include;
match Misc.file_extension source_f with
| "ept" -> compile_program modname source_f
| "epi" -> compile_interface modname source_f
| ext -> raise (Arg.Bad ("Unknow file type: " ^ ext ^ " for file: " ^ source_f))
(** [main] function to be launched *)
let main () =
let read_qualname f = Arg.String (fun s -> f (Names.qualname_of_string s)) in
try
Arg.parse
[
@ -96,9 +112,10 @@ let main () =
"-fname", Arg.Set full_name, doc_full_name;
"-itfusion", Arg.Set do_iterator_fusion, doc_itfusion;
]
(compile compile_impl)
errmsg;
compile errmsg;
with
| Errors.Error -> exit 2;;
(** Launch the [main] *)
main ()

View file

@ -13,7 +13,7 @@ open Compiler_options
let pp p = if !verbose then Mls_printer.print stdout p
let compile pp p =
let compile_program p =
(* Clocking *)
let p = pass "Clocking" true Clocking.program p pp in

View file

@ -1,89 +0,0 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
open Misc
open Location
open Compiler_utils
open Mls2seq
let compile_impl modname filename =
(* input and output files *)
let source_name = filename ^ ".mls"
and mls_norm_name = filename ^ "_norm.mls"
and obc_name = filename ^ ".obc" in
let ic, lexbuf = lexbuf_from_file source_name
and mlsnc = open_out mls_norm_name
and obc = open_out obc_name in
let close_all_files () =
close_in ic;
close_out obc;
close_out mlsnc
in
try
Initial.initialize modname;
(* Set pretty printer to the Minils one *)
let pp = Mls_compiler.pp in
(* Parsing of the file *)
let p = do_silent_pass "Parsing" (Mls_compiler.parse_implementation modname)
lexbuf in
(* Convert Parse tree to Minils AST *)
let p = do_pass "Scoping" Mls_scoping.translate_program p pp in
(* Process the MiniLS AST *)
let p = Mls_compiler.compile pp p in
(* Generate the sequential code *)
Mls2seq.program p;
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 ".mls" in
let modname = String.capitalize(Filename.basename filename) in
compile_impl modname filename
else
raise (Arg.Bad ("Unknow file type: " ^ file))
let errmsg = "Options are:"
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;
"-c", Arg.Set create_object_file, doc_object_file;
"-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;
"-itfusion", Arg.Set do_iterator_fusion, doc_itfusion;
]
compile
errmsg;
with
| Errors.Error -> exit 2;;
main ()

View file

@ -1,275 +0,0 @@
(* lexer.mll *)
{
open Location
open Lexing
open Mls_parser
open Compiler_utils
exception Lexical_error of lexical_error * location;;
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;
"returns", RETURNS;
"var", VAR;
"let", LET;
"tel", TEL;
"contract", CONTRACT;
"assume", ASSUME;
"enforce", ENFORCE;
"with", WITH;
"fby", FBY;
"when", WHEN;
"merge", MERGE;
"type", TYPE;
"true", BOOL(true);
"false", BOOL(false);
"pre", PRE;
"or", OR;
"not", NOT;
"open", OPEN;
"reset", RESET;
"const", CONST;
"if", IF;
"then", THEN;
"else", ELSE;
"with", WITH;
"map", MAP;
"fold", FOLD;
"mapfold", MAPFOLD;
"default", DEFAULT;
"quo", INFIX3("quo");
"mod", INFIX3("mod");
"land", INFIX3("land");
"lor", INFIX2("lor");
"lxor", INFIX2("lxor");
"lsl", INFIX4("lsl");
"lsr", INFIX4("lsr");
"asr", INFIX4("asr");
"on", ON;
]
(* 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)
}
let newline = '\n' | '\r' '\n'
rule token = parse
| newline { new_line lexbuf; token lexbuf }
| [' ' '\t'] + { token lexbuf }
| "." { DOT }
| ".." { DOTDOT }
| "(" { LPAREN }
| ")" { RPAREN }
| "*" { STAR }
| "{" { LBRACE }
| "}" { RBRACE }
| "[" { LBRACKET }
| "]" { RBRACKET }
| ":" { COLON }
| "::" { COLONCOLON }
| ";" { SEMICOL }
| "=" { EQUAL }
| "==" { EQUALEQUAL }
| "&" { AMPERSAND }
| "&&" { AMPERAMPER }
| "||" { BARBAR }
| "," { COMMA }
| "->" { ARROW }
| "|" { BAR }
| "-" { SUBTRACTIVE "-" }
| "-." { SUBTRACTIVE "-." }
| "_" { UNDERSCORE }
| "^" { POWER }
| "@" { AROBASE }
| "<<" { DOUBLE_LESS }
| ">>" { DOUBLE_GREATER }
| (['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 -> NAME 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)) }
(* | "(*@ " (['A'-'Z' 'a'-'z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id)
{
reset_string_buffer();
let l1 = lexbuf.lex_curr_p in
begin try
pragma lexbuf
with Lexical_error(Unterminated_comment, Loc(_, l2)) ->
raise(Lexical_error(Unterminated_comment, Loc (l1, l2)))
end;
PRAGMA(id,get_stored_string())
}*)
| "(*"
{ let comment_start = lexbuf.lex_curr_p in
comment_depth := 1;
begin try
comment lexbuf
with Lexical_error(Unterminated_comment, (Loc (_, comment_end))) ->
raise(Lexical_error(Unterminated_comment,
Loc (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,
Loc (Lexing.lexeme_start_p lexbuf,
Lexing.lexeme_end_p lexbuf)))}
and pragma = parse
| 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, Loc (_, comment_end)) ->
raise(Lexical_error(Unterminated_comment,
Loc (comment_start, comment_end)))
end;
pragma lexbuf }
| "@*)"
{ }
| eof
{ 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
"(*"
{ 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_curr_p in
begin try
string lexbuf
with Lexical_error(Unterminated_string, Loc (_, string_end)) ->
raise(Lexical_error
(Unterminated_string, Loc (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, Loc(dummy_pos,
Lexing.lexeme_start_p 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, Loc (dummy_pos,
Lexing.lexeme_start_p lexbuf))) }
| _
{ store_string_char(Lexing.lexeme_char lexbuf 0);
string lexbuf }
(* eof *)

View file

@ -1,315 +0,0 @@
%{
open Signature
open Names
open Idents
open Types
open Clocks
open Location
open Minils
open Mls_parsetree
open Mls_utils
%}
%token DOT LPAREN RPAREN LBRACE RBRACE COLON SEMICOL
%token EQUAL EQUALEQUAL BARBAR COMMA BAR LET TEL CONST
%token <string> CONSTRUCTOR
%token <string> NAME
%token <int> INT
%token <float> FLOAT
%token <bool> BOOL
%token TYPE NODE RETURNS VAR OPEN
%token FBY PRE WHEN
%token OR STAR NOT
%token AMPERSAND
%token AMPERAMPER
%token RESET
%token IF THEN ELSE
%token DOUBLE_LESS DOUBLE_GREATER
%token ARROW
%token MERGE
%token POWER
%token AROBASE
%token WITH
%token DOTDOT
%token BASE UNDERSCORE ON COLONCOLON
%token DEFAULT
%token LBRACKET RBRACKET
%token MAP FOLD MAPFOLD
%token <string> PREFIX
%token <string> INFIX0
%token <string> INFIX1
%token <string> INFIX2
%token <string> SUBTRACTIVE
%token <string> INFIX3
%token <string> INFIX4
%token EOF
%right AROBASE
%nonassoc DEFAULT
%left ELSE
%left OR
%left AMPERSAND
%left INFIX0 EQUAL
%right INFIX1 EQUALEQUAL BARBAR AMPERAMPER
%left INFIX2 prefixs
%left STAR INFIX3
%left INFIX4
%left WHEN
%right FBY
%right PRE
%right POWER
%start program
%type <Mls_parsetree.program> program
%%
/** Tools **/
%inline slist(S, x) : l=separated_list(S, x) {l}
%inline snlist(S, x) : l=separated_nonempty_list(S, x) {l}
%inline tuple(x) : LPAREN h=x COMMA t=snlist(COMMA,x) RPAREN { h::t }
%inline option(P,x):
|/* empty */ { None }
| P v=x { Some(v) }
qualified(x) :
| n=x { Modules.qualname n }
| m=CONSTRUCTOR DOT n=x { { qual = m; name = n } }
structure(field): LBRACE s=snlist(SEMICOL,field) RBRACE {s}
localize(x): y=x { y, (Loc($startpos(y),$endpos(y))) }
program:
| o=open_modules c=const_decs t=type_decs n=node_decs EOF
{ mk_program o n t c }
open_modules: l=list(opens) {l}
opens: OPEN c=CONSTRUCTOR {c}
const_decs: c=list(const_dec) {c}
const_dec:
| CONST n=qualname COLON t=type_ident EQUAL e=const
{ mk_const_dec n t e (Loc($startpos,$endpos)) }
name: n=NAME | LPAREN n=infix RPAREN | LPAREN n=prefix RPAREN { n }
qualname: n=name { Modules.qualname n }
field_type : n=qualname COLON t=type_ident { mk_field n t }
type_ident: qualname { Tid($1) }
type_decs: t=list(type_dec) {t}
type_dec:
| TYPE n=qualname
{ mk_type_dec Type_abs n (Loc ($startpos,$endpos)) }
| TYPE n=qualname EQUAL e=snlist(BAR,constructor)
{ mk_type_dec (Type_enum e) n (Loc ($startpos,$endpos)) }
| TYPE n=qualname EQUAL s=structure(field_type)
{ mk_type_dec (Type_struct s) n (Loc ($startpos,$endpos)) }
node_decs: ns=list(node_dec) {ns}
node_dec:
NODE n=qualname p=params(n_param) LPAREN args=args RPAREN
RETURNS LPAREN out=args RPAREN
contract=contract vars=loc_vars eqs=equs
{ mk_node p args out vars eqs
~loc:(Loc ($startpos,$endpos))
~contract:contract
n }
contract:
| /* empty */ {None}
| CONTRACT
locvars=loc_vars
eqs=opt_equs
assume=opt_assume
enforce=opt_enforce
withvar=opt_with
{ Some{ c_local=locvars;
c_equs=eqs;
c_assume = assume;
c_enforce = enforce;
c_controllables = withvar } }
;
opt_assume:
| /* empty */ { mk_constructor_exp ptrue (Loc($startpos,$endpos)) }
| ASSUME exp { $2 }
;
opt_enforce:
| /* empty */ { mk_constructor_exp ptrue (Loc($startpos,$endpos)) }
| ENFORCE exp { $2 }
;
opt_with:
| /* empty */ { [] }
| WITH LPAREN params RPAREN { $3 }
;
args_t: SEMICOL p=args {p}
args:
| /* empty */ { [] }
| h=var t=loption(args_t) {h@t}
loc_vars_t:
| /*empty */ { [] }
| SEMICOL { [] }
| SEMICOL h=var t=loc_vars_t {h@t}
loc_vars_h: VAR h=var t=loc_vars_t {h@t}
loc_vars: l=loption(loc_vars_h) {l}
ck_base: | UNDERSCORE | BASE {}
ck:
| ck_base { Cbase }
| ck=ck ON c=constructor LPAREN x=NAME RPAREN { Con (ck, c, x) }
clock_annot:
| /*empty*/ { Cbase }
| COLONCOLON c=ck { c }
var:
| ns=snlist(COMMA, NAME) COLON t=type_ident c=clock_annot
{ List.map (fun n -> mk_var_dec n t c (Loc ($startpos,$endpos))) ns }
opt_equs:
| /* empty */ { [] }
| LET e=slist(SEMICOL, equ) TEL { e }
equs: LET e=slist(SEMICOL, equ) TEL { e }
equ: p=pat EQUAL e=exp { mk_equation p e (Loc ($startpos,$endpos)) }
pat:
| n=NAME {Evarpat n}
| LPAREN p=snlist(COMMA, pat) RPAREN {Etuplepat p}
longname: l=qualified(name) {l}
constructor: /* of type longname */
| ln=qualified(CONSTRUCTOR) { ln }
| b=BOOL { if b then Initial.ptrue else Initial.pfalse }
field:
| c=constructor { mk_constructor_exp c (Loc($startpos,$endpos))}
const: c=_const { mk_static_exp ~loc:(Loc ($startpos,$endpos)) c }
_const:
| i=INT { Sint i }
| f=FLOAT { Sfloat f }
| c=constructor { Sconstructor c }
exps: LPAREN e=slist(COMMA, exp) RPAREN {e}
field_exp: longname EQUAL exp { ($1, $3) }
simple_exp:
| e=_simple_exp {mk_exp e (Loc ($startpos,$endpos)) }
_simple_exp:
| n=NAME { Evar n }
| s=structure(field_exp) { Estruct s }
| t=tuple(exp_woc) { mk_call [] Etuple t None }
| t=tuple(const)
{Econst (mk_static_exp ~loc:(Loc ($startpos,$endpos)) (Stuple t))}
| LBRACKET es=slist(COMMA, exp) RBRACKET { mk_call [] Earray es None }
| LPAREN e=_exp RPAREN { e }
exp:
| e=simple_exp { e }
| e=_exp { mk_exp e (Loc ($startpos,$endpos)) }
exp_woc:
| e=simple_exp { e }
| e=_exp_woc { mk_exp e (Loc ($startpos,$endpos)) }
_exp:
| e=_exp_woc {e}
| c=const { Econst c }
_exp_woc:
| v=exp FBY e=exp { Efby(Some(v), e) }
| PRE exp { Efby(None,$2) }
| app=funapp a=exps r=reset { Eapp(app, a, r) }
| e1=exp i_op=infix e2=exp
{ mk_op_call i_op [e1; e2] }
| p_op=prefix e=exp %prec prefixs
{ mk_op_call p_op [e] }
| IF e1=exp THEN e2=exp ELSE e3=exp
{ mk_call [] Eifthenelse [e1; e2; e3] None }
| e=simple_exp DOT f=field
{ mk_call [f] Efield [e] None }
| e=exp WHEN c=constructor LPAREN n=name RPAREN { Ewhen(e, c, n) }
| MERGE n=name h=handlers { Emerge(n, h) }
| LPAREN r=exp WITH DOT f=field EQUAL nv=exp
{ mk_call [f] Efield_update [r; nv] None }
| e=exp POWER p=e_param
{ mk_call [p] Earray_fill [e] None }
| e=simple_exp i=indexes(exp) /* not e_params to solve conflicts */
{ mk_call i Eselect [e] None }
| e=simple_exp i=indexes(exp) DEFAULT d=exp
{ mk_call [] Eselect_dyn ([e; d]@i) None }
| LPAREN e=exp WITH i=indexes(e_param) EQUAL nv=exp
{ mk_call i Eupdate [e; nv] None }
| e=simple_exp LBRACKET i1=e_param DOTDOT i2=e_param RBRACKET
{ mk_call [i1; i2] Eselect_slice [e] None }
| e1=exp AROBASE e2=exp { mk_call [] Econcat [e1;e2] None }
| LPAREN f=iterator LPAREN op=funapp RPAREN
DOUBLE_LESS p=e_param DOUBLE_GREATER
RPAREN a=exps r=reset { Eiterator(f,op,p,a,r) }
/* Static indexes [p1][p2]... */
indexes(param): is=nonempty_list(index(param)) { is }
index(param): LBRACKET p=param RBRACKET { p }
/* Merge handlers ( B -> e ) ( C -> ec )... */
handlers: hs=nonempty_list(handler) { hs }
handler: LPAREN c=constructor ARROW e=exp RPAREN { c,e }
iterator:
| MAP { Imap }
| FOLD { Ifold }
| MAPFOLD { Imapfold }
reset: r=option(RESET,name) { r }
funapp: ln=longname p=params(e_param) { mk_app p (Enode ln) }
/* inline so that precendance of POWER is respected in exp */
%inline e_param: e=exp { e }
n_param: n=NAME COLON ty=type_ident { mk_param n ty }
params(param):
| /*empty*/ { [] }
| DOUBLE_LESS p=slist(COMMA, param) DOUBLE_GREATER { p }
/*Inlining is compulsory in order to preserve priorities*/
%inline infix:
| op=INFIX0 | op=INFIX1 | op=INFIX2 | op=INFIX3 | op=INFIX4 { op }
| STAR { "*" }
| EQUAL { "=" }
| EQUALEQUAL { "==" }
| AMPERSAND { "&" } | AMPERAMPER { "&&" }
| OR { "or" } | BARBAR { "||" }
%inline prefix:
| op = PREFIX { op }
| NOT { "not" }
| op = SUBTRACTIVE { "~" ^ op } /*TODO test 3 * -2 and co */
%%

View file

@ -1,126 +0,0 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
open Location
open Names
open Signature
open Static
open Types
open Clocks
type var_name = name
type ck =
| Cbase
| Con of ck * constructor_name * var_name
type exp = {
e_desc: edesc;
e_loc: location }
and app = { a_op: Minils.op; a_params: exp list }
and edesc =
| Econst of static_exp
| Evar of var_name
| Efby of exp option * exp
| Eapp of app * exp list * var_name option
| Ewhen of exp * constructor_name * var_name
| Emerge of var_name * (constructor_name * exp) list
| Estruct of (field_name * exp) list
| Eiterator of
Minils.iterator_type * app * exp * exp list * var_name option
and pat =
| Etuplepat of pat list
| Evarpat of var_name
and eq = {
eq_lhs : pat;
eq_rhs : exp;
eq_loc : location }
and var_dec = {
v_name : var_name;
v_type : ty;
v_clock : ck;
v_loc : location }
type contract =
{ c_assume : exp;
c_enforce : exp;
c_controllables : var_dec list;
c_local : var_dec list;
c_equs : eq list }
type node_dec = {
n_name : qualname;
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
n_local : var_dec list;
n_equs : eq list;
n_loc : location;
n_params : param list }
type program = {
p_modname : name;
p_format_version : string;
p_opened : name list;
p_types : Minils.type_dec list;
p_nodes : node_dec list;
p_consts : Minils.const_dec list }
(** {Helper functions to build the Parsetree *)
let mk_node params input output locals eqs ?(loc = no_location)
?(contract = None) ?(constraints = []) name =
{ n_name = name;
n_input = input;
n_output = output;
n_contract = contract;
n_local = locals;
n_equs = eqs;
n_loc = loc;
n_params = params }
let mk_program o n t c =
{ p_modname = Modules.current.Modules.modname;
p_format_version = "";
p_opened = o;
p_nodes = n;
p_types = t;
p_consts = c }
let mk_exp desc loc = { e_desc = desc; e_loc = loc }
let mk_app params op = { a_op = op; a_params = params }
let void = mk_exp (Eapp (mk_app [] Minils.Etuple, [], None))
let mk_call params op exps reset =
Eapp (mk_app params op, exps, reset)
let mk_op_call ?(params=[]) s exps =
mk_call params (Minils.Efun { qual = "Pervasives"; name = s }) exps None
let mk_iterator_call it ln params reset n exps =
Eiterator (it, mk_app params (Minils.Enode ln), n, exps, reset)
let mk_constructor_exp f loc =
mk_exp (Econst (mk_static_exp (Sconstructor f))) loc
let mk_equation lhs rhs loc =
{ eq_lhs = lhs; eq_rhs = rhs; eq_loc = loc }
let mk_var_dec name ty clock loc =
{ v_name = name; v_type = ty; v_clock = clock; v_loc = loc }

View file

@ -168,7 +168,7 @@ struct
| _ -> ed
in ed, m
let node_dec_instance modname n params =
let node_dec_instance n params =
Idents.enter_node n.n_name;
let global_funs =
{ Global_mapfold.defaults with static_exp = static_exp } in
@ -189,12 +189,11 @@ struct
Modules.add_value ln node_sig;
{ n with n_name = ln; n_params = []; n_params_constraints = []; }
let node_dec modname n =
List.map (node_dec_instance modname n) (get_node_instances n.n_name)
let node_dec n =
List.map (node_dec_instance n) (get_node_instances n.n_name)
let program p =
{ p
with p_nodes = List.flatten (List.map (node_dec p.p_modname) p.p_nodes)}
{ p with p_nodes = List.flatten (List.map node_dec p.p_nodes) }
end
end
@ -219,7 +218,7 @@ let load_object_file modname =
let filename = Compiler_utils.findfile (name ^ ".epo") in
let ic = open_in_bin filename in
try
let p:program = input_value ic in
let (p : program) = input_value ic in
if p.p_format_version <> minils_format_version then (
Format.eprintf "The file %s was compiled with \
an older version of the compiler.@\n\

View file

@ -20,15 +20,6 @@ let optunit f = function
| None -> ()
| Some x -> f x
(** [split_string s c] splits the string [s] in a list of sub-strings according
to separator [c]. *)
let rec split_string s c =
try
let id = String.index s c in
let rest = String.sub s (id + 1) (String.length s - id - 1) in
String.sub s 0 id :: split_string rest c
with Not_found -> [s]
(** Print to a string *)
let print_pp_to_string print_fun element =
@ -201,3 +192,10 @@ let assert_2min = function
let assert_3 = function
| [v1; v2; v3] -> v1, v2, v3
| l -> _arity_error 3 l
let (|>) x f = f x
let split_string s separator = Str.split (separator |> Str.quote |> Str.regexp) s
let file_extension s = split_string s "." |> last_element

View file

@ -12,7 +12,9 @@ val optional : ('a -> 'b) -> 'a option -> 'b option
(** Optional with accumulator *)
val optional_wacc : ('a -> 'b -> 'c*'a) -> 'a -> 'b option -> ('c option * 'a)
val optunit : ('a -> unit) -> 'a option -> unit
val split_string : string -> char -> string list
(** [split_string s c] splits the string [s] according to the separator [c] into a list of string without [c] *)
val split_string : string -> string -> string list
(* Generation of unique names. Mandatory call of reset_symbol between
set_min_symbol and gen_symbol *)
@ -83,3 +85,8 @@ val print_pp_to_string : (Format.formatter -> 'a -> unit) -> 'a -> string
(** Replace all non [a-z A-Z 0-9] character of a string by [_] *)
val sanitize_string : string -> string
(** Pipe a value to a function *)
val (|>) : 'a -> ('a -> 'b) -> 'b
(** Return the extension of a filename string *)
val file_extension : string -> string