Commit 20dda6fc authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: typing (cont.)

parent ac0d8c83
......@@ -257,7 +257,10 @@ let specialize_pvsymbol pv =
let make_arrow_type tyl ty =
let arrow ty1 ty2 =
ts_app_real ts_arrow [ty1;ty2] in
(*
create (Dts (ts_arrow, [ty1; ty2])) (lazy (invalid_arg "ity_of_dity")) in
*)
List.fold_right arrow tyl ty
let specialize_vtarrow vta =
......
......@@ -207,40 +207,41 @@ and print_enode pri fmt e = match e.e_node with
| Earrow a ->
print_ps fmt a
| Eapp (e,v) ->
fprintf fmt "%a@ %a" (print_lexpr pri) e print_pv v
fprintf fmt "(%a@ %a)" (print_lexpr pri) e print_pv v
| Elet ({ let_var = lv ; let_expr = e1 }, e2) ->
let print_lv fmt = function
| LetV pv -> print_pvty fmt pv
| LetA ps -> print_psty fmt ps in
let forget_lv = function
| LetV pv -> forget_pv pv
| LetA ps -> forget_ps ps in
fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
print_lv lv (print_lexpr 4) e1 print_expr e2;
forget_lv lv
| Erec (rdl,e) ->
let print_and fmt () = fprintf fmt "@\nand@\n" in
let print_post fmt post =
let vs,f = open_post post in
fprintf fmt "%a ->@ %a" print_vs vs print_term f in
let print_rd fmt { rec_ps = ps ; rec_lambda = lam } =
fprintf fmt "(%a) %a =@ { %a }@ %a@ { %a }"
print_psty ps
(print_list space print_pvty) lam.l_args
print_term lam.l_pre
print_expr lam.l_expr
print_post lam.l_post
in
let forget_rd rd = forget_ps rd.rec_ps in
fprintf fmt (protect_on (pri > 0) "@[<hov 4>let rec %a@]@ in@ %a")
(print_list print_and print_rd) rdl print_expr e;
List.iter forget_rd rdl
| 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
(*
| Tlet (t1,tb) ->
let v,t2 = t_open_bound tb in
fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
print_vs v (print_lterm 4) t1 print_term t2;
forget_var v
| Tcase (v,bl) ->
fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
print_expr v (print_list newline print_branch) bl
| Teps fb ->
let v,f = t_open_bound fb in
fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
print_vsty v print_term f;
forget_var v
| Tquant (q,fq) ->
let vl,tl,f = t_open_quant fq in
fprintf fmt (protect_on (pri > 0) "@[<hov 1>%a %a%a.@ %a@]") print_quant q
(print_list comma print_vsty) vl print_tl tl print_term f;
List.iter forget_var vl
| Ttrue ->
fprintf fmt "true"
| Tfalse ->
fprintf fmt "false"
| Tbinop (b,f1,f2) ->
let asym = Slab.mem Term.asym_label f1.t_label in
let p = prio_binop b in
fprintf fmt (protect_on (pri > p) "@[<hov 1>%a %a@ %a@]")
(print_lterm (p + 1)) f1 (print_binop ~asym) b (print_lterm p) f2
| Tnot f ->
fprintf fmt (protect_on (pri > 4) "not %a") (print_lterm 4) f
*)
| _ ->
fprintf fmt "<expr TODO>"
......
......@@ -134,27 +134,6 @@ let rec extract_labels labs loc e = match e.Ptree.expr_desc with
labs, loc, Ptree.Ecast ({ e with Ptree.expr_desc = d }, ty)
| e -> List.rev labs, loc, e
let unify_args args dity =
let a = create_type_variable () in
let dity' = make_arrow_type (List.map (fun a -> a.dexpr_type) args) a in
unify dity dity';
a
(*
let unify_args_prg ~loc prg args el = match prg with
| PV { pv_vs = vs } ->
errorm ~loc "%s: not a function" vs.vs_name.id_string
| PL pl ->
unify_args pl.pl_ls args el; []
| PA { pa_name = id } | PS { ps_name = id } ->
let rec unify_list = function
| a :: args, e :: el -> unify_arg a e; unify_list (args, el)
| args, [] -> args
| [], _ :: _ -> errorm ~loc "too many arguments for %s" id.id_string
in
unify_list (args, el)
*)
let rec decompose_app args e = match e.Ptree.expr_desc with
| Eapply (e1, e2) -> decompose_app (e2 :: args) e1
| _ -> e, args
......@@ -201,7 +180,9 @@ and dexpr_desc ~userloc denv loc = function
let e, el = decompose_app [e2] e1 in
let e = dexpr ~userloc denv e in
let el = List.map (dexpr ~userloc denv) el in
let res = unify_args el e.dexpr_type in
let res = create_type_variable () in
let dity = make_arrow_type (List.map (fun a -> a.dexpr_type) el) res in
unify e.dexpr_type dity;
DEapply (e, el), res
| Ptree.Elet (id, e1, e2) ->
let e1 = dexpr ~userloc denv e1 in
......@@ -221,7 +202,7 @@ and dexpr_desc ~userloc denv loc = function
let tvars = add_tvars denv.tvars dity in
let denv = { denv with
locals = Mstr.add id.id (tvars, dity) denv.locals;
tvars = tvars }
tvars = tvars }
in
denv, (id, false, dity)
in
......@@ -262,7 +243,7 @@ let rec expr locals de = match de.dexpr_desc with
let e2 = expr locals de2 in
e_rec [def1] e2
| DEfun (bl, tr) ->
let x = { id = "fun"; id_loc = de.dexpr_loc; id_lab = [] } in
let x = { id = "fn"; id_loc = de.dexpr_loc; id_lab = [] } in
let def = expr_fun locals x bl tr in
let e2 = e_cast def.rec_ps (VTarrow def.rec_ps.ps_vta) in
e_rec [def] e2
......@@ -273,20 +254,21 @@ let rec expr locals de = match de.dexpr_desc with
let e2 = expr locals de2 in
e_let def1 e2
| DEapply (de1, del) ->
let e1 = expr locals de1 in
let el = List.map (expr locals) del in
begin match de1.dexpr_desc with
| DEglobal_pl pls -> e_plapp pls el (ity_of_dity de.dexpr_type)
| DEglobal_ls ls -> e_lapp ls el (ity_of_dity de.dexpr_type)
| _ -> e_app e1 el
| _ -> e_app (expr locals de1) el
end
| DEglobal_pv pv ->
e_value pv
| DEglobal_ps ps ->
e_cast ps (vty_of_dity de.dexpr_type)
| DEglobal_pl pls ->
e_plapp pls [] (ity_of_dity de.dexpr_type)
| DEglobal_pl pl ->
assert (pl.pl_ls.ls_args = []);
e_plapp pl [] (ity_of_dity de.dexpr_type)
| DEglobal_ls ls ->
assert (ls.ls_args = []);
e_lapp ls [] (ity_of_dity de.dexpr_type)
| _ ->
assert false (*TODO*)
......
......@@ -21,7 +21,7 @@ module N
type ref 'a = {| ghost mutable contents : 'a |}
let f x = x + x
let f x = x.contents + 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