From 31a04721defeaca6d80a062d757b12b72a901ead Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ce=CC=81dric=20Pasteur?= Date: Wed, 16 Jun 2010 14:17:14 +0200 Subject: [PATCH] Updated lexer and parser --- global/signature.ml | 3 + heptagon/heptagon.ml | 24 +++---- heptagon/parsing/lexer.mll | 4 -- heptagon/parsing/parser.mly | 117 ++++++++++++++-------------------- heptagon/parsing/parsetree.ml | 96 ++++++++++++++++------------ heptagon/parsing/scoping.ml | 4 +- 6 files changed, 119 insertions(+), 129 deletions(-) diff --git a/global/signature.ml b/global/signature.ml index a82091e..fa8b7af 100644 --- a/global/signature.ml +++ b/global/signature.ml @@ -36,3 +36,6 @@ let names_of_arg_list l = List.map (fun ad -> ad.a_name) l let types_of_arg_list l = List.map (fun ad -> ad.a_type) l +let mk_arg name ty = + { a_type = ty; a_name = name } + diff --git a/heptagon/heptagon.ml b/heptagon/heptagon.ml index 182015d..8fae310 100644 --- a/heptagon/heptagon.ml +++ b/heptagon/heptagon.ml @@ -43,9 +43,10 @@ type exp = | Earrow | Eifthenelse | Earray_op of array_op + | Efield_update of longname | Ecall of op_desc * exp option (** [op_desc] is the function called [exp option] is the optional reset condition *) - + and array_op = | Erepeat | Eselect of size_exp list @@ -148,25 +149,20 @@ type interface = and interface_desc = | Iopen of name | Itypedef of type_dec | Isignature of signature - -let edesc e = e.e_desc - -let eqdesc eq = eq.eq_desc - + (* Helper functions to create AST. *) (*TODO refactor en mk_*) -let emake desc ty = - { e_desc = desc; e_ty = ty; e_linearity = NotLinear; e_loc = no_location; } +let mk_exp desc ty = + { e_desc = desc; e_ty = ty; e_loc = no_location; } -let eop op = { a_op = op; a_inlined = Ino; } +let mk_op op = { a_op = op; } -let tmake name desc = { t_name = name; t_desc = desc; t_loc = no_location; } +let mk_type_dec name desc = + { t_name = name; t_desc = desc; t_loc = no_location; } -let eqmake desc = +let mk_equation desc = { eq_desc = desc; eq_statefull = true; eq_loc = no_location; } - -let tybool = Tbase tbool - + let cfalse = Cconstr pfalse let ctrue = Cconstr ptrue diff --git a/heptagon/parsing/lexer.mll b/heptagon/parsing/lexer.mll index a1d6c55..3e0251f 100644 --- a/heptagon/parsing/lexer.mll +++ b/heptagon/parsing/lexer.mll @@ -62,14 +62,10 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "enforce", ENFORCE; "with", WITH; "inlined", INLINED; - "at", AT; "with", WITH; "map", MAP; "fold", FOLD; "mapfold", MAPFOLD; - "copy", COPY; - "flatten", FLATTEN; - "make", MAKE; "quo", INFIX3("quo"); "mod", INFIX3("mod"); "land", INFIX3("land"); diff --git a/heptagon/parsing/parser.mly b/heptagon/parsing/parser.mly index 9c04a1d..0fe28ff 100644 --- a/heptagon/parsing/parser.mly +++ b/heptagon/parsing/parser.mly @@ -1,5 +1,4 @@ %{ -(* $Id$ *) open Misc open Global @@ -20,7 +19,7 @@ open Parsetree %token CHAR %token STRING %token PRAGMA -%token TYPE FUN NODE RETURNS VAR VAL UNSAFE IN OPEN SAFE END CONST +%token TYPE FUN NODE RETURNS VAR VAL IN OPEN END CONST %token FBY PRE SWITCH WHEN EVERY %token OR STAR NOT %token AMPERSAND @@ -46,7 +45,6 @@ open Parsetree %token ENFORCE %token WITH %token INLINED -%token AT %token POWER %token LBRACKET %token RBRACKET @@ -62,8 +60,6 @@ open Parsetree %token INFIX3 %token INFIX4 %token EOF -%token COPY -%token FLATTEN MAKE %right AROBASE %left WITH @@ -153,7 +149,7 @@ label_ty_list: ; label_ty: - IDENT COLON ty_ident { ($1, fst $3) } + IDENT COLON ty_ident { ($1, $3) } ; node_decs: @@ -181,11 +177,6 @@ node_or_fun: | FUN { false } ; -safe: - | /* empty */ { false } - | SAFE { true } -; - in_params: | params {$1} ; @@ -236,7 +227,7 @@ opt_equs: ; opt_assume: - | /* empty */ { e_true () } + | /* empty */ { mk_exp (Econst (Cconstr Initial.ptrue)) } | ASSUME exp { $2 } ; @@ -274,16 +265,9 @@ ident_list: ; ty_ident: - | ty_ident_base - { $1, NotLinear } - | ty_ident_base AT ident - { $1, At $3 } -; - -ty_ident_base: | IDENT { Tid(Name($1)) } - | ty_ident_base POWER simple_exp + | ty_ident POWER simple_exp { Tarray ($1, $3) } ; @@ -409,93 +393,86 @@ exps: ; simple_exp: - | IDENT { emake (Evar $1) } - | const { emake (Econst $1) } + | IDENT { mk_exp (Evar $1) } + | const { mk_exp (Econst $1) } | LBRACE field_exp_list RBRACE - { emake (Estruct($2)) } + { mk_exp (Estruct $2) } | LBRACKET array_exp_list RBRACKET - { emake (Earray $2) } + { mk_exp (Earray $2) } | LPAREN tuple_exp RPAREN - { emake (Etuple $2) } + { mk_exp (Etuple $2) } | LPAREN exp RPAREN { $2 } ; node_name: | longname call_params - { Enode($1, $2) } + { $1, $2, Enode } exp: | simple_exp { $1 } | simple_exp FBY exp - { emake (Eapp(eop (Efby), [$1; $3])) } + { mk_exp (Eapp(mk_app Efby, [$1; $3])) } | PRE exp - { emake (Eapp(eop (Epre(None)), [$2])) } + { mk_exp (Eapp(mk_app (Epre None), [$2])) } | node_name LPAREN exps RPAREN %prec prec_apply - { emake (Eapp(eop $1, $3)) } - | INLINED node_name LPAREN exps RPAREN %prec prec_apply - { emake (Eapp(eop_inlined $2, $4)) } + { mk_exp (mk_call $1 $3) } | NOT exp - { emake (Eapp(eop (Eop(Name("not"),[])), [$2])) } + { mk_exp (mk_op_call "not" [] [$2]) } | exp INFIX4 exp - { emake (Eapp(eop (Eop(Name($2),[])), [$1; $3])) } + { mk_exp (mk_op_call $2 [] [$1; $3]) } | exp INFIX3 exp - { emake (Eapp(eop (Eop(Name($2),[])), [$1; $3])) } + { mk_exp (mk_op_call $2 [] [$1; $3]) } | exp INFIX2 exp - { emake (Eapp(eop (Eop(Name($2),[])), [$1; $3])) } + { mk_exp (mk_op_call $2 [] [$1; $3]) } | exp INFIX1 exp - { emake (Eapp(eop (Eop(Name($2),[])), [$1; $3])) } + { mk_exp (mk_op_call $2 [] [$1; $3]) } | exp INFIX0 exp - { emake (Eapp(eop (Eop(Name($2),[])), [$1; $3])) } + { mk_exp (mk_op_call $2 [] [$1; $3]) } | exp EQUAL exp - { emake (Eapp(eop (Eop(Name("="),[])), [$1; $3])) } + { mk_exp (mk_op_call "=" [] [$1; $3]) } | exp OR exp - { emake (Eapp(eop (Eop(Name("or"),[])), [$1; $3])) } + { mk_exp (mk_op_call "or" [] [$1; $3]) } | exp STAR exp - { emake (Eapp(eop (Eop(Name("*"),[])), [$1; $3])) } + { mk_exp (mk_op_call "*" [] [$1; $3]) } | exp AMPERSAND exp - { emake (Eapp(eop (Eop(Name("&"),[])), [$1; $3])) } + { mk_exp (mk_op_call "&" [] [$1; $3]) } | exp SUBTRACTIVE exp - { emake (Eapp(eop (Eop(Name($2),[])), [$1; $3])) } + { mk_exp (mk_op_call $2 [] [$1; $3]) } | PREFIX exp - { emake (Eapp(eop (Eop(Name($1),[])), [$2])) } + { mk_exp (mk_op_call $1 [] [$2]) } | SUBTRACTIVE exp %prec prec_uminus - { emake (Eapp(eop (Eop(Name("~" ^ $1),[])), [$2])) } + { mk_exp (mk_op_call ("~"^$1) [] [$2]) } | IF exp THEN exp ELSE exp - { emake (Eapp(eop Eifthenelse, [$2; $4; $6])) } + { mk_exp (Eapp(mk_app Eifthenelse [$2; $4; $6])) } | simple_exp ARROW exp - { emake (Eapp(eop Earrow, [$1; $3])) } + { mk_exp (Eapp(mk_app Earrow, [$1; $3])) } | LAST IDENT - { emake (Elast($2)) } - | exp DOT longname { emake (Efield($1, $3)) } + { mk_exp (Elast $2) } + | exp DOT longname + { mk_exp (Efield ($1, $3)) } /*Array operations*/ | exp POWER simple_exp - { emake (Eapp(eop (Erepeat), [$1; $3])) } + { mk_exp (mk_array_op_call Erepeat [$1; $3]) } | exp indexes - { emake (Eapp(eop (Eselect $2), [$1])) } + { mk_exp (mk_array_op_call (Eselect $2) [$1]) } | exp DOT indexes DEFAULT exp - { emake (Eapp(eop (Eselect_dyn), [$1; $5]@$3)) } + { mk_exp (mk_array_op_call Eselect_dyn [$1; $5]@$3) } | exp WITH indexes EQUAL exp - { emake (Eapp(eop (Eupdate $3), [$1; $5])) } + { mk_exp (mk_array_op_call (Eupdate $3) [$1; $5]) } | exp LBRACKET exp DOUBLE_DOT exp RBRACKET - { emake (Eapp(eop Eselect_slice, [$1; $3; $5])) } + { mk_exp (mk_array_op_call Eselect_slice [$1; $3; $5]) } | exp AROBASE exp - { emake (Eapp(eop Econcat, [$1; $3])) } + { mk_exp (mk_array_op_call Econcat [$1; $3]) } /*Iterators*/ | iterator longname DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN %prec prec_apply - { emake (Eapp(eop (Eiterator ($1, $2, [])), $4::$7)) } + { mk_exp (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 %prec prec_apply - { emake (Eapp(eop (Eiterator ($1, $3, $5)), $9::$12)) } - | COPY LPAREN exp RPAREN %prec prec_apply - { emake (Eapp(eop Ecopy, [$3])) } + { mk_exp (mk_iterator_call $1 $3 $5 ($9::$12)) } /*Records operators */ | exp WITH DOT longname EQUAL exp - { emake (Eapp(eop (Efield_update $4), [$1; $6])) } - | LPAREN FLATTEN longname RPAREN LPAREN exps RPAREN - { emake (Eapp(eop (Eflatten $3), $6)) } - | LPAREN MAKE longname RPAREN LPAREN exps RPAREN - { emake (Eapp(eop (Emake $3), $6)) } + { mk_exp (Eapp (mk_app (Efield_update $4), [$1; $6])) } ; call_params: @@ -581,12 +558,12 @@ interface_decls: ; interface_decl: - | type_dec { imake (Itypedef($1)) } - | OPEN Constructor { imake (Iopen($2)) } - | VAL safe node_or_fun ident node_params LPAREN params_signature RPAREN + | type_dec { mk_interface_decl (Itypedef $1) } + | OPEN Constructor { mk_interface_decl (Iopen $2) } + | VAL node_or_fun ident node_params LPAREN params_signature RPAREN RETURNS LPAREN params_signature RPAREN - { imake (Isignature({ sig_name = $4; sig_inputs = $7; sig_outputs = $11; - sig_node = $3; sig_safe = $2; sig_params = $5; })) } + { mk_interface_decl (Isignature({ sig_name = $4; sig_inputs = $6; sig_outputs = $10; + sig_node = $3; sig_params = $4; })) } ; params_signature: @@ -600,8 +577,8 @@ nonmt_params_signature: ; param_signature: - | IDENT COLON ty_ident { (Some($1), $3) } - | ty_ident { (None, $1) } + | IDENT COLON ty_ident { Signature.mk_arg (Some $1) $3) } + | ty_ident { Signature.mk_arg None $1 } ; %% diff --git a/heptagon/parsing/parsetree.ml b/heptagon/parsing/parsetree.ml index d1c2d77..959e5ca 100644 --- a/heptagon/parsing/parsetree.ml +++ b/heptagon/parsing/parsetree.ml @@ -7,17 +7,15 @@ (* *) (**************************************************************************) (* the internal representation *) -(* $Id$ *) -open Location open Names -open Linearity -open Misc +open Location +open Signature -type inlining_policy = - | Ino - | Ione - | Irec +type iterator_type = + | Imap + | Ifold + | Imapfold type ty = | Tprod of ty list @@ -39,21 +37,24 @@ and desc = | Earray of exp list and app = - { a_op : op; (* change of global name after typing *) - a_inlined : inlining_policy; (* node to inline or not *) - } + { a_op : op; } and op = | Epre of const option - | Efby | Earrow | Eifthenelse | Enode of longname * exp list - | Eevery of longname * exp list | Eop of longname * exp list + | Efby | Earrow | Eifthenelse + | Earray_op of array_op + | Efield_update of longname + | Ecall of op_desc + +and array_op = | Erepeat | Eselect of exp list | Eselect_dyn | Eupdate of exp list | Eselect_slice - | Econcat | Ecopy - | Eiterator of iterator_name * longname * exp list - | Efield_update of longname - | Eflatten of longname | Emake of longname + | Econcat + | Eiterator of iterator_type * op_desc + +and op_desc = longname * exp list * op_kind +and op_kind = | Eop | Enode and const = | Cint of int @@ -102,7 +103,6 @@ and present_handler = and var_dec = { v_name : name; v_type : ty; - v_linearity : linearity; v_last : last; v_loc : location; } @@ -116,7 +116,7 @@ type type_dec = and type_desc = | Type_abs | Type_enum of name list - | Type_struct of (name * ty) list + | Type_struct of structure type contract = { c_assume : exp; @@ -152,8 +152,8 @@ type program = type signature = { sig_name : name; - sig_inputs : (name option * (ty * linearity)) list; - sig_outputs : (name option * (ty * linearity)) list; + sig_inputs : arg list; + sig_outputs : arg list; sig_node : bool; sig_safe : bool; sig_params : name list; } @@ -170,26 +170,42 @@ and interface_desc = | Isignature of signature (* Helper functions to create AST. *) -let emake desc = - { e_desc = desc; e_loc = get_current_location () } -let e_true () = - emake (Econst(Cconstr(Modname{ qual="Pervasives"; id="true"}))) -let eop op = { a_op = op; a_inlined = Ino } -let eop_inlined op = { a_op = op; a_inlined = Ione } -let tmake name desc = - { t_name = name; t_desc = desc; t_loc = get_current_location () } -let eqmake desc = - { eq_desc = desc; eq_loc = get_current_location () } -let imake desc = - { interf_desc = desc; interf_loc = get_current_location () } -let vmake name (ty, linearity) last = - { v_name = name; v_type = ty; v_linearity = linearity; - v_last = last; v_loc = get_current_location () } +let mk_exp desc = + { e_desc = desc; e_loc = Location.get_current_location () } -let bmake locals eqs = +let mk_app op = + { a_op = op; } + +let mk_call desc exps = + Eapp (mk_app (Ecall desc), exps) + +let mk_op_call s params exps = + mk_call (Name s, params, Eop) exps + +let mk_array_op_call op exps = + Eapp (mk_app (Earray_op op), exps) + +let mk_iterator_call it ln params exps = + mk_array_op_call (Eiterator (it, (ln, params, Enode))) exps + +let mk_type_dec name desc = + { t_name = name; t_desc = desc; t_loc = Location.get_current_location () } + +let mk_equation desc = + { eq_desc = desc; eq_loc = Location.get_current_location () } + +let mk_interface_decl desc = + { interf_desc = desc; interf_loc = Location.get_current_location () } + +let mk_var_dec name ty last = + { v_name = name; v_type = ty; + v_last = last; v_loc = Location.get_current_location () } + +let mk_block locals eqs = { b_local = locals; b_equs = eqs; - b_loc = get_current_location () } + b_loc = Location.get_current_location () } -let cmake id (ty,_) e = +let mk_const_dec id ty e = { c_name = id; c_type = ty; c_value = e; - c_loc = get_current_location (); } + c_loc = Location.get_current_location (); } + diff --git a/heptagon/parsing/scoping.ml b/heptagon/parsing/scoping.ml index 758e5c6..9309e10 100644 --- a/heptagon/parsing/scoping.ml +++ b/heptagon/parsing/scoping.ml @@ -224,8 +224,10 @@ and translate_block const_env env b = Heptagon.b_loc = b.b_loc } and translate_state_handler const_env env sh = + let b = translate_block const_env env sh.s_block in + let env = build_vd_list env sh.s_block.b_local in { Heptagon.s_state = sh.s_state; - Heptagon.s_block = translate_block const_env env sh.s_block; + Heptagon.s_block = b; Heptagon.s_until = List.map (translate_escape const_env env) sh.s_until; Heptagon.s_unless = List.map (translate_escape const_env env) sh.s_unless; }