Denv.dty is now an abstract type, with a view

parent 36edd6ba
module M
use import int.Int
use import module stdlib.Ref
(* Side effect in expressions (Bart Jacobs' tricky example) *)
parameter b : ref int
......
......@@ -38,18 +38,23 @@ let () = Exn_printer.register (fun fmt e -> match e with
(** types with destructive type variables *)
type dty =
type dty_view =
| Tyvar of type_var
| Tyapp of tysymbol * dty list
| Tyapp of tysymbol * dty_view list
and type_var = {
tag : int;
user : bool;
tvsymbol : tvsymbol;
mutable type_val : dty option;
mutable type_val : dty_view option;
type_var_loc : loc option;
}
let tyvar v = Tyvar v
let tyapp (s, tyl) = Tyapp (s, tyl)
type dty = dty_view
let tvsymbol_of_type_var tv = tv.tvsymbol
let rec print_dty fmt = function
......@@ -64,6 +69,10 @@ let rec print_dty fmt = function
| Tyapp (s, l) ->
fprintf fmt "%s %a" s.ts_name.id_string (print_list comma print_dty) l
let rec view_dty = function
| Tyvar { type_val = Some dty } -> view_dty dty
| dty -> dty
let create_ty_decl_var =
let t = ref 0 in
fun ?loc ~user tv ->
......
......@@ -28,10 +28,17 @@ type type_var
val create_ty_decl_var : ?loc:Ptree.loc -> user:bool -> tvsymbol -> type_var
type dty =
type dty
val tyvar : type_var -> dty
val tyapp : tysymbol * dty list -> dty
type dty_view =
| Tyvar of type_var
| Tyapp of tysymbol * dty list
val view_dty : dty -> dty_view
val unify : dty -> dty -> bool
val print_dty : Format.formatter -> dty -> unit
......
......@@ -196,11 +196,11 @@ let add_prop_decl = with_tuples ~reset:true add_prop_decl
let rec type_inst s ty = match ty.ty_node with
| Ty.Tyvar n -> Mtv.find n s
| Ty.Tyapp (ts, tyl) -> Tyapp (ts, List.map (type_inst s) tyl)
| Ty.Tyapp (ts, tyl) -> tyapp (ts, List.map (type_inst s) tyl)
let rec dty env = function
| PPTtyvar {id=x} ->
Tyvar (find_user_type_var x env)
tyvar (find_user_type_var x env)
| PPTtyapp (p, x) ->
let loc = qloc x in
let ts, a = specialize_tysymbol loc x env.uc in
......@@ -209,7 +209,7 @@ let rec dty env = function
let tyl = List.map (dty env) p in
begin match ts.ts_def with
| None ->
Tyapp (ts, tyl)
tyapp (ts, tyl)
| Some ty ->
let add m v t = Mtv.add v t m in
let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in
......@@ -217,7 +217,7 @@ let rec dty env = function
end
| PPTtuple tyl ->
let ts = ts_tuple (List.length tyl) in
Tyapp (ts, List.map (dty env) tyl)
tyapp (ts, List.map (dty env) tyl)
let find_ns find p ns =
let loc = qloc p in
......@@ -291,7 +291,7 @@ let check_pat_linearity p =
let fresh_type_var loc =
let tv = create_tvsymbol (id_user "a" loc) in
Tyvar (create_ty_decl_var ~loc ~user:false tv)
tyvar (create_ty_decl_var ~loc ~user:false tv)
let rec dpat env pat =
let env, n, ty = dpat_node pat.pat_loc env pat.pat_desc in
......@@ -314,7 +314,7 @@ and dpat_node loc env = function
let s = fs_tuple n in
let tyl = List.map (fun _ -> fresh_type_var loc) pl in
let env, pl = dpat_args s.ls_name loc env tyl pl in
let ty = Tyapp (ts_tuple n, tyl) in
let ty = tyapp (ts_tuple n, tyl) in
env, Papp (s, pl), ty
| PPpas (p, x) ->
let env, p = dpat env p in
......@@ -400,16 +400,16 @@ and dterm_node ~localize loc env = function
let s = fs_tuple n in
let tyl = List.map (fun _ -> fresh_type_var loc) tl in
let tl = dtype_args s.ls_name loc env tyl tl in
let ty = Tyapp (ts_tuple n, tyl) in
let ty = tyapp (ts_tuple n, tyl) in
Tapp (s, tl), ty
| PPinfix (e1, x, e2) ->
let s, tyl, ty = specialize_fsymbol (Qident x) env.uc in
let tl = dtype_args s.ls_name loc env tyl [e1; e2] in
Tapp (s, tl), ty
| PPconst (ConstInt _ as c) ->
Tconst c, Tyapp (Ty.ts_int, [])
Tconst c, tyapp (Ty.ts_int, [])
| PPconst (ConstReal _ as c) ->
Tconst c, Tyapp (Ty.ts_real, [])
Tconst c, tyapp (Ty.ts_real, [])
| PPlet (x, e1, e2) ->
let e1 = dterm ~localize env e1 in
let ty = e1.dt_ty in
......@@ -479,7 +479,7 @@ and dterm_node ~localize loc env = function
| TRterm t ->
let id = { id = "fc"; id_lab = []; id_loc = loc } in
let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
let nty = Tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
let nty = tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
uqu ([],t.dt_ty)
in
let h = { dt_node = Tvar id.id ; dt_ty = ty } in
......@@ -496,8 +496,8 @@ and dterm_node ~localize loc env = function
| [] -> assert false
in
let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
let nty = Tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
uqu ([],Tyapp (ts_pred, [uty]))
let nty = tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
uqu ([],tyapp (ts_pred, [uty]))
in
let h = { dt_node = Tvar id.id ; dt_ty = ty } in
let h = List.fold_left2 (fun h (uid,uty) ty ->
......
......@@ -316,7 +316,8 @@ end = struct
let ts = ty_match Mtv.empty x.pv_ty s.p_ty in
let c = type_c_of_type_v (Tarrow (bl, c)) in
let ef = Mpv.add x (R.Rglobal s) Mpv.empty in
subst_type_c ef ts (subst1 x.pv_vs (t_app s.p_ls [] x.pv_vs.vs_ty)) c
let t = t_app s.p_ls [] (ty_inst ts x.pv_vs.vs_ty) in
subst_type_c ef ts (subst1 x.pv_vs t) c
| _ ->
assert false
......
......@@ -59,7 +59,7 @@ let id_result = "result"
(* phase 1: typing programs (using destructive type inference) **************)
let dty_app (ts, tyl) = assert (ts.ts_def = None); Tyapp (ts, tyl)
let dty_app (ts, tyl) = assert (ts.ts_def = None); tyapp (ts, tyl)
let find_ts uc s = ns_find_ts (get_namespace (theory_uc uc)) [s]
let find_ls uc s = ns_find_ls (get_namespace (theory_uc uc)) [s]
......@@ -113,23 +113,23 @@ let loc_of_ls ls = match ls.ls_name.id_origin with
| User loc -> Some loc
| _ -> None (* FIXME: loc for recursive functions *)
let dmodel_type = function
| Tyapp (ts, tyl) as ty ->
let dmodel_type dty = match view_dty dty with
| Tyapp (ts, tyl) ->
let mt = get_mtsymbol ts in
begin match mt.mt_model with
| None ->
ty
dty
| Some ty ->
let h = Htv.create 17 in
List.iter2 (Htv.add h) mt.mt_args tyl;
let rec inst ty = match ty.ty_node with
| Ty.Tyvar tv -> Htv.find h tv
| Ty.Tyapp (ts, tyl) -> Denv.Tyapp (ts, List.map inst tyl)
| Ty.Tyapp (ts, tyl) -> Denv.tyapp (ts, List.map inst tyl)
in
inst ty
end
| Tyvar _ as ty ->
ty
| Tyvar _ ->
dty
let dpurify ty = try dmodel_type ty with NotMutable -> ty
......@@ -184,9 +184,9 @@ let specialize_exception loc x uc =
let create_type_var loc =
let tv = Ty.create_tvsymbol (id_user "a" loc) in
Tyvar (create_ty_decl_var ~loc ~user:false tv)
tyvar (create_ty_decl_var ~loc ~user:false tv)
let add_pure_var id ty denv = match ty with
let add_pure_var id ty denv = match view_dty ty with
| Tyapp (ts, _) when Ty.ts_equal ts ts_arrow -> denv
| _ -> Typing.add_var id ty denv
......@@ -207,13 +207,13 @@ let expected_type e ty =
let pure_type env = Typing.dty env.denv
let check_mutable_type loc = function
let check_mutable_type loc dty = match view_dty dty with
| Denv.Tyapp (ts, _) when is_mutable_ts ts ->
()
| ty ->
| _ ->
errorm ~loc
"this expression has type %a, but is expected to have a mutable type"
print_dty ty
print_dty dty
let dreference env = function
| Qident id when Mstr.mem id.id env.locals ->
......
......@@ -11,17 +11,16 @@ module P
set r (get r + 1)
{ r = old r + 1 }
(* parameter r : ref int *)
parameter r : ref int
let foo (x : int) =
{ x = 1 }
if x = 1 || absurd then 2 else 3
{ result = 2 }
let f () =
{ }
let r = ref 0 in
(* assert { r = 0 }; *)
let f (r : ref int) =
{ r = 0 }
assert { r = 0 };
incr r;
get r
{ result = 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