From 15448fdff93fb87243c871244e2ba6424ef39b2a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Le=CC=81onard=20Ge=CC=81rard?= Date: Tue, 17 Aug 2010 15:04:16 +0200 Subject: [PATCH] mlsc and mls_parsetree etc. --- compiler/main/mls2obc.ml | 1 - compiler/minils/main/mls_compiler.ml | 9 +- compiler/minils/main/mlsc.ml | 9 +- compiler/minils/minils.ml | 12 ++- compiler/minils/parsing/mls_lexer.mll | 53 +++++----- compiler/minils/parsing/mls_parser.mly | 49 ++++++--- compiler/minils/parsing/mls_parsetree.ml | 122 +++++++++++------------ compiler/utilities/pp_tools.ml | 39 ++------ 8 files changed, 149 insertions(+), 145 deletions(-) diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index e37ef22..d5e1d82 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -365,7 +365,6 @@ and mk_node_call map call_context app loc name_list args = | Minils.Efun _ -> [] | Minils.Enode _ -> [reinit o]) in [], si, [obj], [Acall (name_list, o, Mstep, args)] - | _ -> assert false and translate_iterator map call_context it name_list app loc n x c_list = diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml index 33b1563..1522d96 100644 --- a/compiler/minils/main/mls_compiler.ml +++ b/compiler/minils/main/mls_compiler.ml @@ -12,9 +12,10 @@ open Compiler_utils let pp p = if !verbose then Mls_printer.print stdout p -let parse parsing_fun lexing_fun lexbuf = +let parse prog_name parsing_fun lexing_fun lexbuf = try - parsing_fun lexing_fun lexbuf + let p = parsing_fun lexing_fun lexbuf in + { p with p_modname = prog_name } with | Mls_lexer.Lexical_error(err, loc) -> lexical_error err loc @@ -24,8 +25,8 @@ let parse parsing_fun lexing_fun lexbuf = let l = Loc(pos1,pos2) in syntax_error l -let parse_implementation lexbuf = - parse Mls_parser.program Mls_lexer.token lexbuf +let parse_implementation prog_name lexbuf = + parse prog_name Mls_parser.program Mls_lexer.token lexbuf let compile pp p = (* Clocking *) diff --git a/compiler/minils/main/mlsc.ml b/compiler/minils/main/mlsc.ml index 8c3bd47..cd1159f 100644 --- a/compiler/minils/main/mlsc.ml +++ b/compiler/minils/main/mlsc.ml @@ -14,7 +14,6 @@ open Mls2seq let compile_impl modname filename = - (* input and output files *) (* input and output files *) let source_name = filename ^ ".mls" and mls_norm_name = filename ^ "_norm.mls" @@ -37,10 +36,12 @@ let compile_impl modname filename = let pp = Mls_compiler.pp in (* Parsing of the file *) - let p = Mls_compiler.parse_implementation lexbuf in + let p = + do_silent_pass Mls_compiler.parse_implementation "Parsing" lexbuf true in let p = { p with Minils.p_modname = modname } in - comment "Parsing"; - pp p; + + (* Convert Parse tree to Minils AST *) + let p = Mls_scoping.translate_program "Scoping" p pp true in (* Process the MiniLS AST *) let p = Mls_compiler.compile pp p in diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 5c3753c..dbc2697 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -79,6 +79,8 @@ and op = | Eselect_dyn (** arg1.[arg3...] default arg2 *) | Eupdate (** [ arg1 with arg3..arg_n = arg2 ] *) | Econcat (** arg1@@arg2 *) +(* +*) type pat = | Etuplepat of pat list @@ -150,11 +152,19 @@ let mk_node n_params = param; n_params_constraints = constraints } -let mk_type_dec ?(type_desc = Type_abs) ?(loc = no_location) name = +let mk_type_dec type_desc name loc = { t_name = name; t_desc = type_desc; t_loc = loc } +let mk_const_dec id ty e loc = + { c_name = id; c_type = ty; c_value = e; c_loc = loc } + let mk_app ?(params=[]) ?(unsafe=false) op = { a_op = op; a_params = params; a_unsafe = unsafe } +(** The modname field has to be set when known, TODO LG : format_version *) +let mk_program o n t c = + { p_modname = ""; p_format_version = ""; + p_opened = o; p_nodes = n; p_types = t; p_consts = c } + let void = mk_exp (Eapp (mk_app Etuple, [], None)) diff --git a/compiler/minils/parsing/mls_lexer.mll b/compiler/minils/parsing/mls_lexer.mll index 333eaf5..5be00a5 100644 --- a/compiler/minils/parsing/mls_lexer.mll +++ b/compiler/minils/parsing/mls_lexer.mll @@ -51,7 +51,8 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "lxor", INFIX2("lxor"); "lsl", INFIX4("lsl"); "lsr", INFIX4("lsr"); - "asr", INFIX4("asr") + "asr", INFIX4("asr"); + "on", ON; ] @@ -111,31 +112,33 @@ let newline = '\n' | '\r' '\n' rule token = parse | newline { new_line lexbuf; token lexbuf } | [' ' '\t'] + { token lexbuf } - | "." {DOT} - | ".." {DOTDOT} - | "(" {LPAREN} - | ")" {RPAREN} + | "." { DOT } + | ".." { DOTDOt } + | "(" { LPAREN } + | ")" { RPAREN } | "*" { STAR } - | "{" {LBRACE} - | "}" {RBRACE} - | "[" {LBRACKET} - | "]" {RBRACKET} - | ":" {COLON} - | ";" {SEMICOL} - | "=" {EQUAL} - | "==" {EQUALEQUAL} - | "&" {AMPERSAND} - | "&&" {AMPERAMPER} - | "||" {BARBAR} - | "," {COMMA} - | "->" {ARROW} - | "|" {BAR} - | "-" {SUBTRACTIVE "-"} - | "-." {SUBTRACTIVE "-."} - | "^" {POWER} - | "@" {AROBASE} - | "<<" {DOUBLE_LESS} - | ">>" {DOUBLE_GREATER} + | "{" { 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) diff --git a/compiler/minils/parsing/mls_parser.mly b/compiler/minils/parsing/mls_parser.mly index 05b5b67..036cb0b 100644 --- a/compiler/minils/parsing/mls_parser.mly +++ b/compiler/minils/parsing/mls_parser.mly @@ -4,8 +4,10 @@ open Signature open Names open Idents open Types +open Clocks open Location open Minils +open Mls_parsetree open Mls_utils @@ -32,6 +34,7 @@ open Mls_utils %token AROBASE %token WITH %token DOTDOT +%token BASE UNDERSCORE ON COLONCOLON %token DEFAULT %token LBRACKET RBRACKET %token MAP FOLD MAPFOLD @@ -61,7 +64,7 @@ open Mls_utils %start program -%type program +%type program %% @@ -84,7 +87,7 @@ 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 t n c } + { mk_program o n t c } open_modules: l=list(opens) {l} opens: OPEN c=CONSTRUCTOR {c} @@ -104,11 +107,11 @@ type_ident: NAME { Tid(Name($1)) } type_decs: t=list(type_dec) {t} type_dec: | TYPE n=NAME - { mk_type_dec ~loc:(Loc ($startpos,$endpos)) ~type_desc:Type_abs n } + { mk_type_dec Type_abs n (Loc ($startpos,$endpos)) } | TYPE n=NAME EQUAL e=snlist(BAR,NAME) - { mk_type_dec ~loc:(Loc ($startpos,$endpos)) ~type_desc:(Type_enum e) n } + { mk_type_dec (Type_enum e) n (Loc ($startpos,$endpos)) } | TYPE n=NAME EQUAL s=structure(field_type) - { mk_type_dec ~loc:(Loc ($startpos,$endpos)) ~type_desc:(Type_struct s) n } + { mk_type_dec (Type_struct s) n (Loc ($startpos,$endpos)) } node_decs: ns=list(node_dec) {ns} node_dec: @@ -130,15 +133,30 @@ loc_vars_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) } + +ct: + | LPAREN ctl=snlist(STAR,ct) RPAREN { Cprod ctl } + | c=ck { Ck c } + +clock_annot: + | /*empty*/ { Cbase } + | COLONCOLON c=ck { c } + var: - | ns=snlist(COMMA, NAME) COLON t=type_ident - { List.map (fun id -> mk_var_dec (ident_of_name id) t) ns } + | 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 } equs: LET e=slist(SEMICOL, equ) TEL { e } -equ: p=pat EQUAL e=exp { mk_equation ~loc:(Loc ($startpos,$endpos)) p e } +equ: p=pat EQUAL e=exp { mk_equation p e (Loc ($startpos,$endpos)) } pat: - | n=NAME {Evarpat (ident_of_name n)} + | n=NAME {Evarpat n} | LPAREN p=snlist(COMMA, pat) RPAREN {Etuplepat p} longname: l=qualified(name) {l} /* qualified var (not a constructor) */ @@ -147,11 +165,10 @@ constructor: /* of type longname */ | ln=qualified(CONSTRUCTOR) { ln } | b=BOOL { Name(if b then "true" else "false") } -/* TODO donner un type !! Phase de typing. */ field: | ln=longname { mk_static_exp ~loc:(Loc($startpos,$endpos)) (Sconstructor ln)} -/* TODO donner un type !! Phase de typing. */ + const : c=_const { mk_static_exp ~loc:(Loc ($startpos,$endpos)) c } _const: | i=INT { Sint i } @@ -164,7 +181,7 @@ exps: LPAREN e=slist(COMMA, exp) RPAREN {e} field_exp: longname EQUAL exp { ($1, $3) } simple_exp: - | e=_simple_exp {mk_exp e ~loc:(Loc ($startpos,$endpos)) } + | e=_simple_exp {mk_exp e (Loc ($startpos,$endpos)) } _simple_exp: | n=NAME { Evar (ident_of_name n) } | s=structure(field_exp) { Estruct s } @@ -175,7 +192,7 @@ _simple_exp: exp: | e=simple_exp { e } - | e=_exp { mk_exp e ~loc:(Loc ($startpos,$endpos)) } + | e=_exp { mk_exp e (Loc ($startpos,$endpos)) } _exp: | c=const { Econst c } | v=const FBY e=exp { Efby(Some(v), e) } @@ -196,7 +213,7 @@ _exp: | e=exp POWER p=e_param { Eapp(mk_app ~params:[p] Earray_fill, [e], None) } | e=simple_exp i=indexes(exp) /* not e_params to solve conflicts */ - { Eapp(mk_app ~params:(List.map static_exp_of_exp i) Eselect, [e], None) } + { Eapp(mk_app ~params:i Eselect, [e], None) } | e=simple_exp i=indexes(exp) DEFAULT d=exp { Eapp(mk_app Eselect_dyn, [e; d]@i, None) } | LPAREN e=exp WITH i=indexes(e_param) EQUAL nv=exp @@ -228,10 +245,10 @@ iterator: reset: r=option(RESET,ident) { r } /* TODO : Scoping to deal with node and fun ! */ -funapp: ln=longname p=params(e_param) { mk_app ~params:p (Enode ln) } +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 { static_exp_of_exp e } +%inline e_param: e=exp { e } n_param: n=NAME { mk_param n } params(param): | /*empty*/ { [] } diff --git a/compiler/minils/parsing/mls_parsetree.ml b/compiler/minils/parsing/mls_parsetree.ml index 5aef1a1..ffaad1f 100644 --- a/compiler/minils/parsing/mls_parsetree.ml +++ b/compiler/minils/parsing/mls_parsetree.ml @@ -7,111 +7,107 @@ (* *) (**************************************************************************) - -open Names open Location +open Names open Signature +open Static open Types -open Minils +open Clocks -type exp = - { e_desc: desc; - e_loc: location } +type exp = { + e_desc: edesc; + e_loc: location } -and desc = +and app = { a_op: Minils.op; a_params: exp list } + +and edesc = | Econst of static_exp | Evar of name - | Efby of static_exp option * exp - | Eapp of app * exp list * name option + | Efby of exp option * exp + | Eapp of Minils.app * exp list * name option | Ewhen of exp * constructor_name * name | Emerge of name * (constructor_name * exp) list | Estruct of (field_name * exp) list - | Eiterator of iterator_type * app * static_exp * exp list * name option - + | Eiterator of + Minils.iterator_type * app * exp * exp list * name option and pat = | Etuplepat of pat list | Evarpat of name -type eq = { +and eq = { eq_lhs : pat; eq_rhs : exp; eq_loc : location } and var_dec = { - v_name : name; + v_ident : name; v_type : ty; v_clock : ck; - v_loc : location; } - - -type contract = { - c_assume : exp; - c_enforce : exp; - c_eq : eq list } + v_loc : location } type node_dec = { - n_name : name; - n_statefull : bool; - 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; } + n_name : name; + n_input : var_dec list; + n_output : var_dec list; + n_contract : Minils.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 : type_dec list; + p_types : Minils.type_dec list; p_nodes : node_dec list; - p_consts : const_dec list } + p_consts : Minils.const_dec list } -(* Helper functions to create AST. *) -let mk_exp desc loc = - { e_desc = desc; e_loc = loc } +(** {Helper functions to build the Parsetree *) -let mk_app op params = - { a_op = op; a_params = params } +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 } -let mk_call ?(params=[]) op exps = - Eapp (mk_app op params, exps) +(** The modname field has to be set when known, TODO LG : format_version *) +let mk_program o n t c = + { p_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 (Minils.mk_app Minils.Etuple, [], None)) + +let mk_call ?(unsafe=false) ?(params=[]) reset op exps = + Eapp (Minils.mk_app ~unsafe:unsafe op ~params:params, exps, reset) let mk_op_call ?(params=[]) s exps = - mk_call ~params:params - (Efun (Modname { qual = "Pervasives"; id = s })) exps + mk_call ~params:params None + (Minils.Efun (Modname { qual = "Pervasives"; id = s })) exps -let mk_iterator_call it ln params n exps = - Eiterator (it, mk_app (Enode ln) params, n, exps) +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_type_dec name desc loc = - { t_name = name; t_desc = desc; t_loc = loc } +let mk_equation lhs rhs loc = + { eq_lhs = lhs; eq_rhs = rhs; eq_loc = loc } -let mk_equation desc loc = - { eq_desc = desc; eq_loc = loc } +let mk_var_dec name ty clock loc = + { v_ident = name; v_type = ty; v_clock = clock; v_loc = loc } -let mk_interface_decl desc loc = - { interf_desc = desc; interf_loc = loc } - -let mk_var_dec name ty last loc = - { v_name = name; v_type = ty; - v_last = last; v_loc = loc } - -let mk_block locals eqs loc = - { b_local = locals; b_equs = eqs; - b_loc = loc } - -let mk_const_dec id ty e loc = - { c_name = id; c_type = ty; c_value = e; - c_loc = loc } - -let mk_arg name ty = - { a_type = ty; a_name = name } diff --git a/compiler/utilities/pp_tools.ml b/compiler/utilities/pp_tools.ml index a82bf82..f4d7293 100644 --- a/compiler/utilities/pp_tools.ml +++ b/compiler/utilities/pp_tools.ml @@ -56,35 +56,12 @@ let print_type_params ff pl = print_list_r (fun ff s -> fprintf ff "'%s" s) "("","") " ff pl -(* Map and Set redefinition to allow pretty printing +let print_set print_element ff set = + fprintf ff "@[{@ "; + iter (fun e -> fprintf ff "%a@ " print_element e) set; + fprintf ff "}@]" - module type P = sig - type t - val fprint : Format.formatter -> t -> unit - end - - module type ELT = sig - type t - val compare : t -> t -> int - val fprint : Format.formatter -> t -> unit - end - - module SetMake (Elt : ELT) = struct - module M = Set.Make(Elt) - include M - let fprint ff es = - Format.fprintf ff "@[{@ "; - iter (fun e -> Format.fprintf ff "%a@ " Elt.fprint e) es; - Format.fprintf ff "}@]"; - end - - module MapMake (Key : ELT) (Elt : P) = struct - module M = Map.Make(Key) - include M - let fprint prp eem = - Format.fprintf prp "[@["; - iter (fun k m -> - Format.fprintf prp "@ | %a -> %a" Key.fprint k Elt.fprint m) eem; - Format.fprintf prp "@]@ ]"; - end -*) +let print_map print_key print_element ff map = + pfrintf ff "@[[@ "; + iter (fun k x -> fprintf ff "| %a -> %a@ " print_key k print_element x map; + fprintf ff "]@]"