Commit 87ddbe68 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: a little bit more of syntax

parent f495d946
......@@ -48,6 +48,7 @@
"done", DONE;
"else", ELSE;
"end", END;
"ensures", ENSURES;
"exception", EXCEPTION;
"for", FOR;
"fun", FUN;
......@@ -63,6 +64,7 @@
"raises", RAISES;
"reads", READS;
"rec", REC;
"requires", REQUIRES;
"returns", RETURNS;
"then", THEN;
"try", TRY;
......
......@@ -67,7 +67,11 @@
let mk_prefix op e1 =
let id = { id = prefix op; id_loc = loc_i 1 } in
mk_expr (mk_apply_id id [e1])
let id_result () = { id = "result"; id_loc = loc () }
let lexpr_true () = { Ptree.pp_loc = loc (); Ptree.pp_desc = PPtrue }
let lexpr_false () = { Ptree.pp_loc = loc (); Ptree.pp_desc = PPfalse }
(* parsing LOGIC strings using functions from src/parser/
requires proper relocation *)
......@@ -98,9 +102,10 @@
/* keywords */
%token ABSURD AND AS ASSERT ASSUME BEGIN CHECK DO DONE ELSE END EXCEPTION FOR
%token ABSURD AND AS ASSERT ASSUME BEGIN CHECK DO DONE ELSE END ENSURES
%token EXCEPTION FOR
%token FUN GHOST IF IN INVARIANT LABEL LET MATCH NOT RAISE RAISES READS REC
%token RETURNS THEN TRY TYPE VARIANT VOID WHILE WITH WRITES
%token REQUIRES RETURNS THEN TRY TYPE VARIANT VOID WHILE WITH WRITES
/* symbols */
......@@ -175,6 +180,10 @@ decl:
{ Dlogic (logic_list0_decl $1) }
| LET lident EQUAL expr
{ Dcode ($2, $4) }
| LET lident list1_type_v_binder EQUAL triple
{ Dcode ($2, let p,e,q = $5 in mk_expr_i 3 (Efun ($3, p, e, q))) }
| LET REC lident list1_type_v_binder opt_variant EQUAL triple
{ Dcode ($3, let p,e,q = $7 in mk_expr_i 3 (Erec ($3, $4, $5, p, e, q))) }
;
lident:
......@@ -244,6 +253,14 @@ expr:
{ mk_expr (Elazy (LazyOr, $1, $3)) }
| LET lident EQUAL expr IN expr
{ mk_expr (Elet ($2, $4, $6)) }
| LET lident list1_type_v_binder EQUAL triple IN expr
{ let p,e,q = $5 in
mk_expr (Elet ($2, mk_expr_i 3 (Efun ($3, p, e, q)), $7)) }
| LET REC lident list1_type_v_binder opt_variant EQUAL triple IN expr
{ let p,e,q = $7 in
mk_expr (Elet ($3, mk_expr_i 3 (Erec ($3, $4, $5, p, e, q)), $9)) }
| FUN list1_type_v_binder ARROW triple
{ let p,e,q = $4 in mk_expr (Efun ($2, p, e, q)) }
| MATCH list1_expr_sep_comma WITH option_bar match_cases END
{ mk_expr (Ematch ($2, $5)) }
| GHOST expr
......@@ -258,6 +275,11 @@ expr:
{ mk_expr (Ecast ($1, $3)) }
;
triple:
| LOGIC expr LOGIC
{ lexpr $1, $2, lexpr $3 }
;
simple_expr:
| constant
{ mk_expr (Econstant $1) }
......@@ -359,6 +381,47 @@ list1_pure_type_sep_comma:
| pure_type COMMA list1_pure_type_sep_comma { $1 :: $3 }
;
type_v:
| pure_type
{ Tpure $1 }
;
list1_type_v_binder:
| type_v_binder { [$1] }
| type_v_binder list1_type_v_binder { $1 :: $2 }
;
type_v_binder:
| lident { $1, None }
| LEFTPAR lident COLON type_v RIGHTPAR { $2, Some $4 }
;
opt_colon_spec:
| /* epsilon */ { None }
| COLON type_c { Some $2 }
;
type_c:
| type_v
{ { pc_result_name = id_result ();
pc_result_type = $1;
pc_effect = [];
pc_pre = lexpr_true ();
pc_post = lexpr_true (); } }
| REQUIRES LOGIC RETURNS lident COLON type_v ENSURES LOGIC
{ { pc_result_name = $4;
pc_result_type = $6;
pc_effect = [];
pc_pre = lexpr $2;
pc_post = lexpr $8; } }
;
opt_variant:
| /* epsilon */ { None }
| VARIANT LOGIC { Some (lexpr $2) }
;
/***********************************************************************
ident_rich:
......
......@@ -38,18 +38,20 @@ type loop_annotation = {
loop_variant : lexpr option;
}
type effect = ident list
type type_v =
| Tpure of Ptree.pty
(* | Tarrow of (ident * type_v) list * type_c *)
| Tarrow of (ident * type_v option) list * type_c
(*
and type_c =
{ pc_result_name : Ident.t;
pc_result_type : ptype_v;
pc_effect : peffect;
pc_pre : assertion list;
pc_post : postcondition option }
*)
{ pc_result_name : ident;
pc_result_type : type_v;
pc_effect : effect;
pc_pre : lexpr;
pc_post : lexpr; }
type variant = lexpr
type expr = {
expr_desc : expr_desc;
......@@ -62,6 +64,9 @@ and expr_desc =
| Eident of qualid
| Eapply of expr * expr
| Elet of ident * expr * expr
| Efun of (ident * type_v option) list * lexpr * expr * lexpr
| Erec of ident *
(ident * type_v option) list * variant option * lexpr * expr * lexpr
(* control *)
| Esequence of expr * expr
| Eif of expr * expr * expr
......@@ -76,8 +81,7 @@ and expr_desc =
| Elabel of ident * expr
| Ecast of expr * Ptree.pty
(* TODO: fun, rec, raise, try, any, post?, match
(* TODO: raise, try, any, post?,
ghost *)
type decl =
......
......@@ -3,18 +3,29 @@
use import list.List
}
let rec mem (x:int) (l:int list) =
{ true }
match l with
| Nil -> True
| Cons (y, r) -> x = y || mem x r
end
{ true }
let p =
let x = ref 0 in
x := 1;
assert { !x = 1 };
label L:
assume { !x = 2 };
absurd : int list
absurd : int ref
let f (x : int) =
{ x >= 0 }
(fun y -> { y >= 0 } y+1 { result > y }) x
{ result > 0 }
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
compile-command: "unset LANG; make -C .. testl"
End:
*)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment