Skip to content

Commit

Permalink
Merge branch 'master' into effect-system.
Browse files Browse the repository at this point in the history
Let us no longer do such merges. Instead:
1) make sure that we do all bug fixes in the master branch,
2) rebase all experimental branches on the master before doing a pull request.
  • Loading branch information
matijapretnar committed Aug 14, 2012
2 parents c6bf52b + 672c996 commit 97a5f01
Show file tree
Hide file tree
Showing 5 changed files with 39 additions and 31 deletions.
6 changes: 3 additions & 3 deletions src/ctx.ml
Expand Up @@ -3,10 +3,10 @@ type t = (Common.variable, ty_scheme) Common.assoc

let empty = []

let lookup ~pos ctx x =
let lookup ctx x =
match Common.lookup x ctx with
| Some (ps, t) -> snd (Type.refresh ps t)
| None -> Error.typing ~pos "Unknown name %s" x
| Some (ps, t) -> Some (snd (Type.refresh ps t))
| None -> None

let extend ctx x ty_scheme = (x, ty_scheme) :: ctx

Expand Down
16 changes: 6 additions & 10 deletions src/ctx.mli
Expand Up @@ -6,28 +6,25 @@
*)

(** The types of contexts and type schemes. *)
type ty_scheme = (Type.ty_param list * Type.dirt_param list * Type.region_param list) * Type.ty
type ty_scheme = Type.params * Type.ty

type t

(** [empty] is the empty context. *)
val empty : t

(** [lookup ~pos ctx x] returns a fresh instance of the type scheme assigned
to the variable [x] in the context [ctx]. The optional position is used in
error reporting when the variable is not bound in the context. *)
val lookup : pos:Common.position -> t -> Common.variable -> Type.ty
(** [lookup ctx x] returns a fresh instance of the type scheme assigned
to the variable [x] in the context [ctx]. *)
val lookup : t -> Common.variable -> Type.ty option

(** [extend x ty_scheme ctx] returns the context [ctx] extended with
a variable [x] bound to the type scheme [ty_scheme]. *)
val extend :
t -> Common.variable -> ty_scheme -> t
val extend : t -> Common.variable -> ty_scheme -> t

(** [extend_ty x ty ctx] returns the context [ctx] extended with a variable [x]
bound to the type [ty]. The type is promoted to a type scheme with no
generalized type parameters. *)
val extend_ty :
t -> Common.variable -> Type.ty -> t
val extend_ty : t -> Common.variable -> Type.ty -> t

(** [subst_ctx sbst ctx] returns a substitution of [ctx] under [sbst]. *)
val subst_ctx : t -> Type.substitution -> t
Expand All @@ -36,4 +33,3 @@ val subst_ctx : t -> Type.substitution -> t
type scheme. If [poly] is [true], all free type parameters in [ty] that do
not appear in [ctx] are universally quantified. *)
val generalize : t -> bool -> Type.ty -> ty_scheme

3 changes: 3 additions & 0 deletions src/eff.ml
Expand Up @@ -33,6 +33,9 @@ let options = Arg.align [
("--pervasives",
Arg.String (fun str -> pervasives_file := str),
" Specify the pervasives.eff file");
("--no-beautify",
Arg.Set Type.disable_beautify,
" Do not beautify types");
("--no-pervasives",
Arg.Clear pervasives,
" Do not load pervasives.eff");
Expand Down
6 changes: 5 additions & 1 deletion src/infer.ml
Expand Up @@ -176,7 +176,11 @@ and infer_let_rec ctx cstr pos defs =
[ctx]. It returns the inferred type of [e]. *)
and infer_expr ctx cstr (e,pos) =
match e with
| Core.Var x -> Ctx.lookup ~pos ctx x
| Core.Var x ->
begin match Ctx.lookup ctx x with
| Some ty -> ty
| None -> Error.typing ~pos "Unknown variable %s" x
end
| Core.Const const -> ty_of_const const
| Core.Tuple es -> T.Tuple (C.map (infer_expr ctx cstr) es)
| Core.Record [] -> assert false
Expand Down
39 changes: 22 additions & 17 deletions src/type.ml
Expand Up @@ -182,26 +182,31 @@ let refresh params ty =
let params', sbst = refreshing_subst params in
params', subst_ty sbst ty

let disable_beautify = ref false

(** [beautify ty] returns a sequential replacement of all type parameters in
[ty] that can be used for its pretty printing. *)
let beautify ((ps, ds, rs), ty) =
let next_ty_param = Common.fresh "beautify_ty" in
let next_dirt_param = Common.fresh "beautify_dirt" in
let next_region_param = Common.fresh "beautify_region" in
let (xs, ys, zs) = free_params ty in
let xs_map = List.map (fun p -> (p, Ty_Param (next_ty_param ()))) xs
and ys_map = List.map (fun q -> (q, Dirt_Param (next_dirt_param ()))) ys
and zs_map = List.map (fun r -> (r, Region_Param (next_region_param ()))) zs in
let subst ps ps_map = List.map (fun p ->
match Common.lookup p ps_map with
| None -> p
| Some p' -> p') ps in
let sbst =
{ subst_ty = Common.assoc_map (fun p' -> TyParam p') xs_map ;
subst_dirt = Common.assoc_map (fun q' -> DirtParam q') ys_map ;
subst_region = Common.assoc_map (fun r' -> RegionParam r') zs_map }
in
(subst ps xs_map, subst ds ys_map, subst rs zs_map), subst_ty sbst ty
if !disable_beautify then
((ps, ds, rs), ty)
else
let next_ty_param = Common.fresh "beautify_ty" in
let next_dirt_param = Common.fresh "beautify_dirt" in
let next_region_param = Common.fresh "beautify_region" in
let (xs, ys, zs) = free_params ty in
let xs_map = List.map (fun p -> (p, Ty_Param (next_ty_param ()))) xs
and ys_map = List.map (fun q -> (q, Dirt_Param (next_dirt_param ()))) ys
and zs_map = List.map (fun r -> (r, Region_Param (next_region_param ()))) zs in
let subst ps ps_map = List.map (fun p ->
match Common.lookup p ps_map with
| None -> p
| Some p' -> p') ps in
let sbst =
{ subst_ty = Common.assoc_map (fun p' -> TyParam p') xs_map ;
subst_dirt = Common.assoc_map (fun q' -> DirtParam q') ys_map ;
subst_region = Common.assoc_map (fun r' -> RegionParam r') zs_map }
in
(subst ps xs_map, subst ds ys_map, subst rs zs_map), subst_ty sbst ty


let beautify_dirty (params, ty) drt =
Expand Down

0 comments on commit 97a5f01

Please sign in to comment.