Skip to content

Commit

Permalink
Merge branch 'omit-list-type'
Browse files Browse the repository at this point in the history
  • Loading branch information
@gfngfn
gfngfn committed Sep 16, 2020
2 parents b60d0c0 + 0856deb commit 2c2405b
Show file tree
Hide file tree
Showing 5 changed files with 86 additions and 97 deletions.
135 changes: 77 additions & 58 deletions src/primitives.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -193,70 +193,89 @@ let make_constructor_id ctor =
let vid_option = TypeID.Variant.fresh "option"


let option_type (ty : mono_type) : mono_type =
(dr, DataType(TypeID.Variant(vid_option), [ty]))


let initial_environment =
let add_variant_types vntdefs (tyenv, gmap) =
let tyenv : Typeenv.t =
vntdefs |> List.fold_left (fun tyenv vntdef ->
let (tynm, vid, bids, ctordefs) = vntdef in
let pkd = TypeConv.kind_of_arity (List.length bids) in
let tyenv = tyenv |> Typeenv.add_variant_type tynm vid pkd in
ctordefs |> List.fold_left (fun tyenv ctordef ->
let (ctor, paramtys) = ctordef in
let ctorentry =
{
belongs = vid;
constructor_id = make_constructor_id ctor;
type_variables = bids;
parameter_types = paramtys;
}
in
tyenv |> Typeenv.add_constructor ctor ctorentry
) tyenv
let vid_list = TypeID.Variant.fresh "list"


let option_type (rng : Range.t) (ty : ('a, 'b) typ) : ('a, 'b) typ =
(rng, DataType(TypeID.Variant(vid_option), [ty]))


let list_type (rng : Range.t) (ty : ('a, 'b) typ) : ('a, 'b) typ =
(rng, DataType(TypeID.Variant(vid_list), [ty]))


let add_variant_types vntdefs (tyenv, gmap) =
let tyenv : Typeenv.t =
vntdefs |> List.fold_left (fun tyenv vntdef ->
let (tynm, vid, bids, ctordefs) = vntdef in
let pkd = TypeConv.kind_of_arity (List.length bids) in
let tyenv = tyenv |> Typeenv.add_variant_type tynm vid pkd in
ctordefs |> List.fold_left (fun tyenv ctordef ->
let (ctor, paramtys) = ctordef in
let ctorentry =
{
belongs = vid;
constructor_id = make_constructor_id ctor;
type_variables = bids;
parameter_types = paramtys;
}
in
tyenv |> Typeenv.add_constructor ctor ctorentry
) tyenv
in
(tyenv, gmap)
) tyenv
in
let add_operators (ops : (string * poly_type * string) list) ((tyenv, gmap) : Typeenv.t * global_name_map) : Typeenv.t * global_name_map =
let tyenv =
ops |> List.fold_left (fun tyenv (x, pty, target) ->
let name = OutputIdentifier.Operator(OutputIdentifier.operator target) in
tyenv |> Typeenv.add_val x pty name
) tyenv
in
(tyenv, gmap)
in
let add_primitives (prims : primitive_definition list) ((tyenv, gmap) : Typeenv.t * global_name_map) : Typeenv.t * global_name_map =
prims |> List.fold_left (fun (tyenv, gmap) primdef ->
match primdef.source with
| None ->
(tyenv, gmap)

| Some(srcdef) ->
let targetdef = primdef.target in
let gname =
let arity = List.length targetdef.parameters in
match OutputIdentifier.generate_global targetdef.target_name ~arity:arity ~has_option:false with
| None -> assert false
| Some(gname) -> gname
in
let tyenv = tyenv |> Typeenv.add_val srcdef.identifier srcdef.typ (OutputIdentifier.Global(gname)) in
let gmap = gmap |> GlobalNameMap.add gname primitive_module_name in
(tyenv, gmap)
) (tyenv, gmap)
(tyenv, gmap)


let add_operators (ops : (string * poly_type * string) list) ((tyenv, gmap) : Typeenv.t * global_name_map) : Typeenv.t * global_name_map =
let tyenv =
ops |> List.fold_left (fun tyenv (x, pty, target) ->
let name = OutputIdentifier.Operator(OutputIdentifier.operator target) in
tyenv |> Typeenv.add_val x pty name
) tyenv
in
(tyenv, gmap)


let add_primitives (prims : primitive_definition list) ((tyenv, gmap) : Typeenv.t * global_name_map) : Typeenv.t * global_name_map =
prims |> List.fold_left (fun (tyenv, gmap) primdef ->
match primdef.source with
| None ->
(tyenv, gmap)

| Some(srcdef) ->
let targetdef = primdef.target in
let gname =
let arity = List.length targetdef.parameters in
match OutputIdentifier.generate_global targetdef.target_name ~arity:arity ~has_option:false with
| None -> assert false
| Some(gname) -> gname
in
let tyenv = tyenv |> Typeenv.add_val srcdef.identifier srcdef.typ (OutputIdentifier.Global(gname)) in
let gmap = gmap |> GlobalNameMap.add gname primitive_module_name in
(tyenv, gmap)
) (tyenv, gmap)


let initial_environment =
(Typeenv.empty, GlobalNameMap.empty)
|> add_variant_types [
let bid = BoundID.fresh () in
KindStore.register_bound_id bid UniversalKind;
("option", vid_option, [bid], [
("None", []);
("Some", [(dr, TypeVar(Bound(bid)))])
]);
begin
let bid = BoundID.fresh () in
KindStore.register_bound_id bid UniversalKind;
("option", vid_option, [bid], [
("None", []);
("Some", [(dr, TypeVar(Bound(bid)))])
])
end;
begin
let bid = BoundID.fresh () in
KindStore.register_bound_id bid UniversalKind;
("list", vid_list, [bid], [
(* Here is no constructor definition
because `ListNil` and `ListCons` are provided for type `untyped_ast`. *)
])
end;
]
|> add_operators [
("&&", tylogic, "and");
Expand Down
4 changes: 3 additions & 1 deletion src/primitives.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,8 @@ type primitive_definition = {

val primitive_definitions : primitive_definition list

val option_type : mono_type -> mono_type
val option_type : Range.t -> ('a, 'b) typ -> ('a, 'b) typ

val list_type : Range.t -> ('a, 'b) typ -> ('a, 'b) typ

val initial_environment : Typeenv.t * global_name_map
1 change: 0 additions & 1 deletion src/syntax.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -297,7 +297,6 @@ and ('a, 'b) typ_main =
| EffType of ('a, 'b) effect * ('a, 'b) typ
| TypeVar of 'a
| ProductType of (('a, 'b) typ) TupleList.t
| ListType of ('a, 'b) typ
| DataType of TypeID.t * (('a, 'b) typ) list
| RecordType of (('a, 'b) typ) LabelAssoc.t

Expand Down
12 changes: 0 additions & 12 deletions src/typeConv.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -172,11 +172,6 @@ let lift_scheme (rngf : Range.t -> Range.t) (levpred : int -> bool) (ty : mono_t
let pty = (rngf rng, ProductType(ptys)) in
(bbidset, pty)

| ListType(ty0) ->
let (bbidset, pty0) = aux ty0 in
let pty = (rngf rng, ListType(pty0)) in
(bbidset, pty)

| RecordType(labmap) ->
let (bbidset, plabmap) = aux_label_assoc labmap in
let pty = (rngf rng, RecordType(plabmap)) in
Expand Down Expand Up @@ -303,9 +298,6 @@ fun intern intern_row pty ->
let tys = ptys |> TupleList.map aux in
(rng, ProductType(tys))

| ListType(pty0) ->
(rng, ListType(aux pty0))

| RecordType(plabmap) ->
let labmap = plabmap |> LabelAssoc.map aux in
(rng, RecordType(labmap))
Expand Down Expand Up @@ -627,10 +619,6 @@ fun showtv showrv ty ->
let ss = tys |> TupleList.to_list |> List.map aux in
Printf.sprintf "(%s)" (String.concat ", " ss)

| ListType(ty0) ->
let s0 = aux ty0 in
Printf.sprintf "list<%s>" s0

| RecordType(labmap) ->
begin
match show_label_assoc ~prefix:"" ~suffix:" :" showtv showrv labmap with
Expand Down
31 changes: 6 additions & 25 deletions src/typechecker.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -311,9 +311,6 @@ let occurs (fid : FreeID.t) (ty : mono_type) : bool =
| ProductType(tys) ->
tys |> TupleList.to_list |> aux_list

| ListType(ty) ->
aux ty

| RecordType(labmap) ->
aux_label_assoc labmap

Expand Down Expand Up @@ -406,9 +403,6 @@ let occurs_row (frid : FreeRowID.t) (labmap : mono_type LabelAssoc.t) =
| ProductType(tys) ->
tys |> TupleList.to_list |> aux_list

| ListType(ty) ->
aux ty

| RecordType(labmap) ->
aux_label_assoc labmap

Expand Down Expand Up @@ -450,7 +444,6 @@ fun tyidp tvp oidset ->
| BaseType(_) -> false
| PidType(typid) -> aux_pid typid
| EffType(tyeff, tysub) -> aux_effect tyeff || aux tysub
| ListType(tysub) -> aux tysub
| ProductType(tys) -> tys |> TupleList.to_list |> List.exists aux

| FuncType(tydoms, mndlabmap, optrow, tycod) ->
Expand Down Expand Up @@ -629,9 +622,6 @@ let unify (tyact : mono_type) (tyexp : mono_type) : unit =
| (ProductType(tys1), ProductType(tys2)) ->
aux_list (tys1 |> TupleList.to_list) (tys2 |> TupleList.to_list)

| (ListType(ty1), ListType(ty2)) ->
aux ty1 ty2

| (DataType(TypeID.Variant(vid1), tyargs1), DataType(TypeID.Variant(vid2), tyargs2)) ->
if TypeID.Variant.equal vid1 vid2 then
aux_list tyargs1 tyargs2
Expand Down Expand Up @@ -891,7 +881,7 @@ let type_of_base_constant (rng : Range.t) (bc : base_constant) =
| Float(_) -> (rng, BaseType(FloatType))
| BinaryByString(_)
| BinaryByInts(_) -> (rng, BaseType(BinaryType))
| String(_) -> (rng, ListType((Range.dummy "string_literal", BaseType(CharType))))
| String(_) -> Primitives.list_type rng (Range.dummy "string_literal", BaseType(CharType))
| Char(_) -> (rng, BaseType(CharType))


Expand Down Expand Up @@ -991,8 +981,6 @@ and decode_manual_type_scheme (k : TypeID.t -> unit) (pre : pre) (mty : manual_t
| ("binary", _) -> invalid rng "binary" ~expect:0 ~actual:len_actual
| ("char", []) -> BaseType(CharType)
| ("char", _) -> invalid rng "char" ~expect:0 ~actual:len_actual
| ("list", [ty]) -> ListType(ty)
| ("list", _) -> invalid rng "list" ~expect:1 ~actual:len_actual
| ("pid", [ty]) -> PidType(Pid(ty))
| ("pid", _) -> invalid rng "pid" ~expect:1 ~actual:len_actual
| _ -> raise_error (UndefinedTypeName(rng, tynm))
Expand Down Expand Up @@ -1194,7 +1182,7 @@ and add_labeled_optional_parameters_to_type_environment (pre : pre) (optbinders
match utdefault with
| None ->
let ty_outer = fresh_type_variable pre.level UniversalKind (Range.dummy "optional") in
unify ty_inner (Primitives.option_type ty_outer);
unify ty_inner (Primitives.option_type (Range.dummy "option") ty_outer);
(ty_outer, None)

| Some(utast) ->
Expand Down Expand Up @@ -1378,13 +1366,13 @@ and typecheck (pre : pre) ((rng, utastmain) : untyped_ast) : mono_type * ast =

| ListNil ->
let tysub = fresh_type_variable pre.level UniversalKind (Range.dummy "list-nil") in
let ty = (rng, ListType(tysub)) in
let ty = Primitives.list_type rng tysub in
(ty, IListNil)

| ListCons(utast1, utast2) ->
let (ty1, e1) = typecheck pre utast1 in
let (ty2, e2) = typecheck pre utast2 in
unify ty2 (Range.dummy "list-cons", ListType(ty1));
unify ty2 (Primitives.list_type (Range.dummy "list-cons") ty1);
(ty2, IListCons(e1, e2))

| Case(utast0, branches) ->
Expand Down Expand Up @@ -1586,15 +1574,15 @@ and typecheck_pattern (pre : pre) ((rng, patmain) : untyped_pattern) : mono_type
| PListNil ->
let ty =
let tysub = fresh_type_variable pre.level UniversalKind rng in
(rng, ListType(tysub))
Primitives.list_type rng tysub
in
(ty, IPListNil, BindingMap.empty)

| PListCons(pat1, pat2) ->
let (ty1, ipat1, bindmap1) = typecheck_pattern pre pat1 in
let (ty2, ipat2, bindmap2) = typecheck_pattern pre pat2 in
let bindmap = binding_map_union rng bindmap1 bindmap2 in
unify ty2 (Range.dummy "pattern-cons", ListType(ty1));
unify ty2 (Primitives.list_type (Range.dummy "pattern-cons") ty1);
(ty2, IPListCons(ipat1, ipat2), bindmap)

| PTuple(pats) ->
Expand Down Expand Up @@ -1827,9 +1815,6 @@ and subtype_poly_type_scheme (wtmap : WitnessMap.t) (internbid : BoundID.t -> po
| (ProductType(ptys1), ProductType(ptys2)) ->
aux_list (TupleList.to_list ptys1) (TupleList.to_list ptys2)

| (ListType(ptysub1), ListType(ptysub2)) ->
aux ptysub1 ptysub2

| (RecordType(plabmap1), RecordType(plabmap2)) ->
aux_label_assoc plabmap1 plabmap2

Expand Down Expand Up @@ -2083,9 +2068,6 @@ and poly_type_equal (pty1 : poly_type) (pty2 : poly_type) : bool =
| (RecordType(plabmap1), RecordType(plabmap2)) ->
aux_label_assoc plabmap1 plabmap2

| (ListType(pty1), ListType(pty2)) ->
aux pty1 pty2

| (DataType(TypeID.Variant(vid1), ptyargs1), DataType(TypeID.Variant(vid2), ptyargs2)) ->
TypeID.Variant.equal vid1 vid2 && aux_list ptyargs1 ptyargs2

Expand Down Expand Up @@ -2529,7 +2511,6 @@ and substitute_poly_type (wtmap : WitnessMap.t) (pty : poly_type) : poly_type =
| EffType(peff, ptysub) -> EffType(aux_effect peff, aux ptysub)
| TypeVar(_) -> ptymain
| ProductType(ptys) -> ProductType(ptys |> TupleList.map aux)
| ListType(ptysub) -> ListType(aux ptysub)

| FuncType(ptydoms, pmndlabmap, poptrow, ptycod) ->
FuncType(ptydoms |> List.map aux, pmndlabmap |> LabelAssoc.map aux, aux_option_row poptrow, aux ptycod)
Expand Down

0 comments on commit 2c2405b

Please sign in to comment.