Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

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

programs: typing effects

parent e98c76c5
{
use set.Fset as S
use array.Array as M
(* the graph *)
type vertex
logic v : vertex S.t
logic g_succ(vertex) : vertex S.t
axiom G_succ_sound :
forall x:vertex. S.subset(g_succ(x), v)
logic weight(vertex, vertex) : int (* edge weight, if there is an edge *)
axiom Weight_nonneg : forall x,y:vertex. weight(x,y) >= 0
}
parameter eq_vertex :
x:vertex -> y:vertex -> {} bool { if result=True then x=y else x<>y }
(* visited vertices *)
parameter visited : vertex S.t ref
parameter visited_add :
x:vertex -> {} unit writes visited { !visited = S.add(x, old(!visited)) }
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/dijkstra"
End:
*)
......@@ -184,6 +184,9 @@ rule token = parse
{ logic_start_loc := loc lexbuf;
let s = logic lexbuf in
LOGIC (fst !logic_start_loc, s) }
(* FIXME: allow newlines as well *)
| "{" space* "}"
{ LOGIC (lexeme_start_p lexbuf, "true") }
| "{{"
{ LEFTBLEFTB }
| "}}"
......@@ -224,7 +227,7 @@ and logic = parse
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. test"
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
......@@ -90,6 +90,8 @@
let lexpr (loc, s) = parse_string Lexer.parse_lexpr loc s
let empty_effect = { pe_reads = []; pe_writes = []; pe_raises = [] }
%}
/* Tokens */
......@@ -431,15 +433,35 @@ type_c:
| type_v
{ { pc_result_name = id_result ();
pc_result_type = $1;
pc_effect = [];
pc_effect = empty_effect;
pc_pre = lexpr_true ();
pc_post = lexpr_true (); } }
| LOGIC type_v LOGIC
| LOGIC type_v effects LOGIC
{ { pc_result_name = id_result ();
pc_result_type = $2;
pc_effect = [];
pc_effect = $3;
pc_pre = lexpr $1;
pc_post = lexpr $3; } }
pc_post = lexpr $4; } }
;
effects:
| opt_reads opt_writes opt_raises
{ { pe_reads = $1; pe_writes = $2; pe_raises = $3 } }
;
opt_reads:
| /* epsilon */ { [] }
| READS list0_lident_sep_comma { $2 }
;
opt_writes:
| /* epsilon */ { [] }
| WRITES list0_lident_sep_comma { $2 }
;
opt_raises:
| /* epsilon */ { [] }
| RAISES list0_uident_sep_comma { $2 }
;
opt_variant:
......@@ -447,4 +469,30 @@ opt_variant:
| VARIANT LOGIC { Some (lexpr $2) }
;
list0_lident_sep_comma:
| /* epsilon */ { [] }
| list1_lident_sep_comma { $1 }
;
list1_lident_sep_comma:
| lident { [$1] }
| lident COMMA list1_lident_sep_comma { $1 :: $3 }
;
list0_uident_sep_comma:
| /* epsilon */ { [] }
| list1_uident_sep_comma { $1 }
;
list1_uident_sep_comma:
| uident { [$1] }
| uident COMMA list1_uident_sep_comma { $1 :: $3 }
;
/*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*/
......@@ -38,7 +38,11 @@ type loop_annotation = {
loop_variant : lexpr option;
}
type effect = ident list
type effect = {
pe_reads : ident list;
pe_writes : ident list;
pe_raises : ident list;
}
type type_v =
| Tpure of Ptree.pty
......
......@@ -29,7 +29,15 @@ type lazy_op = Pgm_ptree.lazy_op
(* phase 1: destructive typing *)
type deffect = string list
type dreference =
| DRlocal of string
| DRglobal of Term.lsymbol
type deffect = {
de_reads : dreference list;
de_writes : dreference list;
de_raises : Term.lsymbol list;
}
type dlexpr = Typing.denv * Ptree.lexpr
......@@ -84,7 +92,15 @@ and dtriple = dlexpr * dexpr * dlexpr
type variant = Term.term
type effect = Term.vsymbol list
type reference =
| Rlocal of Term.vsymbol
| Rglobal of Term.lsymbol
type effect = {
e_reads : reference list;
e_writes : reference list;
e_raises : Term.lsymbol list;
}
type type_v =
| Tpure of Ty.ty
......
......@@ -59,6 +59,7 @@ let id_result = "result"
let dty_bool uc = Tyapp (ns_find_ts (get_namespace uc) ["bool"], [])
let dty_unit uc = Tyapp (ns_find_ts (get_namespace uc) ["unit"], [])
let dty_label uc = Tyapp (ns_find_ts (get_namespace uc) ["label"], [])
let ts_ref uc = ns_find_ts (get_namespace uc) ["ref"]
let ts_arrow uc = ns_find_ts (get_namespace uc) ["arrow"]
type denv = {
......@@ -103,6 +104,29 @@ let rec dpurify env = function
dcurrying env.uc (List.map (fun (_,ty) -> dpurify env ty) bl)
(dpurify env c.dc_result_type)
let check_reference _loc _ty =
() (*TODO*)
let dreference env id =
if Typing.mem_var id.id env.denv then
(* local variable *)
let ty = Typing.find_var id.id env.denv in
check_reference id.id_loc ty;
DRlocal id.id
else
let p = Qident id in
let s, _tyl, ty = Typing.specialize_fsymbol p env.uc in
check_reference id.id_loc ty;
DRglobal s
let dexception _env _id =
assert false (*TODO*)
let deffect env e =
{ de_reads = List.map (dreference env) e.Pgm_ptree.pe_reads;
de_writes = List.map (dreference env) e.Pgm_ptree.pe_writes;
de_raises = List.map (dexception env) e.Pgm_ptree.pe_raises; }
let rec dtype_v env = function
| Pgm_ptree.Tpure pt ->
DTpure (pure_type env pt)
......@@ -115,7 +139,7 @@ and dtype_c env c =
let ty = dtype_v env c.Pgm_ptree.pc_result_type in
{ dc_result_name = c.Pgm_ptree.pc_result_name.id;
dc_result_type = ty;
dc_effect = List.map (fun x -> x.id) c.Pgm_ptree.pc_effect;
dc_effect = deffect env c.Pgm_ptree.pc_effect;
dc_pre = env.denv, c.Pgm_ptree.pc_pre;
dc_post =
let denv = Typing.add_var id_result (dpurify env ty) env.denv in
......@@ -132,11 +156,11 @@ and dbinder env ({id=x; id_loc=loc}, v) =
env, (x, v)
let rec dexpr env e =
let d, ty = expr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
let d, ty = dexpr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
{ dexpr_desc = d; dexpr_loc = e.Pgm_ptree.expr_loc;
dexpr_denv = env.denv; dexpr_type = ty; }
and expr_desc env loc = function
and dexpr_desc env loc = function
| Pgm_ptree.Econstant (ConstInt _ as c) ->
DEconstant c, Tyapp (Ty.ts_int, [])
| Pgm_ptree.Econstant (ConstReal _ as c) ->
......@@ -152,7 +176,8 @@ and expr_desc env loc = function
let e1 = dexpr env e1 in
let e2 = dexpr env e2 in
let ty2 = create_type_var loc and ty = create_type_var loc in
if not (Denv.unify e1.dexpr_type (Tyapp (ts_arrow env.uc, [ty2; ty]))) then
if not (Denv.unify e1.dexpr_type (Tyapp (ts_arrow env.uc, [ty2; ty])))
then
errorm ~loc:e1.dexpr_loc "this expression is not a function";
expected_type e2 ty2;
DEapply (e1, e2), ty
......@@ -273,6 +298,15 @@ let purify uc = function
| Tarrow (bl, c) ->
currying uc (List.map (fun (v,_) -> v.vs_ty) bl) c.c_result_name.vs_ty
let reference _uc env = function
| DRlocal x -> Rlocal (Mstr.find x env)
| DRglobal ls -> Rglobal ls
let effect uc env e =
{ e_reads = List.map (reference uc env) e.de_reads;
e_writes = List.map (reference uc env) e.de_writes;
e_raises = e.de_raises; }
let rec type_v uc env = function
| DTpure ty ->
Tpure (Denv.ty_of_dty ty)
......@@ -286,7 +320,7 @@ and type_c uc env c =
let v = create_vsymbol (id_fresh c.dc_result_name) ty in
{ c_result_name = v;
c_result_type = tyv;
c_effect = []; (* TODO *)
c_effect = effect uc env c.dc_effect;
c_pre =
(let denv, l = c.dc_pre in Typing.type_fmla denv env l);
c_post =
......@@ -447,6 +481,6 @@ End:
TODO:
- mutually recursive functions: check variants are all present or all absent
- variant: check type int or relation order specified
- typing effects
- typing exceptions in effects (raises)
*)
......@@ -4,8 +4,6 @@ use import list.List
logic c : int
}
let id x = x
let test (n:int) =
let rec is_even (x:int) =
{true}
......
......@@ -7,7 +7,9 @@ theory Base
logic empty : 'a t
axiom Empty_def1 : forall x : 'a. not mem(x, empty)
logic is_empty(s : 'a t) = forall x : 'a. not mem(x, s)
axiom Empty_def1 : is_empty(empty : 'a t)
logic add('a, 'a t) : 'a t
......@@ -18,6 +20,12 @@ theory Base
logic add'(x:'a, s:'a t) : 'a t =
epsilon res:'a t. forall y:'a. mem(y, res) <-> (y = x or mem(y, s))
logic remove('a, 'a t) : 'a t
axiom Remove_def1 :
forall x, y : 'a. forall s : 'a t.
mem(x, remove(y, s)) <-> (x <> y and mem(x, s))
logic union('a t, 'a t) : 'a t
axiom Union_def1 :
......@@ -48,8 +56,22 @@ theory Fset
clone export Base
logic cardinal('a t) : int
axiom Cardinal_nonneg : forall s : 'a t. cardinal(s) >= 0
axiom Cardinal_empty : cardinal(empty : 'a t) = 0
(* TODO other axioms for cardinal *)
axiom Cardinal_add :
forall x : 'a. forall s : 'a t.
not mem(x, s) -> cardinal(add(x, s)) = 1 + cardinal(s)
axiom Cardinal_remove :
forall x : 'a. forall s : 'a t.
mem(x, s) -> cardinal(s) = 1 + cardinal(remove(x, s))
axiom Cardinal_subset :
forall s1, s2 : 'a t. subset(s1, s2) -> cardinal(s1) <= cardinal(s2)
end
theory Set
......
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