diff --git a/src/ast.ml b/src/ast.ml index 2179b24..fcf814c 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -47,6 +47,7 @@ type t_expression = | ETriOp of full_ty * triop * t_expression * t_expression * t_expression | EComp of full_ty * compop * t_expression * t_expression | EWhen of full_ty * t_expression * t_expression + | EReset of full_ty * t_expression * t_expression | EConst of full_ty * const | ETuple of full_ty * (t_expression list) | EApp of full_ty * t_node * t_expression diff --git a/src/lexer.mll b/src/lexer.mll index 3a4175c..4b28de5 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -30,6 +30,7 @@ ("else", ELSE); ("merge", TO_merge); ("when", WHEN); + ("reset", RESET); ("pre", MO_pre); ("true", CONST_BOOL(true)); ("false", CONST_BOOL(false)); diff --git a/src/parser.mly b/src/parser.mly index 8dba723..e116564 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -35,6 +35,7 @@ | ETriOp (full_ty , _ , _ , _ , _) -> full_ty | EComp (full_ty , _ , _ , _) -> full_ty | EWhen (full_ty , _ , _) -> full_ty + | EReset (full_ty , _ , _) -> full_ty | EConst (full_ty , _) -> full_ty | ETuple (full_ty , _) -> full_ty | EApp (full_ty , _ , _) -> full_ty @@ -160,6 +161,7 @@ %token TO_merge %token WHEN +%token RESET %token IF %token THEN @@ -359,6 +361,13 @@ expr: then EWhen (type_exp $1, $1, $3) else raise (MyParsingError ("The when does not type-check!", current_location())) } + | expr RESET expr + { let e1 = $1 in let t1 = type_exp e1 in + let e2 = $3 in let t2 = type_exp e2 in + if t2 = FTBase TBool + then EReset (type_exp $1, $1, $3) + else raise (MyParsingError ("The reset does not type-check!", + current_location())) } /* Constants */ | CONST_INT { EConst (FTBase TInt, CInt $1) } | CONST_BOOL { EConst (FTBase TBool, CBool $1) } diff --git a/src/pp.ml b/src/pp.ml index a08bfa3..c807e28 100644 --- a/src/pp.ml +++ b/src/pp.ml @@ -40,6 +40,13 @@ let pp_expression = (pp_expression_aux (upd_prefix prefix)) e1 (pp_expression_aux (upd_prefix prefix)) e2 end + | EReset (_, e1, e2) -> + begin + Format.fprintf fmt "\t\t\t%sRESET\n%a\t\t\tRESET\n%a" + prefix + (pp_expression_aux (upd_prefix prefix)) e1 + (pp_expression_aux (upd_prefix prefix)) e2 + end | EConst (_, c) -> begin match c with | CBool true -> Format.fprintf fmt "\t\t\t%s\n" prefix