Commit 92ad3c64 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: typing assignments

parent ad1413a1
......@@ -96,7 +96,7 @@ and dexpr_desc =
| DEfun of dubinder list * dtriple
| DElet of ident * dexpr * dexpr
| DEletrec of drecfun list * dexpr
| DEassign of dexpr * Term.lsymbol * int * dexpr
| DEassign of dexpr * dexpr
| DEsequence of dexpr * dexpr
| DEif of dexpr * dexpr * dexpr
| DEloop of dloop_annotation * dexpr
......
......@@ -238,6 +238,9 @@ and print_enode pri fmt e = match e.e_node with
| Eif (v,e1,e2) ->
fprintf fmt (protect_on (pri > 0) "if %a then %a@ else %a")
print_pv v print_expr e1 print_expr e2
| Eassign (pv1,r,pv2) ->
fprintf fmt (protect_on (pri > 0) "%a <%a> <- %a")
print_pv pv1 print_regty r print_pv pv2
(*
| Tcase (v,bl) ->
fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
......
......@@ -344,12 +344,17 @@ and dexpr_desc ~userloc denv loc = function
in
let res = dexpr_app (hidden_pl ~loc cs) (List.map get_val pjl) in
mk_let ~loc ~userloc e1 res
| Ptree.Eassign (e1, q, e2) ->
let fl = { expr_desc = Eident q ; expr_loc = loc } in
let e1 = { expr_desc = Eapply (fl,e1) ; expr_loc = loc } in
let e1 = dexpr ~userloc denv e1 in
let e2 = dexpr ~userloc denv e2 in
expected_type e2 e1.dexpr_type;
DEassign (e1, e2), dity_unit
| Ptree.Econstant _c ->
assert false (*TODO*)
| Ptree.Eletrec (_rdl, _e1) ->
assert false (*TODO*)
| Ptree.Eassign (_e1, _q, _e2) ->
assert false (*TODO*)
| Ptree.Eloop (_ann, _e1) ->
assert false (*TODO*)
| Ptree.Elazy (_lazy_op, _e1, _e2) ->
......@@ -427,6 +432,8 @@ let rec expr locals de = match de.dexpr_desc with
e_lapp ls [] (ity_of_dity de.dexpr_type)
| DEif (de1, de2, de3) ->
e_if (expr locals de1) (expr locals de2) (expr locals de3)
| DEassign (de1, de2) ->
e_assign (expr locals de1) (expr locals de2)
| _ ->
assert false (*TODO*)
......
......@@ -29,7 +29,9 @@ module N
let bang y = y.contents in
let z = bang x + zero in
let u = {| f1 = z; f2 = Node x Nil |} in
{| contents = {| u with f2 = Node one Nil |} |}
let r = {| contents = {| u with f2 = Node one Nil |} |} in
x.contents <- one;
r (* zero *)
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