Skip to content

Commit

Permalink
refactor out type reading logic (#67)
Browse files Browse the repository at this point in the history
  • Loading branch information
butterunderflow authored Aug 24, 2024
2 parents 969d8ce + 040a41f commit ac0fa47
Show file tree
Hide file tree
Showing 10 changed files with 743 additions and 528 deletions.
33 changes: 17 additions & 16 deletions lib/typing/check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ module U = Unify
module T = Syntax.Parsetree
module I = Types_in
module P = Poly
module R = Read_type
module IdMap = Map.Make (Ident)
module IntMap = Map.Make (Int)

Expand Down Expand Up @@ -278,16 +279,15 @@ and check_cons c env =
and check_field_cons me c env =
let me_typed = check_mod me env in
match get_mod_ty me_typed with
| I.MTMod { constr_defs; _ } ->
let t, id = List.assoc c constr_defs in
| I.MTMod st ->
let t, id = R.find_constr_comp c st in
EFieldCons (me_typed, c, id, P.inst t)
| I.MTFun _ -> failwith "try get field from functor"

and check_field me x env =
let me_typed = check_mod me env in
match get_mod_ty me_typed with
| I.MTMod { val_defs; _ } ->
EField (me_typed, x, P.inst (List.assoc x val_defs))
| I.MTMod st -> EField (me_typed, x, P.inst (R.find_val_comp x st))
| I.MTFun _ -> failwith "try get field from functor"

and check_ann e te env =
Expand Down Expand Up @@ -452,8 +452,7 @@ and check_functor name ext_mt0 me1 env =
and check_mod_field me name env =
let me_typed = check_mod me env in
match get_mod_ty me_typed with
| I.MTMod { mod_defs; _ } ->
MEField (me_typed, name, List.assoc name mod_defs)
| I.MTMod st -> MEField (me_typed, name, R.find_mod_comp name st)
| I.MTFun _ -> failwith "try get field from functor"

and check_mod_apply me0 me1 env =
Expand Down Expand Up @@ -525,12 +524,14 @@ and shift_mt (mt : I.mod_ty) env : I.mod_ty =
(* todo: remove this object *)
inherit [_] Types_in.map as super

method! visit_MTMod () id val_defs constr_defs ty_defs mod_sigs
mod_defs owned_mods =
let shifted_id = get_id_or_default id in
super#visit_MTMod () shifted_id val_defs constr_defs ty_defs
mod_sigs mod_defs
(List.map get_id_or_default owned_mods)
method! visit_MTMod () st =
let shifted_id = get_id_or_default st.id in
super#visit_MTMod ()
{
st with
id = shifted_id;
owned_mods = List.map get_id_or_default st.owned_mods;
}

method! visit_ty_id () (id, name) = (get_id_or_default id, name)

Expand Down Expand Up @@ -574,12 +575,12 @@ and normalize (t : T.ty) (ctx : norm_ctx) (env : Env.t) : I.ty =
let me_typed = check_mod me env in
let mod_ty = get_mod_ty me_typed in
match mod_ty with
| I.MTMod { id; ty_defs; _ } -> (
match I.get_def n ty_defs with
| I.MTMod st -> (
match R.find_ty_def n st with
| I.TDOpaque (_, _)
| I.TDAdt (_, _, _)
| I.TDRecord (_, _, _) ->
TCons ((id, n), tes)
TCons ((st.id, n), tes)
| I.TDAlias (_, te) -> (
match tes with
| [] -> te
Expand Down Expand Up @@ -613,7 +614,7 @@ and normalize_mt (me : T.mod_ty) env : I.mod_ty =
let me_typed = check_mod me env in
let mt = get_mod_ty me_typed in
match mt with
| I.MTMod mt -> List.assoc name mt.mod_sigs
| I.MTMod st -> R.find_mod_sig_comp name st
| I.MTFun (_mt0, _mt1) -> failwith "try get field from functor")
| T.MTSig comps ->
let env' = normalize_msig comps (Env.enter_env env) in
Expand Down
41 changes: 41 additions & 0 deletions lib/typing/read_type.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
module I = Types_in

let get_def_name (td : I.ty_def) =
match td with
| TDOpaque (name, _)
| TDAdt (name, _, _)
| TDRecord (name, _, _)
| TDAlias (name, _) ->
name

let find_ty_def name (st : I.structure) =
try
List.find
(fun td ->
match td with
| I.TDOpaque (name', _)
| I.TDAdt (name', _, _)
| I.TDRecord (name', _, _)
| I.TDAlias (name', _)
when name' = name ->
true
| _ -> false)
st.ty_defs
with
| Not_found -> Report.(error_comp_not_found Type name st)

let find_component kind name map st =
try List.assoc name map with
| Not_found -> Report.error_comp_not_found kind name st

let find_val_comp name (st : I.structure) =
find_component Value name st.val_defs st

let find_constr_comp name (st : I.structure) =
find_component Constructor name st.constr_defs st

let find_mod_comp name (st : I.structure) =
find_component Mod name st.mod_defs st

let find_mod_sig_comp name (st : I.structure) =
find_component ModSig name st.mod_sigs st
7 changes: 7 additions & 0 deletions lib/typing/render.ml
Original file line number Diff line number Diff line change
Expand Up @@ -471,6 +471,13 @@ module MakePP (Config : PPConfig) = struct
pp_ty formatter ?env ty;
Fmt.pp_print_flush formatter ();
Buffer.contents buf

let pp_str_of_mod_expr ?env me =
let buf = Buffer.create 10 in
let formatter = Fmt.formatter_of_buffer buf in
pp_mod formatter ?env me;
Fmt.pp_print_flush formatter ();
Buffer.contents buf
end

module ShowAllConfig : PPConfig = struct
Expand Down
36 changes: 32 additions & 4 deletions lib/typing/report.ml
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,24 @@ exception UnificationError of (T.ty * T.ty)

exception OccurError of string * T.ty

exception ComponentInCompatible of string * T.bind_ty * T.bind_ty
type incompatible_kind =
| Value
| Type
| Mod
| ModSig
| Constructor

exception ComponentInCompatible0 of string * T.bind_ty * T.bind_ty

exception ComponentNotFound of incompatible_kind * string * T.structure

exception LocatedErr of exn * Lexing.position * Lexing.position * Env.t

let error_incompatible name vt0 vt1 =
raise (ComponentInCompatible (name, vt0, vt1))
let error_incompatible0 name vt0 vt1 =
raise (ComponentInCompatible0 (name, vt0, vt1))

let error_comp_not_found kind name mt =
raise (ComponentNotFound (kind, name, mt))

let error_unification t0 t1 = raise (UnificationError (t0, t1))

Expand Down Expand Up @@ -42,11 +54,27 @@ let report_error ?env (err : exn) =
Printf.printf "type variable %s occured in " tvn;
PP.pp_ty Format.std_formatter te;
None
| ComponentInCompatible (name, (_, t0), (_, t1)) ->
| ComponentInCompatible0 (name, (_, t0), (_, t1)) ->
Printf.printf
"Value component %s has type `%s`, which is not compatible with `%s`"
name (PP.pp_str_of_ty t0) (PP.pp_str_of_ty t1);
None
| ComponentNotFound (kind, name, { id = mid; _ }) ->
Printf.printf "%s component %s not exists in module %s"
(match kind with
| Value -> "Value"
| Type -> "Type definition"
| Mod -> "Module"
| ModSig -> "Module Signature"
| Constructor -> "Constructor")
name
(match env with
| Some env -> (
match Env.lookup_hint mid env with
| Some me -> PP.pp_str_of_mod_expr me
| None -> Printf.sprintf "{ id = %d}" mid)
| None -> Printf.sprintf "%d" mid);
None
| Failure msg ->
Printf.printf "%s\n" msg;
None
Expand Down
60 changes: 22 additions & 38 deletions lib/typing/subtype.ml
Original file line number Diff line number Diff line change
@@ -1,23 +1,25 @@
module I = Types_in
module R = Read_type
module P = Poly

let build_mod_correspond mt0 mt1 =
(* a map which correspond mt0 with mt1 *)
let mid_map = ref [] in
let rec collect_mid_maping mt0 mt1 =
match (mt0, mt1) with
| ( I.MTMod { id = id0; mod_defs = mds0; _ },
I.MTMod { id = id1; mod_defs = mds1; _ } ) ->
mid_map := (id1, id0) :: !mid_map;
| I.MTMod st0, I.MTMod st1 ->
mid_map := (st1.id, st0.id) :: !mid_map;
List.iter
(fun (name, md1) ->
let md0 = List.assoc name mds0 in
let md0 = R.find_mod_comp name st0 in
collect_mid_maping md0 md1)
mds1
st1.mod_defs
| I.MTFun (argt0, mt0), I.MTFun (argt1, mt1) ->
collect_mid_maping argt0 argt1;
collect_mid_maping mt0 mt1
| _ -> failwith "subtype check error"
| _ ->
failwith
"subtype check error, structure is not compatible with functor"
in
collect_mid_maping mt0 mt1;
!mid_map
Expand Down Expand Up @@ -49,30 +51,12 @@ let compatible mt0 mt1 =
let alias_map : (I.ty_id * I.ty) list ref = ref [] in
let rec compatible_aux mt0 mt1 : unit =
match (mt0, mt1) with
| ( I.MTMod
{
val_defs = vds0;
constr_defs = cds0;
ty_defs = tds0;
mod_defs = mds0;
mod_sigs = _ms0;
id = id0;
_;
},
I.MTMod
{
val_defs = vds1;
constr_defs = cds1;
ty_defs = tds1;
mod_defs = mds1;
mod_sigs = ms1;
_;
} ) ->
| I.MTMod st0, I.MTMod st1 ->
List.iter
(fun td1 ->
match td1 with
| I.TDOpaque (name, paras) -> (
let td0 = I.get_def name tds0 in
let td0 = R.find_ty_def name st0 in
match td0 with
| I.TDOpaque (_, paras0)
| I.TDAdt (_, paras0, _)
Expand All @@ -83,23 +67,23 @@ let compatible mt0 mt1 =
type"
| I.TDAlias (_, ty0) -> (
match paras with
| [] -> alias_map := ((id0, name), ty0) :: !alias_map
| [] -> alias_map := ((st0.id, name), ty0) :: !alias_map
| _ :: _ -> failwith "type alias has parameter"))
| _ ->
let td0 = I.get_def (I.get_def_name td1) tds0 in
let td0 = R.(find_ty_def (get_def_name td1) st0) in
if td0 <> Alias.dealias_td td1 !alias_map then
failwith "a type def component not compatible")
tds1;
st1.ty_defs;
List.iter
(fun (name, vt1) ->
let vt0 = List.assoc name vds0 in
let vt0 = R.find_val_comp name st0 in
if
P.align_inst vt0 <> P.align_inst (Alias.dealias vt1 !alias_map)
then Report.error_incompatible name vt0 vt1)
vds1;
then Report.error_incompatible0 name vt0 vt1)
st1.val_defs;
List.iter
(fun (name, (cd1, cid1)) ->
let cd0, cid0 = List.assoc name cds0 in
let cd0, cid0 = R.find_constr_comp name st0 in
if
cid1 <> cid0
|| P.align_inst cd0
Expand All @@ -108,13 +92,13 @@ let compatible mt0 mt1 =
failwith
(Printf.sprintf "a constructor component `%s` not compatible"
name))
cds1;
st1.constr_defs;
List.iter
(fun (name, md1) -> compatible_aux (List.assoc name mds0) md1)
mds1;
(fun (name, md1) -> compatible_aux (R.find_mod_comp name st0) md1)
st1.mod_defs;
List.iter
(fun (name, ms1) -> compatible_aux (List.assoc name mds0) ms1)
ms1
(fun (name, ms1) -> compatible_aux (R.find_mod_comp name st0) ms1)
st1.mod_sigs
| I.MTFun (argt0, mt0), I.MTFun (argt1, mt1) ->
compatible_aux argt1 argt0;
compatible_aux mt0 mt1
Expand Down
45 changes: 12 additions & 33 deletions lib/typing/types_in.ml
Original file line number Diff line number Diff line change
Expand Up @@ -31,17 +31,19 @@ and ty_def =
| TDRecord of string * type_paras * (string * ty) list
| TDAlias of string * ty

and structure = {
id : int; (* give every module type an identity *)
val_defs : (string * bind_ty) list;
constr_defs :
(string * (bind_ty * int (* constructor id of a adt *))) list;
ty_defs : ty_def list;
mod_sigs : (string * mod_ty) list;
mod_defs : (string * mod_ty) list;
owned_mods : int list;
}

and mod_ty =
| MTMod of {
id : int; (* give every module type an identity *)
val_defs : (string * bind_ty) list;
constr_defs :
(string * (bind_ty * int (* constructor id of a adt *))) list;
ty_defs : ty_def list;
mod_sigs : (string * mod_ty) list;
mod_defs : (string * mod_ty) list;
owned_mods : int list;
}
| MTMod of structure
| MTFun of (mod_ty * mod_ty)
[@@deriving
sexp,
Expand Down Expand Up @@ -86,26 +88,3 @@ let string_ty = TCons (mk_root_tid "string", [])
let bool_ty = TCons (mk_root_tid "bool", [])

let unit_ty = TCons (mk_root_tid "unit", [])

let same_def td0 td1 = td0 = td1

let get_def_name (td : ty_def) =
match td with
| TDOpaque (name, _)
| TDAdt (name, _, _)
| TDRecord (name, _, _)
| TDAlias (name, _) ->
name

let get_def name ty_def_group =
List.find
(fun td ->
match td with
| TDOpaque (name', _)
| TDAdt (name', _, _)
| TDRecord (name', _, _)
| TDAlias (name', _)
when name' = name ->
true
| _ -> false)
ty_def_group
4 changes: 1 addition & 3 deletions lib/typing/unify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,6 @@ open Types_in
module SMap = Map.Make (Ident)
module Tree = Syntax.Parsetree

exception OccurError of (tv ref * ty)

exception IllFormType

let occurs (tpv : tv ref) (te : ty) : unit =
Expand Down Expand Up @@ -66,7 +64,7 @@ let occur (tpv : tv ref) (te : ty) : bool =
occurs tpv te;
false
with
| OccurError (_tpv, _te) -> true
| Report.OccurError (_tpv, _te) -> true

(* initialize forward definition *)
let () = Env.occur := occur
2 changes: 0 additions & 2 deletions lib/typing/unify.mli
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
val unify : Types_in.ty -> Types_in.ty -> unit

val occur : Types_in.tv ref -> Types_in.ty -> bool

exception OccurError of (Types_in.tv ref * Types_in.ty)
Loading

0 comments on commit ac0fa47

Please sign in to comment.