Updated lexer and parser
This commit is contained in:
Cédric Pasteur
Cédric Pasteur
parent
dc3d564b70
commit
31a04721de
|
|
@ -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 }
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
|
|
|
|||
|
|
@ -1,5 +1,4 @@
|
|||
%{
|
||||
(* $Id$ *)
|
||||
|
||||
open Misc
|
||||
open Global
|
||||
|
|
@ -20,7 +19,7 @@ open Parsetree
|
|||
%token <char> CHAR
|
||||
%token <string> STRING
|
||||
%token <string * string> 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 <string> INFIX3
|
||||
%token <string> 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 }
|
||||
;
|
||||
|
||||
%%
|
||||
|
|
|
|||
|
|
@ -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 (); }
|
||||
|
||||
|
|
|
|||
|
|
@ -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; }
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue