diff --git a/src/programs/pgm_ttree.mli b/src/programs/pgm_ttree.mli index 474a7610a627f8e993e9984badedadde31e8b7d4..ecbdc9a41e62df915aa5398ded00df861a38e55e 100644 --- a/src/programs/pgm_ttree.mli +++ b/src/programs/pgm_ttree.mli @@ -48,7 +48,7 @@ and expr_desc = | Eassert of assertion_kind * lexpr | Elazy_and of expr * expr | Elazy_or of expr * expr - | Elet of ident * expr * expr + | Elet of string * expr * expr | Eghost of expr | Elabel of ident * expr | Ewhile of expr * loop_annotation * expr diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml index d90f7e68d0b28f17e8d2b449769f8a2cce1db06a..98f119e5a723226ea4af9ed53789318522f1e2b1 100644 --- a/src/programs/pgm_typing.ml +++ b/src/programs/pgm_typing.ml @@ -51,24 +51,34 @@ let report fmt = function (*** from Typing *************************************************************) type denv = { - uc : theory_uc; (* the theory under construction *) - utyvars : (string, type_var) Hashtbl.t; (* user type variables *) - dvars : dty Mstr.t; (* local variables, to be bound later *) + uc : theory_uc; + utyvars : (string, type_var) Hashtbl.t; + dvars : dty Mstr.t; + (* predefined symbols, from theory programs.Prelude *) + ts_unit : Ty.tysymbol; ts_arrow : Ty.tysymbol; } -let create_denv uc = { - uc = uc; - utyvars = Hashtbl.create 17; - dvars = Mstr.empty; - ts_arrow = ns_find_ts (get_namespace uc) ["Prelude"; "arrow"]; -} +let create_denv uc = + let ns = get_namespace uc in + { uc = uc; + utyvars = Hashtbl.create 17; + dvars = Mstr.empty; + ts_unit = ns_find_ts ns ["Prelude"; "unit"]; + ts_arrow = ns_find_ts ns ["Prelude"; "arrow"]; + } (*****************************************************************************) let currying env tyl ty = let make_arrow_type ty1 ty2 = Tyapp (env.ts_arrow, [ty1; ty2]) in List.fold_right make_arrow_type tyl ty +let expected_type e ty = + if not (Denv.unify e.expr_type ty) then + errorm ~loc:e.expr_loc + "this expression has type %a, but is expected to have type %a" + print_dty e.expr_type print_dty ty + let rec expr env e = let d, ty = expr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in { expr_desc = d; expr_type = ty; expr_loc = e.Pgm_ptree.expr_loc } @@ -90,27 +100,36 @@ and expr_desc env loc = function let e2 = expr env e2 in begin match e1.expr_type with | Tyapp (ts, [ty2; ty]) when ts == env.ts_arrow -> - if not (Denv.unify ty2 e2.expr_type) then - errorm ~loc:e2.expr_loc - "this expression has type %a, but is expected to have type %a" - print_dty e2.expr_type print_dty ty2; + expected_type e2 ty2; Eapply (e1, e2), ty | _ -> errorm ~loc:e1.expr_loc "this expression is not a function" end + | Pgm_ptree.Elet ({id=x}, e1, e2) -> + let e1 = expr env e1 in + let ty1 = e1.expr_type in + let env = { env with dvars = Mstr.add x ty1 env.dvars } in + let e2 = expr env e2 in + Elet (x, e1, e2), e2.expr_type + | Pgm_ptree.Esequence (e1, e2) -> + let e1 = expr env e1 in + expected_type e1 (Tyapp (env.ts_unit, [])); + let e2 = expr env e2 in + Esequence (e1, e2), e2.expr_type + | Pgm_ptree.Eskip -> + Eskip, Tyapp (env.ts_unit, []) + | Pgm_ptree.Elabel (l, e1) -> + (* TODO: add label to env *) + let e1 = expr env e1 in + Elabel (l, e1), e1.expr_type + | Pgm_ptree.Eif (e1, e2, e3) -> + assert false (*TODO*) | _ -> assert false (*TODO*) -(* | Eident of qualid *) -(* | Eapply of 'info expr * 'info expr *) -(* | Esequence of 'info expr * 'info expr *) -(* | Eif of 'info expr * 'info expr * 'info expr *) -(* | Eskip *) (* | Eassert of assertion_kind * lexpr *) (* | Elazy_and of 'info expr * 'info expr *) (* | Elazy_or of 'info expr * 'info expr *) -(* | Elet of ident * 'info expr * 'info expr *) (* | Eghost of 'info expr *) -(* | Elabel of ident * 'info expr *) (* | Ewhile of 'info expr * loop_annotation * 'info expr *) let code uc id e = diff --git a/src/programs/test.mlw b/src/programs/test.mlw index a49e45852bcc16b27a11ba914b7f1aab25e4ba70..ff52524cc6dd7ee65fadf6f27dc3ad2391d4f7f0 100644 --- a/src/programs/test.mlw +++ b/src/programs/test.mlw @@ -3,7 +3,6 @@ { use import programs.Prelude - use import int.Int type foo logic foo : foo logic f(int) : int @@ -11,9 +10,8 @@ } let p = - !(ref 1) - + - 2 + let x = ref 1 in + begin ignore(1); ignore(3); 2 end { axiom A : forall x:int. f(x) = g(x-1) diff --git a/theories/bool.why b/theories/bool.why index 1bfd0a2fc7b1ab29a2303a983a317457d2dfb11b..338624dae9940ac01ee489cff0e486abfc1ee3a5 100644 --- a/theories/bool.why +++ b/theories/bool.why @@ -1,5 +1,5 @@ -theory Base +theory Bool type bool = True | False @@ -32,7 +32,7 @@ end theory Ite - use import Base + use import Bool logic ite(b:bool, x:'a, y:'a) : 'a = match b with diff --git a/theories/programs.why b/theories/programs.why index 4ad8a9a1d201c18eaea528ca97f66302f14699c8..4ed8fb3385d35f0e2e0a0bd6fb2546eeb2c1fdae 100644 --- a/theories/programs.why +++ b/theories/programs.why @@ -1,11 +1,17 @@ theory Prelude + use export int.Int + use export bool.Bool + type ('a, 'b) arrow type 'a ref logic ref ('a) : 'a ref logic (!_)('a ref) : 'a + type unit + logic ignore('a) : unit + type label logic at ('a, label) : 'a logic old ('a) : 'a