Skip to content
GitLab
Commit 13012033 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: more typing

parent b66d6145
Hide whitespace changes
Inline Side-by-side
src/programs/pgm_lexer.mll
View file @ 13012033
......@@ -48,7 +48,6 @@
"done", DONE;
"else", ELSE;
"end", END;
"ensures", ENSURES;
"exception", EXCEPTION;
"for", FOR;
"fun", FUN;
......@@ -60,12 +59,11 @@
"let", LET;
"match", MATCH;
"not", NOT;
"parameter", PARAMETER;
"raise", RAISE;
"raises", RAISES;
"reads", READS;
"rec", REC;
"requires", REQUIRES;
"returns", RETURNS;
"then", THEN;
"try", TRY;
"type", TYPE;
......
src/programs/pgm_parser.mly
View file @ 13012033
......@@ -69,6 +69,7 @@
mk_expr (mk_apply_id id [e1])
let id_result () = { id = "result"; id_loc = loc () }
let id_anonymous () = { id = "_"; 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 }
......@@ -102,10 +103,11 @@
/* keywords */
%token ABSURD AND AS ASSERT ASSUME BEGIN CHECK DO DONE ELSE END ENSURES
%token ABSURD AND AS ASSERT ASSUME BEGIN CHECK DO DONE ELSE END
%token EXCEPTION FOR
%token FUN GHOST IF IN INVARIANT LABEL LET MATCH NOT RAISE RAISES READS REC
%token REQUIRES RETURNS THEN TRY TYPE VARIANT VOID WHILE WITH WRITES
%token FUN GHOST IF IN INVARIANT LABEL LET MATCH NOT PARAMETER
%token RAISE RAISES READS REC
%token THEN TRY TYPE VARIANT VOID WHILE WITH WRITES
/* symbols */
......@@ -184,6 +186,8 @@ decl:
{ Dlet ($2, mk_expr_i 3 (Efun ($3, $5))) }
| LET REC list1_recfun_sep_and
{ Dletrec $3 }
| PARAMETER lident COLON type_v
{ Dparam ($2, $4) }
;
list1_recfun_sep_and:
......@@ -389,11 +393,6 @@ 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 }
......@@ -409,6 +408,22 @@ opt_colon_spec:
| COLON type_c { Some $2 }
;
type_v:
| simple_type_v
{ $1 }
| simple_type_v ARROW type_c
{ Tarrow ([id_anonymous (), Some $1], $3) }
| lident COLON simple_type_v ARROW type_c
{ Tarrow ([$1, Some $3], $5) }
;
simple_type_v:
| pure_type
{ Tpure $1 }
| LEFTPAR type_v RIGHTPAR
{ $2 }
;
type_c:
| type_v
{ { pc_result_name = id_result ();
......@@ -416,12 +431,12 @@ type_c:
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;
| LOGIC type_v LOGIC
{ { pc_result_name = id_result ();
pc_result_type = $2;
pc_effect = [];
pc_pre = lexpr $2;
pc_post = lexpr $8; } }
pc_pre = lexpr $1;
pc_post = lexpr $3; } }
;
opt_variant:
......@@ -430,420 +445,3 @@ opt_variant:
;
/***********************************************************************
ident_rich:
| uident { $1 }
| lident_rich { $1 }
;
lident_rich:
| lident
{ $1 }
| LEFTPAR UNDERSCORE lident_op UNDERSCORE RIGHTPAR
{ { id = infix $3; id_loc = loc () } }
| LEFTPAR lident_op UNDERSCORE RIGHTPAR
{ { id = prefix $2; id_loc = loc () } }
/*
| LEFTPAR UNDERSCORE lident_op RIGHTPAR
{ { id = postfix $3; id_loc = loc () } }
* /
;
lident_op:
| OP0 { $1 }
| OP2 { $1 }
| OP3 { $1 }
| EQUAL { "=" }
;
any_op:
| OP0 { $1 }
| OP2 { $1 }
| OP3 { $1 }
;
any_qualid:
| ident { Qident $1 }
| any_qualid DOT ident { Qdot ($1, $3) }
;
tqualid:
| uident { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }
qualid:
| ident_rich { Qident $1 }
| uqualid DOT ident_rich { Qdot ($1, $3) }
params:
| /* epsilon * / { [] }
| LEFTPAR list1_param_sep_comma RIGHTPAR { $2 }
;
param:
| primitive_type { None, $1 }
| lident COLON primitive_type { Some $1, $3 }
;
list1_param_sep_comma:
| param { [$1] }
| param COMMA list1_param_sep_comma { $1 :: $3 }
;
primitive_types:
| /* epsilon * / { [] }
| LEFTPAR list1_primitive_type_sep_comma RIGHTPAR { $2 }
logic_type_option:
| /* epsilon * / { None }
| COLON primitive_type { Some $2 }
;
type_var:
| QUOTE ident { $2 }
;
primitive_type:
| type_var
{ PPTtyvar $1 }
| lqualid
{ PPTtyapp ([], $1) }
| primitive_type lqualid
{ PPTtyapp ([$1], $2) }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR lqualid
{ PPTtyapp ($2 :: $4, $6) }
;
list1_primitive_type_sep_comma:
| primitive_type { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;
list0_ident_sep_comma:
| /* epsilon * / { [] }
| list1_ident_sep_comma { $1 }
;
list1_ident_sep_comma:
| ident { [$1] }
| ident COMMA list1_ident_sep_comma { $1 :: $3 }
;
decl:
| INCLUDE STRING
{ Include (loc_i 2,$2) }
| LET ident EQUAL expr
{ Program (loc_i 2,$2, $4) }
| LET ident binders EQUAL list0_bracket_assertion expr
{ Program (loc_i 2,$2, locate (Slam ($3, $5, force_function_post $6))) }
| LET REC recfun
{ let (loc,p) = $3 in Program (loc,rec_name p, locate p) }
| EXCEPTION ident
{ Exception (loc (), $2, None) }
| EXCEPTION ident OF primitive_type
{ Exception (loc (), $2, Some $4) }
| PARAMETER list1_ident_sep_comma COLON type_v
{ Parameter (loc_i 3, $2, $4) }
type_v:
| simple_type_v ARROW type_c
{ PVarrow ([Ident.anonymous, $1], $3) }
| ident COLON simple_type_v ARROW type_c
{ PVarrow ([($1, $3)], $5) }
| simple_type_v
{ $1 }
;
simple_type_v:
| primitive_type REF { PVref $1 }
| primitive_type { PVpure $1 }
| LEFTPAR type_v RIGHTPAR { $2 }
;
type_c:
| LEFTB opt_assertion RIGHTB result effects LEFTB opt_post_condition RIGHTB
{ let id,v = $4 in
{ pc_result_name = id; pc_result_type = v;
pc_effect = $5; pc_pre = list_of_some $2; pc_post = $7 } }
| type_v
{ ptype_c_of_v $1 }
;
result:
| RETURNS ident COLON type_v { $2, $4 }
| type_v { Ident.result, $1 }
;
effects:
| opt_reads opt_writes opt_raises
{ { pe_reads = $1; pe_writes = $2; pe_raises = $3 } }
;
opt_reads:
| /* epsilon * / { [] }
| READS list0_ident_sep_comma { $2 }
;
opt_writes:
| /* epsilon * / { [] }
| WRITES list0_ident_sep_comma { $2 }
;
opt_raises:
| /* epsilon * / { [] }
| RAISES list0_ident_sep_comma { $2 }
;
opt_assertion:
| /* epsilon * / { None }
| assertion { Some $1 }
;
assertion:
| lexpr
{ { pa_name = Anonymous; pa_value = $1; pa_loc = loc () } }
| lexpr AS ident
{ { pa_name = Name $3; pa_value = $1; pa_loc = loc () } }
;
opt_post_condition:
| /* epsilon * / { None }
| post_condition { Some $1 }
;
post_condition:
| assertion
{ $1, [] }
| assertion BAR list1_exn_condition_sep_bar
{ $1, $3 }
| BAR list1_exn_condition_sep_bar
{ Format.eprintf "%awarning: no postcondition; false inserted@\n"
Loc.report_position (loc ());
(* if Options.werror then exit 1; *)
({ pa_name = Anonymous; pa_value = mk_pp PPfalse; pa_loc = loc () }, $2) }
;
bracket_assertion:
| LEFTB assertion RIGHTB { $2 }
;
list1_bracket_assertion:
| bracket_assertion { [$1] }
| bracket_assertion list1_bracket_assertion { $1 :: $2 }
;
list0_bracket_assertion:
| /* epsilon * / { [] }
| LEFTB RIGHTB { [] }
| list1_bracket_assertion { $1 }
;
list1_exn_condition_sep_bar:
| exn_condition { [$1] }
| exn_condition BAR list1_exn_condition_sep_bar { $1 :: $3 }
;
exn_condition:
| ident BIGARROW assertion { $1,$3 }
;
expr:
| simple_expr %prec prec_simple
{ $1 }
| ident COLONEQUAL expr
{ locate
(Sapp (locate (Sapp (locate (Svar Ident.ref_set),
locate_i 1 (Svar $1))),
$3)) }
| ident LEFTSQ expr RIGHTSQ COLONEQUAL expr
{ locate
(Sapp (locate
(Sapp (locate
(Sapp (locate (Svar Ident.array_set),
locate_i 1 (Svar $1))),
$3)),
$6)) }
| IF expr THEN expr ELSE expr
{ locate (Sif ($2, $4, $6)) }
| IF expr THEN expr %prec prec_no_else
{ locate (Sif ($2, $4, locate (Sconst ConstUnit))) }
| WHILE expr DO invariant_variant expr DONE
{ (* syntactic suget for
try loop { invariant variant } if b then e else raise Exit
with Exit -> void end *)
let inv,var = $4 in
locate
(Stry
(locate
(Sloop (inv, var,
locate
(Sif ($2, $5,
locate (Sraise (exit_exn, None, None)))))),
[((exit_exn, None), locate (Sconst ConstUnit))])) }
| IDENT COLON expr
{ locate (Slabel ($1, $3)) }
| LET ident EQUAL expr IN expr
{ locate (Sletin ($2, $4, $6)) }
| LET ident EQUAL REF expr IN expr
{ locate (Sletref ($2, $5, $7)) }
| FUN binders ARROW list0_bracket_assertion expr %prec prec_fun
{ locate (Slam ($2, $4, force_function_post $5)) }
| LET ident binders EQUAL list0_bracket_assertion expr IN expr
{ let b = force_function_post ~warn:true $6 in
locate (Sletin ($2, locate (Slam ($3, $5, b)), $8)) }
| LET REC recfun %prec prec_letrec
{ let _loc,p = $3 in locate p }
| LET REC recfun IN expr
{ let _loc,p = $3 in locate (Sletin (rec_name p, locate p, $5)) }
| RAISE ident opt_cast
{ locate (Sraise ($2, None, $3)) }
| RAISE LEFTPAR ident expr RIGHTPAR opt_cast
{ locate (Sraise ($3, Some $4 , $6)) }
| TRY expr WITH bar_ list1_handler_sep_bar END
{ locate (Stry ($2, $5)) }
| ABSURD opt_cast
{ locate (Sabsurd $2) }
| simple_expr list1_simple_expr %prec prec_app
{ locate (app $1 $2) }
| expr BARBAR expr
{ locate (Slazy_or ($1, $3))
(* let ptrue = locate (Sconst (ConstBool true)) in
locate (Sif ($1, ptrue, $3)) *) }
| expr AMPAMP expr
{ locate (Slazy_and ($1, $3))
(* let pf = locate (Sconst (ConstBool false)) in
locate (Sif ($1, $3, pf)) *) }
| NOT expr
{ locate (Snot $2)
(* let pf = locate (Sconst (ConstBool false)) in
let pt = locate (Sconst (ConstBool true)) in
locate (Sif ($2, pf, pt)) *) }
| expr relation_id expr %prec prec_relation
{ bin_op $2 $1 $3 }
| expr PLUS expr
{ bin_op (loc_i 2, Ident.t_add) $1 $3 }
| expr MINUS expr
{ bin_op (loc_i 2, Ident.t_sub) $1 $3 }
| expr TIMES expr
{ bin_op (loc_i 2, Ident.t_mul) $1 $3 }
| expr SLASH expr
{ bin_op (loc_i 2, Ident.t_div) $1 $3 }
| expr PERCENT expr
{ bin_op (loc_i 2, Ident.t_mod_int) $1 $3 }
| MINUS expr %prec uminus
{ un_op (loc_i 1, Ident.t_neg) $2 }
| expr SEMICOLON expr
{ locate (Sseq ($1, $3)) }
| ASSERT list1_bracket_assertion SEMICOLON expr
{ locate (Sassert (`ASSERT,$2, $4)) }
| CHECK list1_bracket_assertion SEMICOLON expr
{ locate (Sassert (`CHECK,$2, $4)) }
| expr LEFTB post_condition RIGHTB
{ locate (Spost ($1, $3, Transparent)) }
| expr LEFTBLEFTB post_condition RIGHTBRIGHTB
{ locate (Spost ($1, $3, Opaque)) }
;
simple_expr:
| ident %prec prec_ident
{ locate (Svar $1) }
| INTEGER
{ locate (Sconst (ConstInt $1)) }
| FLOAT
{ let f = $1 in locate (Sconst (ConstFloat f)) }
| VOID
{ locate (Sconst ConstUnit) }
| TRUE
{ locate (Sconst (ConstBool true)) }
| FALSE
{ locate (Sconst (ConstBool false)) }
| BANG ident
{ locate (Sderef $2) }
| ident LEFTSQ expr RIGHTSQ
{ locate
(Sapp (locate (Sapp (locate (Svar Ident.array_get),
locate_i 1 (Svar $1))),
$3)) }
| LEFTSQ type_c RIGHTSQ
{ locate (Sany $2) }
| LEFTPAR expr RIGHTPAR
{ $2 }
| BEGIN expr END
{ $2 }
;
relation_id:
| LT { loc (), Ident.t_lt }
| LE { loc (), Ident.t_le }
| GT { loc (), Ident.t_gt }
| GE { loc (), Ident.t_ge }
| EQUAL { loc (), Ident.t_eq }
| NOTEQ { loc (), Ident.t_neq }
;
list1_simple_expr:
| simple_expr %prec prec_simple { [$1] }
| simple_expr list1_simple_expr { $1 :: $2 }
;
list1_handler_sep_bar:
| handler { [$1] }
| handler BAR list1_handler_sep_bar { $1 :: $3 }
;
handler:
| ident ARROW expr { (($1, None), $3) }
| ident ident ARROW expr { (($1, Some $2), $4) }
;
opt_cast:
| /* epsilon * / { None }
| COLON type_v { Some $2 }
;
invariant_variant:
| /* epsilon * / { None, None }
| LEFTB opt_invariant RIGHTB { $2, None }
| LEFTB opt_invariant VARIANT variant RIGHTB { $2, Some $4 }
;
opt_invariant:
| /* epsilon * / { None }
| INVARIANT assertion { Some $2 }
;
recfun:
| ident binders COLON type_v opt_variant EQUAL
list0_bracket_assertion expr %prec prec_recfun
{ (loc_i 1),Srec ($1, $2, $4, $5, $7, force_function_post $8) }
;
opt_variant:
| LEFTB VARIANT variant RIGHTB { Some $3 }
| /* epsilon * / { None }
;
variant:
| lexpr FOR ident { ($1, $3) }
| lexpr { ($1, Ident.t_zwf_zero) }
;
binders:
| list1_binder { List.flatten $1 }
;
list1_binder:
| binder { [$1] }
| binder list1_binder { $1 :: $2 }
;
binder:
| LEFTPAR RIGHTPAR
{ [Ident.anonymous, PVpure PPTunit] }
| LEFTPAR list1_ident_sep_comma COLON type_v RIGHTPAR
{ List.map (fun s -> (s, $4)) $2 }
;
*****/
src/programs/pgm_ptree.ml
View file @ 13012033
......@@ -42,7 +42,7 @@ type effect = ident list
type type_v =
| Tpure of Ptree.pty
| Tarrow of (ident * type_v option) list * type_c
| Tarrow of binder list * type_c
and type_c =
{ pc_result_name : ident;
......@@ -51,9 +51,9 @@ and type_c =
pc_pre : lexpr;
pc_post : lexpr; }
type variant = lexpr
and binder = ident * type_v option
type binder = ident * type_v option
type variant = lexpr
type expr = {
expr_desc : expr_desc;
......@@ -91,6 +91,7 @@ type decl =
| Dlet of ident * expr
| Dletrec of (ident * binder list * variant option * triple) list
| Dlogic of Ptree.decl list
| Dparam of ident * type_v
type file = decl list
src/programs/pgm_ttree.ml
View file @ 13012033
......@@ -31,22 +31,22 @@ type lazy_op = Pgm_ptree.lazy_op
type deffect = string list
type dlexpr = Typing.denv * Ptree.lexpr
type dtype_v =
| DTpure of Denv.dty
| DTarrow of (string * dtype_v) list * dtype_c
| DTarrow of dbinder list * dtype_c
and dtype_c =
{ dc_result_name : Term.vsymbol;
{ dc_result_name : string;
dc_result_type : dtype_v;
dc_effect : deffect;
dc_pre : Ptree.lexpr;
dc_post : Ptree.lexpr; }
type dvariant = Pgm_ptree.lexpr
dc_pre : dlexpr;
dc_post : dlexpr; }
type dbinder = string * dtype_v
and dbinder = string * dtype_v
type dlexpr = Typing.denv * Ptree.lexpr
type dvariant = Pgm_ptree.lexpr
type dexpr = {
dexpr_desc : dexpr_desc;
......@@ -85,16 +85,16 @@ type effect = Term.vsymbol list
type type_v =
| Tpure of Ty.ty
| Tarrow of Term.vsymbol list * type_c
| Tarrow of binder list * type_c
and type_c =
{ pc_result_name : Term.vsymbol;
pc_result_type : type_v;
pc_effect : effect;
pc_pre : Term.fmla;
pc_post : Term.fmla; }
{ c_result_name : Term.vsymbol;
c_result_type : type_v;
c_effect : effect;
c_pre : Term.fmla;
c_post : Term.fmla; }
type binder = Term.vsymbol * type_v
and binder = Term.vsymbol * type_v
type loop_annotation = {
loop_invariant : Term.fmla option;
......@@ -129,9 +129,9 @@ and expr_desc =