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

toujours plus de typage des programmes

parent fabc962d
......@@ -223,9 +223,9 @@ expr:
| assertion_kind LOGIC
{ mk_expr (Eassert ($1, lexpr $2)) }
| expr AMPAMP expr
{ mk_expr (Elazy_and ($1, $3)) }
{ mk_expr (Elazy (LazyAnd, $1, $3)) }
| expr BARBAR expr
{ mk_expr (Elazy_or ($1, $3)) }
{ mk_expr (Elazy (LazyOr, $1, $3)) }
| LET lident EQUAL expr IN expr
{ mk_expr (Elet ($2, $4, $6)) }
| GHOST expr
......
......@@ -29,6 +29,8 @@ type assertion_kind = Aassert | Aassume | Acheck
type lexpr = Ptree.lexpr
type lazy_op = LazyAnd | LazyOr
type loop_annotation = {
loop_invariant : lexpr option;
loop_variant : lexpr option;
......@@ -47,8 +49,7 @@ and expr_desc =
| Eif of expr * expr * expr
| Eskip
| Eassert of assertion_kind * lexpr
| Elazy_and of expr * expr
| Elazy_or of expr * expr
| Elazy of lazy_op * expr * expr
| Elet of ident * expr * expr
| Eghost of expr
| Elabel of ident * expr
......
......@@ -31,6 +31,8 @@ type lexpr = Ptree.lexpr
type loop_annotation = Pgm_ptree.loop_annotation
type lazy_op = Pgm_ptree.lazy_op
type expr = {
expr_desc : expr_desc;
expr_type : Denv.dty;
......@@ -46,8 +48,7 @@ and expr_desc =
| Eif of expr * expr * expr
| Eskip
| Eassert of assertion_kind * lexpr
| Elazy_and of expr * expr
| Elazy_or of expr * expr
| Elazy of lazy_op * expr * expr
| Elet of string * expr * expr
| Eghost of expr
| Elabel of ident * expr
......
......@@ -55,6 +55,7 @@ type denv = {
utyvars : (string, type_var) Hashtbl.t;
dvars : dty Mstr.t;
(* predefined symbols, from theory programs.Prelude *)
ts_bool : Ty.tysymbol;
ts_unit : Ty.tysymbol;
ts_arrow : Ty.tysymbol;
}
......@@ -64,6 +65,7 @@ let create_denv uc =
{ uc = uc;
utyvars = Hashtbl.create 17;
dvars = Mstr.empty;
ts_bool = ns_find_ts ns ["Prelude"; "bool"];
ts_unit = ns_find_ts ns ["Prelude"; "unit"];
ts_arrow = ns_find_ts ns ["Prelude"; "arrow"];
}
......@@ -123,14 +125,29 @@ and expr_desc env loc = function
let e1 = expr env e1 in
Elabel (l, e1), e1.expr_type
| Pgm_ptree.Eif (e1, e2, e3) ->
assert false (*TODO*)
| _ ->
assert false (*TODO*)
(* | Eassert of assertion_kind * lexpr *)
(* | Elazy_and of 'info expr * 'info expr *)
(* | Elazy_or of 'info expr * 'info expr *)
(* | Eghost of 'info expr *)
(* | Ewhile of 'info expr * loop_annotation * 'info expr *)
let e1 = expr env e1 in
expected_type e1 (Tyapp (env.ts_bool, []));
let e2 = expr env e2 in
let e3 = expr env e3 in
expected_type e3 e2.expr_type;
Eif (e1, e2, e3), e2.expr_type
| Pgm_ptree.Eassert (k, le) ->
Eassert (k, le), Tyapp (env.ts_unit, [])
| Pgm_ptree.Eghost e1 ->
let e1 = expr env e1 in
Eghost e1, e1.expr_type
| Pgm_ptree.Ewhile (e1, a, e2) ->
let e1 = expr env e1 in
expected_type e1 (Tyapp (env.ts_bool, []));
let e2 = expr env e2 in
expected_type e1 (Tyapp (env.ts_unit, []));
Ewhile (e1, a, e2), Tyapp (env.ts_unit, [])
| Pgm_ptree.Elazy (op, e1, e2) ->
let e1 = expr env e1 in
expected_type e1 (Tyapp (env.ts_bool, []));
let e2 = expr env e2 in
expected_type e2 (Tyapp (env.ts_bool, []));
Elazy (op, e1, e2), Tyapp (env.ts_bool, [])
let code uc id e =
let env = create_denv uc in
......
......@@ -11,7 +11,12 @@
let p =
let x = ref 1 in
begin ignore(1); ignore(3); 2 end
L:
begin
assert { !x = f(1) };
ignore (!x + f 1);
g 2
end
{
axiom A : forall x:int. f(x) = g(x-1)
......
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