Skip to content
Browse files

Cleaned up Ctx and added an interface for it.

  • Loading branch information...
1 parent 663dbf4 commit da2ac90c3040797b5bad4f8eda6a965474aeaee8 @matijapretnar committed
Showing with 72 additions and 44 deletions.
  1. +24 −25 src/ctx.ml
  2. +37 −0 src/ctx.mli
  3. +3 −4 src/eff.ml
  4. +8 −15 src/infer.ml
View
49 src/ctx.ml
@@ -1,33 +1,32 @@
-(** Type inference contexts *)
-module C = Common
-module T = Type
+type ty_scheme = Type.param list * Type.ty
+type context = (Common.variable, ty_scheme) Common.assoc
-let extend_var x pt ctx = (x, pt) :: ctx
+let empty = []
-let extend_vars vars ctx =
- List.fold_right (fun (x, t) ctx -> extend_var x ([], t) ctx) vars ctx
+let lookup ?pos ctx x =
+ match Common.lookup x ctx with
+ | Some (ps, t) -> snd (Type.refresh ps t)
+ | None -> Error.typing ?pos "Unknown name %s" x
-(** Initial context has no variables and only builtin types *)
-let initial = []
+let extend x ty_scheme ctx = (x, ty_scheme) :: ctx
-(** [freeparams ctx] returns a list of all free type parameters in [ctx] *)
-let free_params lst =
- C.uniq (List.flatten (List.map (fun (_,(ps,t)) -> C.diff (T.free_params t) ps) lst))
+let extend_ty x ty ctx = (x, ([], ty)) :: ctx
-(** [subst_ctx sbst ctx] applies a type substitution to all types occurring in
- [ctx]. *)
let subst_ctx sbst ctx =
- C.assoc_map
- (fun (ps,t) ->
- assert (List.for_all (fun (p,_) -> not (List.mem p ps)) sbst);
- (ps, T.subst_ty sbst t))
- ctx
+ let subst_ty_scheme (ps, ty) =
+ assert (List.for_all (fun (p, _) -> not (List.mem p ps)) sbst);
+ (ps, Type.subst_ty sbst ty)
+ in
+ Common.assoc_map subst_ty_scheme ctx
-(* [generalize_vars sbst ctx vars] generalizes the given variables. *)
-let generalize_vars ctx vars =
- let qs = free_params ctx in
- C.assoc_map (fun t -> C.diff (T.free_params t) qs, t) vars
+(** [free_params ctx] returns a list of all free type parameters in [ctx]. *)
+let free_params ctx =
+ let binding_params (_, (ps, ty)) = Common.diff (Type.free_params ty) ps in
+ Common.uniq (List.flatten (List.map binding_params ctx))
-(* [generalize ctx t] returns the variables over which we may generalize type [t]. *)
-let generalize ctx t =
- C.diff (T.free_params t) (free_params ctx)
+let generalize ctx poly ty =
+ if poly then
+ let ps = Common.diff (Type.free_params ty) (free_params ctx) in
+ (ps, ty)
+ else
+ ([], ty)
View
37 src/ctx.mli
@@ -0,0 +1,37 @@
+(** Type contexts
+
+ Type contexts assign type schemes to variables, and are used for type
+ inference. A type scheme consists of a type and a list of universally
+ quantified type parameters.
+*)
+
+(** The types of contexts and type schemes. *)
+type ty_scheme = Type.param list * Type.ty
+type context
+
+(** [empty] is the empty context. *)
+val empty : context
+
+(** [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 -> context -> Common.variable -> Type.ty
+
+(** [extend x ty_scheme ctx] returns the context [ctx] extended with
+ a variable [x] bound to the type scheme [ty_scheme]. *)
+val extend :
+ Common.variable -> ty_scheme -> context -> context
+
+(** [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 :
+ Common.variable -> Type.ty -> context -> context
+
+(** [subst_ctx sbst ctx] returns a substitution of [ctx] under [sbst]. *)
+val subst_ctx : Type.substitution -> context -> context
+
+(** [generalize ctx poly ty] generalizes the type [ty] in context [ctx] to a
+ type scheme. If [poly] is [true], all free type parameters in [ty] that do
+ not appear in [ctx] are universally quantified. *)
+val generalize : context -> bool -> Type.ty -> ty_scheme
View
7 src/eff.ml
@@ -80,7 +80,7 @@ let parse parser lex =
Error.syntax ~pos:(Lexer.position_of_lex lex) "unrecognised symbol."
let initial_ctxenv =
- (Ctx.initial, Eval.initial)
+ (Ctx.empty, Eval.initial)
let exec_topdef interactive (ctx, env) (d,pos) =
match d with
@@ -109,7 +109,7 @@ let exec_topdef interactive (ctx, env) (d,pos) =
end;
(ctx, env)
| S.External (x, t, f) ->
- let ctx = Ctx.extend_var x (Desugar.external_ty t) ctx in
+ let ctx = Ctx.extend x (Desugar.external_ty t) ctx in
begin match C.lookup f External.values with
| Some v -> (ctx, Eval.update x v env)
| None -> Error.runtime ~pos:pos "unknown external symbol %s." f
@@ -129,8 +129,7 @@ let infer_top_comp ctx c =
let sbst = Unify.solve !cstr in
let ctx = Ctx.subst_ctx sbst ctx in
let ty = Type.subst_ty sbst ty in
- let ps = (if Infer.nonexpansive (fst c) then Ctx.generalize ctx ty else []) in
- ctx, (ps, ty)
+ ctx, Ctx.generalize ctx (Infer.nonexpansive (fst c)) ty
let rec exec_cmd interactive (ctx, env) e =
match e with
View
23 src/infer.ml
@@ -79,7 +79,7 @@ let extend_with_pattern ?(forbidden_vars=[]) ctx cstr p =
let vars, t = infer_pattern cstr p in
match C.find (fun (x,_) -> List.mem_assoc x vars) forbidden_vars with
| Some (x,_) -> Error.typing ~pos:(snd p) "Several definitions of %s." x
- | None -> vars, t, Ctx.extend_vars vars ctx
+ | None -> vars, t, List.fold_right (fun (x, t) ctx -> Ctx.extend_ty x t ctx) vars ctx
let rec infer_abstraction ctx cstr (p, c) =
let _, t1, ctx = extend_with_pattern ctx cstr p in
@@ -115,12 +115,9 @@ and infer_let ctx cstr pos defs =
let sbst = Unify.solve !cstr in
let ws = Common.assoc_map (T.subst_ty sbst) ws in
let ctx = Ctx.subst_ctx sbst ctx in
- let ws =
- (if nonexpansive (fst c)
- then Ctx.generalize_vars ctx ws
- else C.assoc_map (fun t -> ([],t)) ws)
+ let ws = Common.assoc_map (Ctx.generalize ctx (nonexpansive (fst c))) ws
in
- let ctx' = List.fold_right (fun (x,(ps, t)) ctx -> Ctx.extend_var x (ps, t) ctx) ws ctx' in
+ let ctx' = List.fold_right (fun (x, ty_scheme) ctx -> Ctx.extend x ty_scheme ctx) ws ctx' in
(List.rev ws @ vs, ctx'))
([], ctx) defs in
vars, Ctx.subst_ctx (Unify.solve !cstr) ctx
@@ -136,7 +133,7 @@ and infer_let_rec ctx cstr pos defs =
defs
in
let vars = List.fold_right (fun (f,u1,u2,_,_) vars -> (f, (T.Arrow (u1, u2))) :: vars) lst [] in
- let ctx' = List.fold_right (fun (f,u1,u2,_,_) ctx -> Ctx.extend_var f ([], T.Arrow (u1, u2)) ctx) lst ctx in
+ let ctx' = List.fold_right (fun (f,u1,u2,_,_) ctx -> Ctx.extend_ty f (T.Arrow (u1, u2)) ctx) lst ctx in
List.iter
(fun (_,u1,u2,p,c) ->
let _, tp, ctx' = extend_with_pattern ctx' cstr p in
@@ -148,8 +145,8 @@ and infer_let_rec ctx cstr pos defs =
let sbst = Unify.solve !cstr in
let vars = Common.assoc_map (T.subst_ty sbst) vars in
let ctx = Ctx.subst_ctx sbst ctx in
- let vars = Ctx.generalize_vars ctx vars in
- let ctx = List.fold_right (fun (x,(ps,t)) ctx -> Ctx.extend_var x (ps, t) ctx) vars ctx
+ let vars = Common.assoc_map (Ctx.generalize ctx true) vars in
+ let ctx = List.fold_right (fun (x, ty_scheme) ctx -> Ctx.extend x ty_scheme ctx) vars ctx
in
vars, ctx
@@ -157,11 +154,7 @@ 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
- | I.Var x ->
- begin match C.lookup x ctx with
- | Some (ps, t) -> snd (T.refresh ps t)
- | None -> Error.typing ~pos:pos "Unknown name %s" x
- end
+ | I.Var x -> Ctx.lookup ~pos:pos ctx x
| I.Const const -> T.ty_of_const const
| I.Tuple es -> T.Tuple (C.map (infer_expr ctx cstr) es)
| I.Record [] -> assert false
@@ -293,7 +286,7 @@ and infer_comp ctx cstr cp =
add_constraint cstr (snd e1) t1 T.int_ty;
let t2 = infer_expr ctx cstr e2 in
add_constraint cstr (snd e2) t2 T.int_ty;
- let ctx = Ctx.extend_var i ([], T.int_ty) ctx in
+ let ctx = Ctx.extend_ty i T.int_ty ctx in
let t = infer ctx c in
add_constraint cstr (snd c) t T.unit_ty;
T.unit_ty

0 comments on commit da2ac90

Please sign in to comment.
Something went wrong with that request. Please try again.