Skip to content

Commit

Permalink
Address James' feedback
Browse files Browse the repository at this point in the history
  • Loading branch information
dhil committed Sep 29, 2024
1 parent 270b21d commit 376363a
Show file tree
Hide file tree
Showing 6 changed files with 23 additions and 10 deletions.
5 changes: 1 addition & 4 deletions core/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -247,9 +247,6 @@ let make_effect_var : is_dot:bool -> ParserPosition.t -> Datatype.row_var

let dummy_phrase pos = with_pos pos (Sugartypes.RecordLit ([], None))

let fresh_abstract_identity : unit -> exn
= fun () -> let exception E in E

module MutualBindings = struct

type mutual_bindings =
Expand Down Expand Up @@ -542,7 +539,7 @@ signature:
| SIG sigop COLON datatype { with_pos $loc ($2, datatype $4) }

typedecl:
| TYPENAME CONSTRUCTOR typeargs_opt { alias $loc $2 $3 (Typename ( WithPos.make (Datatype.Abstract (fresh_abstract_identity ())), None)) }
| TYPENAME CONSTRUCTOR typeargs_opt { alias $loc $2 $3 (Typename ( WithPos.make (Datatype.Abstract (Gensym.gensym ())), None)) }
| TYPENAME CONSTRUCTOR typeargs_opt EQ datatype { alias $loc $2 $3 (Typename ( $5 , None)) }
| EFFECTNAME CONSTRUCTOR typeargs_opt EQ LBRACE erow RBRACE { alias $loc $2 $3 (Effectname ( $6 , None)) }
| EFFECTNAME CONSTRUCTOR typeargs_opt EQ effect_app { alias $loc $2 $3 (Effectname (([], $5), None)) }
Expand Down
3 changes: 1 addition & 2 deletions core/sugartypes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -191,9 +191,8 @@ type fieldconstraint = Readonly | Default
[@@deriving show]

module Datatype = struct
let pp_exn fmt _ = Format.fprintf fmt "exn"
type t =
| Abstract of exn
| Abstract of Gensym.t
| TypeVar of SugarTypeVar.t
| QualifiedTypeApplication of Name.t list * type_arg list
| Function of with_pos list * row * with_pos
Expand Down
2 changes: 1 addition & 1 deletion core/types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,7 @@ and typ =
| Table of (Temporality.t * typ * typ * typ)
| Lens of Lens.Type.t
| ForAll of (Quantifier.t list * typ)
| Abstract of exn
| Abstract of Gensym.t
(* Effect *)
| Effect of row
| Operation of (typ * typ * DeclaredLinearity.t)
Expand Down
2 changes: 1 addition & 1 deletion core/types.mli
Original file line number Diff line number Diff line change
Expand Up @@ -143,7 +143,7 @@ and typ =
| Table of (Temporality.t * typ * typ * typ)
| Lens of Lens.Type.t
| ForAll of (Quantifier.t list * typ)
| Abstract of exn
| Abstract of Utility.Gensym.t
(* Effect *)
| Effect of row
| Operation of (typ * typ * DeclaredLinearity.t)
Expand Down
4 changes: 2 additions & 2 deletions core/unify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ let rec eq_types : (datatype * datatype) -> bool =
| Abstract abs ->
begin match unalias t2 with
| Abstract abs' ->
abs == abs' (* pointer equality *)
Gensym.equal abs abs'
&& (let [@ocaml.warning "-8"]Alias (_, (_, _, tyargs, _), _) = t1 in
let [@ocaml.warning "-8"]Alias (_, (_, _, tyargs', _), _) = t2 in
List.for_all2 (fun (_tyk, ty) (_tyk', ty') -> eq_types (ty, ty')) tyargs tyargs')
Expand Down Expand Up @@ -611,7 +611,7 @@ let rec unify' : unify_env -> (datatype * datatype) -> unit =
| Abstract _, _ | _, Abstract _ ->
failwith "freestanding Abstract (must be under an alias)"
| Alias (_, _, Abstract abs), Alias (_, _, Abstract abs') ->
if abs == abs'
if Gensym.equal abs abs'
then let [@ocaml.warning "-8"]Alias (_, (_, _, tyargs, _), _) = t1 in
let [@ocaml.warning "-8"]Alias (_, (_, _, tyargs', _), _) = t2 in
List.iter2 (fun tyargs tyargs' -> unify_type_args' rec_env (tyargs, tyargs')) tyargs tyargs'
Expand Down
17 changes: 17 additions & 0 deletions core/utility.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1087,6 +1087,23 @@ let pair_fresh_names ?prefix:pfx list =
let refresh_names =
graph_func (fun x -> gensym ~prefix:x ())

(** Generates an opaque unique identity. TODO(dhil): reconcile the
above (legacy) gensym with this. *)
module Gensym: sig
type t
val gensym : unit -> t (* generates a unique identity *)
val to_string : t -> string (* string representation; used in codegen *)
val equal : t -> t -> bool (* decides whether two identities are the same *)
val pp : Format.formatter -> 'a -> unit
end = struct
type t = exn
let gensym () =
let exception E in E
let to_string exn = Printf.sprintf "%d" (Hashtbl.hash exn)
let equal exn exn' = exn == exn'
let pp fmt exn = Format.fprintf fmt "%s" (to_string exn)
end

(** Return [true] if any element of the given list is [true] *)
let any_true = List.exists identity

Expand Down

0 comments on commit 376363a

Please sign in to comment.