WhyML: typing

parent 4e5cdd39
......@@ -161,7 +161,7 @@ end
let exit_exn () = Qident (mk_id "%Exit" (floc ()))
let id_anonymous () = mk_id "_" (floc ())
let ty_unit () = Tpure (PPTtuple [])
let ty_unit () = PPTtuple []
let id_lt_nat () = Qident (mk_id "lt_nat" (floc ()))
......@@ -1318,7 +1318,7 @@ type_v_binder:
type_v_param:
| LEFTPAR RIGHTPAR
{ [id_anonymous (), Some (ty_unit ())] }
| LEFTPAR lidents_lab COLON type_v RIGHTPAR
| LEFTPAR lidents_lab COLON primitive_type RIGHTPAR
{ List.map (fun i -> (i, Some $4)) $2 }
;
......@@ -1334,9 +1334,9 @@ type_v:
;
arrow_type_v:
| simple_type_v ARROW type_c
| primitive_type ARROW type_c
{ Tarrow ([id_anonymous (), Some $1], $3) }
| lident labels COLON simple_type_v ARROW type_c
| lident labels COLON primitive_type ARROW type_c
{ Tarrow ([add_lab $1 $2, Some $4], $6) }
/* TODO: we could alllow lidents instead, e.g. x y : int -> ... */
/*{ Tarrow (List.map (fun x -> x, Some $3) $1, $5) }*/
......
......@@ -196,6 +196,8 @@ type pre = lexpr
type post = lexpr * (qualid * lexpr) list
type binder = ident * pty option
type type_v =
| Tpure of pty
| Tarrow of binder list * type_c
......@@ -206,8 +208,6 @@ and type_c =
pc_pre : pre;
pc_post : post; }
and binder = ident * type_v option
type expr = {
expr_desc : expr_desc;
expr_loc : loc;
......
......@@ -63,7 +63,7 @@ and dutype_c =
duc_pre : Ptree.lexpr;
duc_post : Ptree.lexpr * (Term.lsymbol * Ptree.lexpr) list; }
and dubinder = ident * Denv.dty * dutype_v
and dubinder = ident * Denv.dty
type dvariant = Ptree.lexpr * Term.lsymbol option
......@@ -154,7 +154,7 @@ and itype_c =
ic_pre : T.pre;
ic_post : T.post; }
and ibinder = ivsymbol * itype_v
and ibinder = ivsymbol * ty
type mark = Term.vsymbol
......
......@@ -266,7 +266,7 @@ let rec dpurify_utype_v = function
| DUTpure ty ->
ty
| DUTarrow (bl, c) ->
dcurrying (List.map (fun (_,ty,_) -> ty) bl)
dcurrying (List.map (fun (_,ty) -> ty) bl)
(dpurify_utype_v c.duc_result_type)
(* user indicates whether region type variables can be instantiated *)
......@@ -307,12 +307,11 @@ and dutype_c env c =
}
and dubinder env ({id=x; id_loc=loc} as id, v) =
let v = match v with
| Some v -> dutype_v env v
| None -> DUTpure (create_type_var loc)
let ty = match v with
| Some v -> dtype ~user:true env v
| None -> create_type_var loc
in
let ty = dpurify_utype_v v in
add_local env x ty, (id, ty, v)
add_local env x ty, (id, ty)
let rec add_local_pat env p = match p.dp_node with
| Denv.Pwild -> env
......@@ -475,7 +474,7 @@ and dexpr_desc ~ghost ~userloc env loc = function
| Ptree.Efun (bl, t) ->
let env, bl = map_fold_left dubinder env bl in
let (_,e,_) as t = dtriple ~ghost ~userloc env t in
let tyl = List.map (fun (_,ty,_) -> ty) bl in
let tyl = List.map (fun (_,ty) -> ty) bl in
let ty = dcurrying tyl e.dexpr_type in
DEfun (bl, t), ty
| Ptree.Elet (x, e1, e2) ->
......@@ -730,7 +729,7 @@ and dletrec ~ghost ~userloc env dl =
let env, bl = map_fold_left dubinder env bl in
let v = option_map (dvariant env) v in
let (_,e,_) as t = dtriple ~ghost ~userloc env t in
let tyl = List.map (fun (_,ty,_) -> ty) bl in
let tyl = List.map (fun (_,ty) -> ty) bl in
let ty = dcurrying tyl e.dexpr_type in
if not (Denv.unify ty tyres) then
errorm ~loc:id.id_loc
......@@ -1026,12 +1025,11 @@ and iutype_c env c =
ic_pre = ifmla env c.duc_pre;
ic_post = iupost env ty c.duc_post; }
and iubinder env (x, ty, tyv) =
let tyv = iutype_v env tyv in
and iubinder env (x, ty) =
let ty = Denv.ty_of_dty ty in
let label, _ = label_set_from_list x.id_loc x.id_lab in
let env, v = iadd_local env (id_user ~label x.id x.id_loc) ty in
env, (v, tyv)
env, (v, ty)
let mk_iexpr loc ty d =
{ iexpr_desc = d; iexpr_loc = loc; iexpr_lab = []; iexpr_type = ty }
......@@ -1502,8 +1500,8 @@ and type_c env c =
and add_binders env bl =
map_fold_left add_binder env bl
and add_binder env (i, v) =
let v = type_v env v in
and add_binder env (i, ty) =
let v = tpure ty in
let env, vs = add_local env i v in
env, vs
......
......@@ -90,9 +90,9 @@ and dexpr_desc =
| DElocal of string
| DEglobal_pv of pvsymbol
| DEglobal_ps of psymbol
| DEglobal_pl of plsymbol * dexpr list
| DElogic of Term.lsymbol * dexpr list
| DEapply of dexpr * dexpr
| DEglobal_pl of plsymbol
| DEglobal_ls of Term.lsymbol
| DEapply of dexpr * dexpr list
| DEfun of dubinder list * dtriple
| DElet of ident * dexpr * dexpr
| DEletrec of drecfun list * dexpr
......
......@@ -74,14 +74,6 @@ let create_dreg ~user dity =
ref { rid = unique (); rity = dity; ruser = user;
reg = lazy (create_region (id_fresh "rho") (ity_of_dity dity)) }
let find_type_variable htv tv =
try
Htv.find htv tv
with Not_found ->
let dtv = create_type_variable () in
Htv.add htv tv dtv;
dtv
let ts_app_real ts dl =
create (Dts (ts, dl)) (lazy (ity_pur ts (List.map ity_of_dity dl)))
......@@ -178,32 +170,10 @@ let unify d1 d2 =
try unify d1 d2
with Exit -> raise (TypeMismatch (ity_of_dity d1, ity_of_dity d2))
let rec dity_of_ity ~user htv hreg ity = match ity.ity_node with
| Ityvar tv -> assert (not user); find_type_variable htv tv
| Itypur (ts, ityl) -> ts_app ts (List.map (dity_of_ity ~user htv hreg) ityl)
| Ityapp (its, ityl, rl) ->
its_app_real its (List.map (dity_of_ity ~user htv hreg) ityl)
(List.map (dreg_of_reg ~user htv hreg) rl)
and dreg_of_reg ~user htv hreg r =
try
Hreg.find hreg r
with Not_found ->
let dreg = create_dreg ~user (dity_of_ity ~user htv hreg r.reg_ity) in
Hreg.add hreg r dreg;
dreg
let dity_of_vtv ~user htv hreg v = dity_of_ity ~user htv hreg v.vtv_ity
let ts_arrow =
let v = List.map (fun s -> create_tvsymbol (Ident.id_fresh s)) ["a"; "b"] in
Ty.create_tysymbol (Ident.id_fresh "arrow") v None
let make_arrow_type tyl ty =
let arrow ty1 ty2 =
create (Dts (ts_arrow, [ty1; ty2])) (lazy (invalid_arg "ity_of_dity")) in
List.fold_right arrow tyl ty
let rec vty_of_dity dity = match !dity.node with
| Dts (ts, [d1; d2]) when ts_equal ts ts_arrow ->
VTarrow (vty_arrow (vty_value (ity_of_dity d1)) (vty_of_dity d2))
......@@ -250,73 +220,75 @@ let specialize_scheme tvs dity =
in
specialize dity
(***
(* Specialization of symbols *)
let find_type_variable htv tv =
try
Htv.find htv tv
with Not_found ->
let dtv = create_type_variable () in
Htv.add htv tv dtv;
dtv
let rec dity_of_ity ~user htv hreg ity = match ity.ity_node with
| Ityvar tv -> assert (not user); find_type_variable htv tv
| Itypur (ts, ityl) -> ts_app ts (List.map (dity_of_ity ~user htv hreg) ityl)
| Ityapp (its, ityl, rl) ->
its_app_real its (List.map (dity_of_ity ~user htv hreg) ityl)
(List.map (dreg_of_reg ~user htv hreg) rl)
and dreg_of_reg ~user htv hreg r =
try
Hreg.find hreg r
with Not_found ->
let dreg = create_dreg ~user (dity_of_ity ~user htv hreg r.reg_ity) in
Hreg.add hreg r dreg;
dreg
let dity_of_vtv ~user htv hreg v = dity_of_ity ~user htv hreg v.vtv_ity
let specialize_vtvalue ~user vtv =
let htv = Htv.create 17 in
let hreg = Hreg.create 17 in
[], dity_of_vtv ~user htv hreg vtv
dity_of_vtv ~user htv hreg vtv
let specialize_pvsymbol pv =
specialize_vtvalue ~user:true pv.pv_vtv
let make_arrow_type tyl ty =
let arrow ty1 ty2 =
create (Dts (ts_arrow, [ty1; ty2])) (lazy (invalid_arg "ity_of_dity")) in
List.fold_right arrow tyl ty
let specialize_vtarrow ~user vta =
let specialize_vtarrow vta =
let htv = Htv.create 17 in
let hreg = Hreg.create 17 in
let rec decompose args a =
let args = dity_of_vtv ~user htv a.vta_arg :: args in
match a.vta_result with
| VTvalue v -> List.rev args, dity_of_vtv htv v
| VTarrow a1 -> decompose args a1
let rec specialize a =
let arg = dity_of_vtv ~user:false htv hreg a.vta_arg in
let res = match a.vta_result with
| VTvalue v -> dity_of_vtv ~user:false htv hreg v
| VTarrow a1 -> specialize a1
in
make_arrow_type [arg] res
in
decompose [] vta
specialize vta
let specialize_psymbol ps = specialize_vtarrow ps.ps_vta
let specialize_plsymbol pls =
let htv = Htv.create 17 in
List.map (dity_of_vtv htv) pls.pl_args, dity_of_vtv htv pls.pl_value
let hreg = Hreg.create 17 in
let args = List.map (dity_of_vtv ~user:false htv hreg) pls.pl_args in
make_arrow_type args (dity_of_vtv ~user:false htv hreg pls.pl_value)
let dity_of_ty htv ty = dity_of_ity htv (ity_of_ty ty)
let dity_of_ty ~user htv hreg ty = dity_of_ity ~user htv hreg (ity_of_ty ty)
let specialize_lsymbol ls =
let htv = Htv.create 17 in
let hreg = Hreg.create 17 in
let ty = match ls.ls_value with
| None -> dity_of_ity htv ity_bool
| Some ty -> dity_of_ty htv ty
| None -> dity_of_ity ~user:false htv hreg ity_bool
| Some ty -> dity_of_ty ~user:false htv hreg ty
in
List.map (dity_of_ty htv) ls.ls_args, ty
let specialize_prgsymbol = function
| PV pv -> specialize_vtvalue pv.pv_vtv
| PA pa -> specialize_vtarrow pa.pa_vta
| PS ps -> specialize_vtarrow ps.ps_vta
| PL pl -> specialize_plsymbol pl
let specialize_darrow (args, res) =
let htv = Hashtbl.create 17 in
let rec specialize_dity d =
try Hashtbl.find htv !d.uid
with Not_found ->
let d = match !d.node with
| Dvar -> create_type_variable ()
| Duvar s -> create_user_type_variable s
| Dits (its, dl) -> its_app its (List.map specialize_dity dl)
| Dts (ts, dl) -> ts_app ts (List.map specialize_dity dl)
in
Hashtbl.add htv !d.uid d;
d
in
List.map specialize_dity args, specialize_dity res
let match_darrow ps da =
let rec match_arrow s vta (args, res) =
let s, args = match args with
| [] -> assert false
| arg :: args ->
let ity1 = vta.vta_arg.vtv_ity in
let ity2 = ity_of_dity arg in
ity_match s ity1 ity2, args
in
match vta.vta_result with
| VTvalue v -> assert (args = []); ity_match s v.vtv_ity (ity_of_dity res)
| VTarrow a -> match_arrow s a (args, res)
in
match_arrow ity_subst_empty ps.ps_vta da
***)
let args = List.map (dity_of_ty ~user:false htv hreg) ls.ls_args in
make_arrow_type args ty
......@@ -41,6 +41,8 @@ val create_type_variable: unit -> dity
val its_app: user:bool -> itysymbol -> dity list -> dity
val ts_app: tysymbol -> dity list -> dity
val make_arrow_type: dity list -> dity -> dity
val unify: dity -> dity -> unit
(** destructive unification *)
......@@ -50,11 +52,7 @@ val vty_of_dity: dity -> vty
val specialize_scheme: tvars -> dity -> dity
(***
val specialize_lsymbol: lsymbol -> dity
val specialize_pvsymbol: pvsymbol -> dity
val specialize_psymbol: psymbol -> dity
val specialize_plsymbol: plsymbol -> dity
val match_darrow: psymbol -> darrow -> ity_subst
***)
......@@ -158,7 +158,6 @@ let print_psty fmt ps =
let print_ppat fmt ppat = print_pat fmt ppat.ppat_pattern
(*
(* expressions *)
let rec print_expr fmt e = print_lexpr 0 fmt e
......@@ -208,10 +207,11 @@ and print_enode pri fmt e = match e.e_node with
| Earrow a ->
print_ps fmt a
| Eapp (e,v) ->
fprint fmt "%a@ %a" (print_lexpr pri) e print_pv v
fprintf fmt "%a@ %a" (print_lexpr pri) e print_pv v
| 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")
......@@ -241,7 +241,11 @@ and print_enode pri fmt e = match e.e_node with
(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>"
(*
and print_tbranch fmt br =
let p,t = t_open_branch br in
fprintf fmt "@[<hov 4>| %a ->@ %a@]" print_pat p print_term t;
......@@ -250,11 +254,6 @@ and print_tbranch fmt br =
and print_tl fmt tl =
if tl = [] then () else fprintf fmt "@ [%a]"
(print_list alt (print_list comma print_term)) tl
(*
val print_expr : formatter -> expr -> unit (* expression *)
*)
*)
(** Type declarations *)
......
......@@ -52,9 +52,7 @@ val print_effect : formatter -> effect -> unit (* effect *)
val print_ppat : formatter -> ppattern -> unit (* program patterns *)
(*
val print_expr : formatter -> expr -> unit (* expression *)
*)
val print_ty_decl : formatter -> itysymbol -> unit
val print_data_decl : formatter -> data_decl -> unit
......
......@@ -134,17 +134,13 @@ 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_arg dity { dexpr_loc = loc; dexpr_type = (args, res) } =
if args <> [] then errorm ~loc "value expected";
unify dity res
let unify_args ls args el =
try
List.iter2 unify_arg args el
with Invalid_argument _ ->
raise (Term.BadArity (ls, List.length args, List.length el))
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
......@@ -157,11 +153,11 @@ let unify_args_prg ~loc prg args el = match prg with
| [], _ :: _ -> 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
*)
(* value restriction *)
let rec is_fun e = match e.dexpr_desc with
......@@ -179,13 +175,12 @@ let rec dexpr ~userloc denv e =
in
e
and dexpr_desc ~userloc denv _loc = function
and dexpr_desc ~userloc denv loc = function
| Ptree.Eident (Qident {id=x}) when Mstr.mem x denv.locals ->
(* local variable *)
let tvs, dity = Mstr.find x denv.locals in
let dity = specialize_scheme tvs dity in
DElocal x, dity
(***
| Ptree.Eident p ->
let x = Typing.string_list_of_qualid [] p in
begin
......@@ -194,11 +189,11 @@ and dexpr_desc ~userloc denv _loc = function
begin match prg with
| PV pv -> DEglobal_pv pv, specialize_pvsymbol pv
| PS ps -> DEglobal_ps ps, specialize_psymbol ps
| PL pl -> DEglobal_pl (pl, []), specialize_plsymbol pl
| PL pl -> DEglobal_pl pl, specialize_plsymbol pl
end
with Not_found -> try
let ls = ns_find_ls (Theory.get_namespace (get_theory denv.uc)) x in
DElogic (ls, []), specialize_lsymbol ls
DEglobal_ls ls, specialize_lsymbol ls
with Not_found ->
errorm ~loc "unbound symbol %a" Typing.print_qualid p
end
......@@ -206,19 +201,8 @@ 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
begin match e.dexpr_desc with
| DElogic (ls, _) ->
let args, res = e.dexpr_type in
unify_args ls args el;
DElogic (ls, el), ([], res)
| DEglobal (prg, _) ->
let args, res = e.dexpr_type in
let args = unify_args_prg ~loc prg args el in
DEglobal (prg, el), (args, res)
| _ ->
assert false (*TODO*)
end
***)
let res = unify_args el e.dexpr_type in
DEapply (e, el), res
| Ptree.Elet (id, e1, e2) ->
let e1 = dexpr ~userloc denv e1 in
let tvars =
......@@ -228,6 +212,24 @@ and dexpr_desc ~userloc denv _loc = function
{ denv with locals = Mstr.add id.id s denv.locals; tvars = tvars } in
let e2 = dexpr ~userloc denv e2 in
DElet (id, e1, e2), e2.dexpr_type
| Ptree.Efun (bl, tr) ->
let dbinder denv (id, pty) =
let dity = match pty with
| Some pty -> dity_of_pty ~user:false denv pty
| None -> create_type_variable ()
in
let tvars = add_tvars denv.tvars dity in
let denv = { denv with
locals = Mstr.add id.id (tvars, dity) denv.locals;
tvars = tvars }
in
denv, (id, false, dity)
in
let denv, bl = Util.map_fold_left dbinder denv bl in
let _,e,_ as tr = dtriple ~userloc denv tr in
let dity =
make_arrow_type (List.map (fun (_,_,d) -> d) bl) e.dexpr_type in
DEfun (bl, tr), dity
| Ptree.Ecast (e1, pty) ->
let e1 = dexpr ~userloc denv e1 in
unify e1.dexpr_type (dity_of_pty ~user:false denv pty);
......@@ -237,6 +239,14 @@ and dexpr_desc ~userloc denv _loc = function
| _ ->
assert false (*TODO*)
and dtriple ~userloc denv (p, e, q) =
let e = dexpr ~userloc denv e in
let q = dpost denv q in
p, e, q
and dpost _denv (q, _ql) =
q, [] (* TODO *)
let id_user x = id_user x.id x.id_loc
let rec expr locals de = match de.dexpr_desc with
......@@ -262,20 +272,22 @@ let rec expr locals de = match de.dexpr_desc with
let locals = Mstr.add x.id def1.let_var locals in
let e2 = expr locals de2 in
e_let def1 e2
| DEapply (de1, de2) ->
| DEapply (de1, del) ->
let e1 = expr locals de1 in
let e2 = expr locals de2 in
e_app e1 [e2]
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
end
| DEglobal_pv pv ->
e_value pv
| DEglobal_ps ps ->
e_cast ps (vty_of_dity de.dexpr_type)
| DEglobal_pl (pls, del) ->
let ity = ity_of_dity de.dexpr_type in
e_plapp pls (List.map (expr locals) del) ity
| DElogic (ls, del) ->
let ity = ity_of_dity de.dexpr_type in
e_lapp ls (List.map (expr locals) del) ity
| DEglobal_pl pls ->
e_plapp pls [] (ity_of_dity de.dexpr_type)
| DEglobal_ls ls ->
e_lapp ls [] (ity_of_dity de.dexpr_type)
| _ ->
assert false (*TODO*)
......@@ -763,7 +775,8 @@ let add_module lib path mm mt m =
Loc.try3 loc close_namespace uc import name
| Dlet (_id, e) ->
let e = dexpr ~userloc:None (create_denv uc) e in
ignore (expr Mstr.empty e);
let e = expr Mstr.empty e in
Format.eprintf "%a@." Mlw_pretty.print_expr e;
uc
| Dletrec _ | Dparam _ | Dexn _ ->
assert false (* TODO *)
......
......@@ -12,6 +12,7 @@ module M
end
module N
use import int.Int
use import M
goal G1: f 41 = 42
......@@ -19,6 +20,8 @@ module N
with forest 'a = Cons (tree 'a) (forest 'a) | Nil
type ref 'a = {| ghost mutable contents : 'a |}
let f x = x + x
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