Commit 892ae0d7 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Implement weak polymorphic variables. These variables are displayed as _weak0 (as in OCaml).

They cannot be generalized. These are juste variables "waiting to be instantiated".
When such an instantiation occurs, the typing environment is patched to substitute all occurrences
of the variables with their instance.
As with OCaml, one can observe weak polymorphic variables in the toplevel e.g. by creating mutable
references or performing partial applications of polymorphic functions.
When compiling a file, an error is raised when toplevel identifiers whose type contains polymorphic variables remain.
parent 2a289e1c
Pipeline #191 passed with stages
in 4 minutes and 24 seconds
......@@ -198,7 +198,7 @@ let compile_rec_funs env funs =
open Cduce_loc
let eval ~run ~show (tenv, cenv, codes) e =
let e, t = Typer.type_expr tenv e in
let tenv, e, t = Typer.type_expr tenv e in
let e, lsize = compile_expr cenv e in
if run then
let v = Eval.expr e lsize in
......
......@@ -158,7 +158,7 @@ let rec print_exn ppf = function
Format.fprintf ppf "%a@." print_protect (Printexc.to_string exn)
let eval_quiet tenv cenv e =
let e, _ = Typer.type_expr tenv e in
let _, e, _ = Typer.type_expr tenv e in
Compile.compile_eval_expr cenv e
let debug ppf tenv _cenv = function
......
......@@ -106,6 +106,7 @@ let compile verbose name src =
let ty_env, c_env, code =
Compile.comp_unit ?show Builtin.env (Compile.empty descr) p
in
Typer.check_weak_variables ty_env;
Compunit.leave ();
let ext = Externals.get () in
let depends = Tbl.fold (fun name c accu -> (name, digest c) :: accu) tbl [] in
......
......@@ -364,7 +364,7 @@ match n with
%inline type_params:
| { [] }
| "(" l = separated_nonempty_list(",", POLY) ")" {
| "(" l = separated_nonempty_list(",", poly_var) ")" {
let seen = ref [] in
List.map (fun s ->
if List.mem s !seen then
......@@ -373,6 +373,14 @@ match n with
U.mk s) l
};
%inline poly_var:
v = POLY {
if v <> "" && v.[0] = '_' then
parsing_error $sloc "Type variable names starting with _ are reserved for weak
polymorphic variables, they cannot appear in programs.";
v
};
pat:
| x = arrow_pat "where" l = and_pat_list { mk $sloc (Recurs(x, List.rev l)) }
......@@ -439,7 +447,7 @@ constr_pat:
;
simple_pat:
| p = POLY { mk $sloc (Poly (U.mk p)) }
| p = poly_var { mk $sloc (Poly (U.mk p)) }
| "{" r = record_spec "}" { r }
| "ref" p = constr_pat {
let get_fun = mk $sloc (Arrow (pat_nil, p))
......@@ -757,7 +765,7 @@ namespace_binding_rem:
%inline poly_list:
| { [] }
| l = nonempty_list(POLY) "." { List.map U.mk l }
| l = nonempty_list(poly_var) "." { List.map U.mk l }
;
%inline fun_decl_after_lpar:
......
......@@ -64,10 +64,12 @@ type item =
type t = {
ids : item Env.t;
ids_loc : loc Env.t;
ns : Ns.table;
keep_ns : bool;
poly_vars : (U.t * Var.t) list;
mono_vars : Var.Set.t;
mutable weak_vars : Types.t option Var.Map.map;
}
(* Namespaces *)
......@@ -118,10 +120,12 @@ let type_schema env loc name uri =
let empty_env =
{
ids = Env.empty;
ids_loc = Env.empty;
ns = Ns.def_table;
keep_ns = false;
poly_vars = [];
mono_vars = Var.Set.empty;
weak_vars = Var.Map.empty;
}
let enter_id x i env = { env with ids = Env.add x i env.ids }
......@@ -1339,9 +1343,36 @@ and type_check' loc env e constr precise =
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1arrow t2
else
match Types.Tallying.squareapply env.mono_vars t1 t2 with
| None -> raise_loc loc (constraint_exn t2 dom)
| Some (_, res) -> res
match Types.Tallying.apply_raw env.mono_vars t1 t2 with
| None -> raise_loc loc (constraint_exn t2 dom)
| Some (subst, tx, ty, res) ->
List.iter
(fun s ->
Var.Map.iteri
(fun wv t ->
match Var.kind wv with
| `generated | `user -> ()
| `weak ->
let tt = Types.Subst.clean_type env.mono_vars t in
env.weak_vars <-
Var.Map.update
(fun prev next ->
match (prev, next) with
| None, Some t -> next
| Some tp, Some tn when Types.equiv tp tn ->
next
| Some tp, Some tn ->
error loc
(Format.asprintf
"the weak polymorphic variable %a is \
instantiated several times in the \
same expression."
Var.print wv)
| _ -> assert false)
wv (Some tt) env.weak_vars)
s)
subst;
res
(*
if Types.Arrow.need_arg t1 then
let t2 = type_check env e2 dom true in
......@@ -1425,7 +1456,8 @@ and type_check_pair ?(kind = `Normal) loc env e1 e2 constr precise =
let t1 = type_check env e1 (Types.Product.pi1 rects) (precise || need_s) in
let c2 = Types.Product.constraint_on_2 rects t1 in
if Types.is_empty c2 then
raise_loc loc (ShouldHave2 (constr, "but the first component has type:", t1));
raise_loc loc
(ShouldHave2 (constr, "but the first component has type:", t1));
let t2 = type_check env e2 c2 precise in
if precise then
......@@ -1593,13 +1625,34 @@ let report_unused_branches () =
let clear_unused_branches () = cur_branch := []
(* API *)
let update_weak_variables env =
let to_patch, to_keep =
Var.Map.split
(fun v -> function Some _ -> true | None -> false)
env.weak_vars
in
let to_patch =
Var.Map.map (function Some t -> t | None -> assert false) to_patch
in
{
env with
ids =
Env.mapi
(fun v -> function
| Val t ->
let tt = Types.Subst.apply_full to_patch t in
Val tt
| x -> x)
env.ids;
weak_vars = to_keep;
}
let type_expr env e =
clear_unused_branches ();
let e = expr env e in
let t = type_check env e Types.any true in
report_unused_branches ();
(e, t)
(update_weak_variables env, e, t)
let type_let_decl env p e =
clear_unused_branches ();
......@@ -1607,22 +1660,46 @@ let type_let_decl env p e =
let typs = type_let_decl env decl in
report_unused_branches ();
let is_value = Typed.is_value decl.let_body in
(* patch env to update weak variables *)
let env = update_weak_variables env in
let typs =
List.map
(fun (id, t) ->
let tt = Types.Subst.clean_type Var.Set.empty t in
let vars = Types.Subst.vars tt in
if not (Var.Set.is_empty vars) && not is_value then
raise_loc_generic p.loc
(Format.asprintf
"The type of identifier %a is %a.@\n\
It contains polymorphic variables that cannot be generalized."
Ident.print id Types.Print.print tt);
(id, tt))
if (not (Var.Set.is_empty vars)) && not is_value then
let weak_vars, all_weak_vars, _ =
List.fold_left
(fun (acc, accw, i) v ->
let wv = Var.mk ~kind:`weak ("_weak" ^ string_of_int i) in
((v, Types.var wv) :: acc, Var.Map.add wv None accw, i + 1))
([], env.weak_vars, Var.Map.length env.weak_vars)
vars
in
let () = env.weak_vars <- all_weak_vars in
let subst = Types.Subst.from_list weak_vars in
(id, Types.Subst.apply_full subst tt)
else
(* raise_loc_generic p.loc
(Format.asprintf
"The type of identifier %a is %a.@\n\
It contains polymorphic variables that cannot be generalized."
Ident.print id Types.Print.print tt);*)
(id, tt))
typs
in
let env = enter_values typs env in
({ env with mono_vars = Var.Set.empty; poly_vars = [] }, decl, typs)
( {
env with
ids_loc =
List.fold_left
(fun acc (id, _) -> Env.add id p.loc acc)
env.ids_loc typs;
mono_vars = Var.Set.empty;
poly_vars = [];
},
decl,
typs )
let type_let_funs env funs =
clear_unused_branches ();
......@@ -1640,6 +1717,7 @@ let type_let_funs env funs =
let funs = List.map (expr env') funs in
let typs = type_rec_funs env funs in
report_unused_branches ();
let env = update_weak_variables env in
let env = enter_values typs env in
let env = { env with mono_vars = Var.Set.empty; poly_vars = [] } in
(env, funs, typs)
......@@ -1650,3 +1728,24 @@ let find_cu x env =
| ECDuce cu -> cu
| _ -> raise (Error ("Cannot find external unit " ^ (U.to_string x)))
*)
let check_weak_variables env =
Env.iter
(fun id -> function
| Val t ->
let vrs = Types.Subst.vars t in
List.iter
(fun v ->
match Var.kind v with
| `generated | `user -> ()
| `weak ->
let loc = Env.find id env.ids_loc in
error loc
(Format.asprintf
"Identifier %a has type:@\n\
%a@\n\
which contains weak polymorphic variables." Ident.print
id Types.Print.print t))
vrs
| _ -> ())
env.ids
......@@ -39,7 +39,7 @@ val type_open: t -> Cduce_loc.loc -> Utf8.t list -> t
val type_keep_ns : t -> bool -> t
val type_expr: t -> Ast.pexpr -> Typed.texpr * Types.descr
val type_expr: t -> Ast.pexpr -> t * Typed.texpr * Types.descr
val type_defs: t -> (Cduce_loc.loc * Utf8.t * Utf8.t list * Ast.ppat) list -> t
......@@ -50,8 +50,7 @@ val type_let_funs: t -> Ast.pexpr list ->
t * Typed.texpr list * (id * Types.t) list
(* Assume that all the expressions are Abstractions *)
val check_weak_variables: t -> unit
(* Operators *)
type type_fun = Types.t -> bool -> Types.t
......
......@@ -137,10 +137,11 @@ let apply subst t =
else
match check_var_aux vrs t with
| `Pos v -> Some (Positive.ty (vtype subst v))
| `Neg v -> Some
| `Neg v ->
Some
(Positive.diff (Positive.ty Types.any)
(Positive.ty (vtype subst v)))
| _ -> None)
| _ -> None)
t
in
Types.descr (Positive.solve v)
......@@ -172,12 +173,14 @@ let extract t =
| _ -> assert false
let refresh pvars t =
let all_vars = vars t in
let all_vars = List.filter (fun v -> Var.kind v <> `weak) (vars t) in
let all_vars = Var.Set.diff all_vars pvars in
if Var.Set.is_empty all_vars then t
else
let subst =
Var.Map.map_from_slist (fun v -> Types.var Var.(mk (name v))) all_vars
Var.Map.map_from_slist
(fun v -> Types.var Var.(mk ~kind:(kind v) (name v)))
all_vars
in
apply subst t
......@@ -199,16 +202,15 @@ let solve_rectype t alpha =
Positive.define x v;
Types.descr (Positive.solve x)
let clean_type ?(pos=Types.empty) ?(neg=Types.any) delta t =
let clean_type ?(pos = Types.empty) ?(neg = Types.any) delta t =
let polarities = vars_gen true t in
let clean_subst =
Var.Map.fold
(fun v pol acc ->
match pol with
| `Both -> acc
| `Pos -> if Var.Set.mem delta v then acc else Var.Map.add v pos acc
| `Neg -> if Var.Set.mem delta v then acc else Var.Map.add v neg acc
)
| `Pos -> if Var.Set.mem delta v then acc else Var.Map.add v pos acc
| `Neg -> if Var.Set.mem delta v then acc else Var.Map.add v neg acc)
polarities Var.Map.empty
in
apply_full clean_subst t
......@@ -499,7 +499,7 @@ let merge delta m =
let solve delta s =
let add_eq alpha s t acc =
let beta = var Var.(mk ~kind:`generated ("_" ^ name alpha)) in
let beta = let a = Var.name alpha in var Var.(mk ~kind:`generated (a ^ a)) in
Var.Map.replace alpha (cap (cup s beta) t) acc
in
let extra_var t acc =
......
module V = struct
type t = { id : int; name : string; kind : [ `user | `generated ] }
type t = { id : int; name : string; kind : [ `user | `generated | `weak ] }
let equal a b = a == b || a.id == b.id
......@@ -11,12 +11,16 @@ module V = struct
let dump ppf x =
Format.fprintf ppf "VAR(%d,%s,%s)" x.id x.name
(if x.kind = `user then "`user" else "`generated")
(match x.kind with
| `user -> "`user"
| `generated -> "`generated"
| `weak -> "`weak")
end
include V
let print ppf v = Format.fprintf ppf "'%s" v.name
let print ppf v =
Format.fprintf ppf "'%s" v.name
module Set = struct
include SortedList.Make (V)
......@@ -73,9 +77,11 @@ let renaming vars =
(fun v1 v2 ->
let c =
match (v1.kind, v2.kind) with
| `user, `user | `generated, `generated -> 0
| `user, `user | `generated, `generated | `weak, `weak -> 0
| `weak, _ -> -1
| _, `weak -> 1
| `user, _ -> -1
| `generated, _ -> 1
| _, `user -> 1
in
if c == 0 then compare v1 v2 else c)
vv
......
......@@ -9,16 +9,17 @@ module V : Custom.T
include module type of V with type t = V.t
(** Type [t = V.t] represents variables. *)
(** Sets of variables. *)
module Set : sig
include SortedList.S with module Elem = V
val print : Format.formatter -> t -> unit
end
(** Sets of variables. *)
module Map = Set.Map
(** Maps indexed by variables. *)
val mk : ?kind:[ `generated | `user ] -> string -> t
val mk : ?kind:[ `generated | `user | `weak ] -> string -> t
(** mk ~kind "name" creates a fresh variable with name [name] and kind [kind].
It is distinct (in the sense of [equal] and [compare]) from all other
created variables, even those with the same name. The optional kind is used
......@@ -33,7 +34,7 @@ val name : t -> string
val id : t -> int
(** [id v] returns the internal id of the variable. *)
val kind : t -> [ `generated | `user ]
val kind : t -> [ `generated | `user | `weak ]
(** [kind v] returns the kind of the variable. *)
val print : Format.formatter -> t -> unit
......@@ -58,4 +59,4 @@ val merge : t list -> t list -> (Set.t * Set.t) option
(** [merge pos neg] returns the pair of sets of variables contained in [pos] and
[neg] as an option. The option is [None] if [pos] and [neg] have a non-empty
intersection.
*)
\ No newline at end of file
*)
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