Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generative labels #1169

Open
wants to merge 72 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
72 commits
Select commit Hold shift + click to select a range
b1969a3
effectalias init
Orbion-J May 13, 2022
49a9a61
desalias inline
Orbion-J May 13, 2022
36a488f
alias = effectname and typename | init
Orbion-J May 18, 2022
dbb6b5b
merge into 1 construct ok; still 2 contexts
Orbion-J May 19, 2022
84ffd9b
merge type and effect aliases contexts
Orbion-J May 20, 2022
5150615
effectname body desugared into effectname
Orbion-J May 20, 2022
ee1651e
Merge branch 'merge-typenames-effectnames'
Orbion-J May 20, 2022
a2d8bdc
Revert "desalias inline"
Orbion-J May 23, 2022
419aca4
Revert "effectname body desugared into effectname"
Orbion-J May 23, 2022
6e8c0df
"effectname" in links-mode.el
Orbion-J May 24, 2022
1355a93
cleaning before pr
Orbion-J May 24, 2022
50edb64
re-cleaning
Orbion-J May 24, 2022
ce200de
effectname -> typename _::Kind
Orbion-J May 27, 2022
c0c3e5b
Update bin/repl.ml
Orbion-J May 27, 2022
eace411
Update bin/repl.ml
Orbion-J May 27, 2022
93b2cf1
Update bin/repl.ml
Orbion-J May 27, 2022
1736097
Update bin/repl.ml
Orbion-J May 27, 2022
bb0fb30
Update bin/repl.ml
Orbion-J May 27, 2022
6206a6b
Update core/desugarDatatypes.mli
Orbion-J May 27, 2022
9a499fc
Update bin/repl.ml
Orbion-J May 27, 2022
c45fbbc
Update core/defaultAliases.ml
Orbion-J May 27, 2022
832a424
Update core/desugarDatatypes.ml
Orbion-J May 27, 2022
0bd30cd
Update core/desugarDatatypes.ml
Orbion-J May 27, 2022
35e50e8
Update core/desugarDatatypes.ml
Orbion-J May 27, 2022
14df529
rename alias_env -> tycon_env as originally
Orbion-J May 27, 2022
31dffbb
Merge branch 'master' of github.com:Orbion-J/links
Orbion-J May 27, 2022
3489b8a
idem
Orbion-J May 27, 2022
b35a3da
fixes & add primary kind in aliases
Orbion-J May 30, 2022
69f2920
new error kind mismatch
Orbion-J Jun 1, 2022
f88808d
fresh label : init
Orbion-J Jun 3, 2022
5bce834
local labels : working
Orbion-J Jun 13, 2022
dccac21
fix : embeded errors
Orbion-J Jun 13, 2022
fd82138
fixes
Orbion-J Jun 14, 2022
806570a
fix label projections
Orbion-J Jun 14, 2022
7dc5f76
fix : underscore in effect app
Orbion-J Jun 15, 2022
ca580a5
various fixes
Orbion-J Jun 15, 2022
e118c0e
short type in effectname + short fun non desugar
Orbion-J Jun 16, 2022
109ca66
comment
Orbion-J Jun 16, 2022
0ab606c
Merge branch 'master' into master
Orbion-J Jun 16, 2022
dc0682f
always desugar op type with type application
Orbion-J Jun 16, 2022
01d9a09
correction tests
Orbion-J Jun 16, 2022
56ac19b
erase local labels out of scope (err when nested)
Orbion-J Jun 20, 2022
7a9a437
nested fresh label
Orbion-J Jun 22, 2022
4b6d3f9
fix stack overflow w/ points + clean debug
Orbion-J Jun 22, 2022
fd52e08
alias stuff
Orbion-J Jun 23, 2022
aa73727
functional
Orbion-J Jun 24, 2022
99c0878
remove wrong UnboundTyCon error
Orbion-J Jun 24, 2022
07040be
Merge branch 'links-lang:master' into master
Orbion-J Jun 24, 2022
6d907e7
default arg in repl
Orbion-J Jun 24, 2022
75a4f73
Merge branch 'master' of github.com:Orbion-J/links
Orbion-J Jun 24, 2022
82641fc
alias stuff + context management
Orbion-J Jun 24, 2022
b9e25e6
wip
Orbion-J Jun 27, 2022
571ffa2
Merge branch 'master' into fresh-label
Orbion-J Jun 27, 2022
c76a41e
Merge branch 'links-lang:master' into fresh-label
Orbion-J Jun 27, 2022
38f7f3e
fold_left_map in ListUtils (not in Ocaml < 4.11)
Orbion-J Jun 27, 2022
58919f5
Merge branch 'fresh-label' of github.com:Orbion-J/links into fresh-label
Orbion-J Jun 27, 2022
6a5e7da
fix in test
Orbion-J Jun 27, 2022
310ebb4
fixes rule-check ocamlformat
Orbion-J Jun 27, 2022
152b59a
fixes rule-check ocamlformat bis
Orbion-J Jun 27, 2022
de09626
fix tests unit labels
Orbion-J Jun 27, 2022
667a886
fix Labels in tests
Orbion-J Jun 28, 2022
61ad662
fix Labels tests
Orbion-J Jun 28, 2022
589a7db
fix labels tests
Orbion-J Jun 28, 2022
3ea8ddf
fix labels tests
Orbion-J Jun 28, 2022
ab3ab86
fix labels tests
Orbion-J Jun 28, 2022
5e5dae6
change pollution test
Orbion-J Jul 22, 2022
d31a6fe
Merge branch 'fresh-label' of github.com:Orbion-J/links into Orbion-J…
dhil Jan 31, 2023
066af32
Refactor
dhil Jan 31, 2023
478c2a2
Fix bug and generalise.
dhil Jan 31, 2023
717eba0
Fix unique label resolution
dhil Jan 31, 2023
ec92181
Fix session exceptions regression
dhil Jan 31, 2023
192c437
Slight hack to make unique labels work properly with elaborated modules.
dhil Jan 31, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Fix bug and generalise.
This commit fixes a regression introduced by the previous commit,
wherein numeric labels wouldn't get looked up correctly in
`Label.{Map,Set}`.

This commit also generalises `fresh` such that it can be used locally
within a binding context. Furthermore, it changes the syntax such that
it no longer introduces encloses a list of bindings, but instead uses
the standard block-structured scope of Links.
  • Loading branch information
dhil committed Jan 31, 2023
commit 478c2a2e0e695e000717857c0408bdb3cc082969
16 changes: 8 additions & 8 deletions core/desugarLabels.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ open Sugartypes
module Env = Label.Env

let visitor =
object (self)
object (_self)
inherit SugarTraversals.map as super

val mutable label_env : Env.t = Env.empty
Expand All @@ -18,12 +18,10 @@ let visitor =
| _ -> failwith ("The local label " ^ Label.show lbl ^ " is not bound")

method! bindingnode = function
| FreshLabel (labels, decls) ->
| FreshLabel labels ->
let labels = List.map Label.bind_local labels in
label_env <- Env.bind_labels labels label_env ;
let decls = List.map self#binding decls in
label_env <- Env.unbind_labels labels label_env ;
FreshLabel(labels, decls)
FreshLabel labels
| b -> super#bindingnode b

end
Expand All @@ -33,9 +31,11 @@ let program p = visitor#program p
let sentence = function
| Definitions bs ->
let bs' = visitor#list (fun o b -> o#binding b) bs in
Definitions bs'
| Expression p -> Expression p
| Directive d -> Directive d
Definitions bs'
| Expression p ->
let p' = visitor#phrase p in
Expression p'
| Directive d -> Directive d

module Untyped = struct
open Transform.Untyped
Expand Down
45 changes: 31 additions & 14 deletions core/label.ml
Original file line number Diff line number Diff line change
@@ -1,6 +1,13 @@
open Utility
open CommonTypes

let show_unique_labels_idents =
Settings.(flag ~default:false "show_unique_labels_idents"
|> privilege `User
|> synopsis "Show the internal numeric identifier for each unique label"
|> convert parse_bool
|> sync)

let internal_error message =
Errors.internal_error ~filename:"label.ml" ~message
let local_error show lbl =
Expand Down Expand Up @@ -43,7 +50,10 @@ module Label = struct
type label = t

let show = function
| Local (name, id) -> "`" ^ name ^ "<" ^ Uid.show id ^ ">"
| Local (name, id) ->
if Settings.get show_unique_labels_idents
then Printf.sprintf "`%s<%s>" name (Uid.show id)
else Printf.sprintf "`%s" name
| Global name -> name
| Number n -> string_of_int n

Expand All @@ -54,21 +64,25 @@ module Label = struct
| Number n -> string_of_int n
end

let make_local ?(uid=Uid.Free) name = Local (name, uid)

let make_global name = Global name

let make ?(local=false) name =
if local
then make_local name
else make_global name

let of_int i = Number i

let to_int = function
| Number n -> n
| Global i -> int_of_string i
| l -> raise (local_error show l)

let make_local ?(uid=Uid.Free) name = Local (name, uid)

let make_global name = Global name

let make textual_name =
let is_digit ch =
Char.code ch >= 48 && Char.code ch <= 57
in
if String.for_all is_digit textual_name
then of_int (int_of_string textual_name)
else make_global textual_name

let name = function
| Local (name,_) -> "`"^name
| Global name -> name
Expand All @@ -79,9 +93,12 @@ module Label = struct
| Local (_, uid), Local (_, uid') -> Uid.compare uid uid'
| Global g, Global g' -> String.compare g g'
| Local _, Global _ -> 1
| Number n, Number n' -> Int.compare n n'
| Local _, Number _ -> 1
| _, _ -> -1
| Global _, Number _ -> 1
| Number _, Global _ -> -1
| Number _, Local _ -> -1
| Global _, Local _ -> -1
| Number n, Number m -> Int.compare n m

let equal lbl lbl' = compare lbl lbl' = 0

Expand Down Expand Up @@ -109,8 +126,8 @@ module Label = struct
| None , Local (name, _) -> Local (name, Uid.new_uid ())
| _ -> raise (not_local_error show lbl)

let one = Number 1
let two = Number 2
let one = of_int 1
let two = of_int 2
let return = make_global "return"
end

Expand Down
16 changes: 8 additions & 8 deletions core/label.mli
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
open CommonTypes
val show_unique_labels_idents : bool Settings.setting

module Uid : sig
type t = Id of Int.t | Free
end

type local = Name.t * Uid.t
type global = Name.t
type local = string * Uid.t
type global = string

type t =
| Local of local
Expand All @@ -14,18 +14,18 @@ type t =
[@@deriving show]
type label = t

val make_local : ?uid:Uid.t -> Name.t -> t
val make_global : Name.t -> t
val make : ?local:bool -> Name.t -> t
val make_local : ?uid:Uid.t -> string -> t
val make_global : string -> t
val make : string -> t

val of_int : Int.t -> t
val to_int : t -> Int.t
val name : t -> Name.t
val name : t -> string

val compare : t -> t -> int
val equal : t -> t -> bool
val textual_equal : t -> t -> bool
val name_is : t -> Name.t -> bool
val name_is : t -> string -> bool

val is_local : t -> bool
val is_global : t -> bool
Expand Down
8 changes: 4 additions & 4 deletions core/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -300,7 +300,7 @@ let parse_foreign_language pos lang =

let any = any_pat dp
let local_label = Label.make_local
let label = Label.make_global
let label = Label.make
%}

%token EOF
Expand Down Expand Up @@ -456,8 +456,7 @@ nofun_declaration:
| typedecl SEMICOLON { $1 }
| links_module | links_open SEMICOLON { $1 }
| pollute = boption(OPEN) IMPORT CONSTRUCTOR SEMICOLON { import ~ppos:$loc($2) ~pollute [$3] }
| FRESH separated_nonempty_list(COMMA, BTCONSTRUCTOR)
LBRACE declarations RBRACE { with_pos $loc (FreshLabel(List.map local_label $2, $4))}
| FRESH separated_nonempty_list(COMMA, BTCONSTRUCTOR) SEMICOLON { with_pos $loc (FreshLabel (List.map local_label $2))}

alien_datatype:
| VARIABLE COLON datatype SEMICOLON { (binder ~ppos:$loc($1) $1, datatype $3) }
Expand Down Expand Up @@ -983,6 +982,7 @@ binding:
| fun_kind VARIABLE arg_lists perhaps_location switch_funlit_body { switch_fun_binding ~ppos:$loc None ($1, $2, $3, $4, $5) }
| typedecl SEMICOLON | links_module
| links_open SEMICOLON { $1 }
| FRESH separated_nonempty_list(COMMA, BTCONSTRUCTOR) SEMICOLON { with_pos $loc (FreshLabel (List.map local_label $2))}

mutual_binding_block:
| MUTUAL LBRACE mutual_bindings RBRACE { MutualBindings.flatten $3 }
Expand Down Expand Up @@ -1189,7 +1189,7 @@ field_label:
| CONSTRUCTOR { label $1 }
| VARIABLE { label $1 }
| STRING { label $1 }
| UINTEGER { label (string_of_int $1) }
| UINTEGER { Label.Number $1 }

rfields:
| fields_def(rfield, COMMA, row_var, kinded_row_var) { $1 }
Expand Down
19 changes: 8 additions & 11 deletions core/sugarTraversals.ml
Original file line number Diff line number Diff line change
Expand Up @@ -805,10 +805,9 @@ class map =
in
let language = o#foreign_language (Alien.language alien) in
AlienBlock (Alien.modify ~language ~declarations alien)
| FreshLabel(_x, _x_i1) ->
let _x = o#list (fun o -> o#label) _x in
let _x_i1 = o#list (fun o -> o#binding) _x_i1 in
FreshLabel(_x,_x_i1)
| FreshLabel ls ->
let ls = o#list (fun o -> o#label) ls in
FreshLabel ls

method binding : binding -> binding =
fun p ->
Expand Down Expand Up @@ -1594,9 +1593,8 @@ class fold =
let o = o#binder b in
o#datatype' dt)
(Alien.declarations alien)
| FreshLabel(_x, _x_i1) ->
let o = o#list (fun o -> o#label) _x in
let o = o#list (fun o -> o#binding) _x_i1 in
| FreshLabel ls ->
let o = o#list (fun o -> o#label) ls in
o

method binding : binding -> 'self_type =
Expand Down Expand Up @@ -2551,10 +2549,9 @@ class fold_map =
(Alien.declarations alien)
in
o, AlienBlock (Alien.modify ~language:lang ~declarations alien)
| FreshLabel(_x, _x_i1) ->
let o, _x = o#list (fun o -> o#label) _x in
let o, _x_i1 = o#list (fun o -> o#binding) _x_i1 in
o, FreshLabel(_x,_x_i1)
| FreshLabel ls ->
let (o, ls) = o#list (fun o -> o#label) ls in
(o, FreshLabel ls)


method binding : binding -> ('self_type * binding) =
Expand Down
3 changes: 1 addition & 2 deletions core/sugartoir.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1334,8 +1334,7 @@ struct
let xt = Binder.to_type binder in
I.alien (Var.make_info xt x scope, Alien.object_name alien, Alien.language alien,
fun v -> eval_bindings scope (extend [x] [(v, xt)] env) bs e)
| FreshLabel (_, decls) -> (* TODO: is that right ? ignore local labels *)
eval_bindings scope env (decls @ bs) e
| FreshLabel _ -> eval_bindings scope env bs e (* TODO: is that right ? ignore local labels *)
| Aliases _
| Infix _ ->
(* Ignore type alias and infix declarations - they
Expand Down
10 changes: 2 additions & 8 deletions core/sugartypes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,6 @@ module Pattern = struct
| Cons of with_pos * with_pos
| List of with_pos list
| Variant of Label.t * with_pos option
(* | Effect of Label.t * with_pos list * with_pos *)
| Operation of Label.t * with_pos list * with_pos
| Negative of Label.t list
| Record of (Label.t * with_pos) list * with_pos option
Expand Down Expand Up @@ -535,7 +534,7 @@ and bindingnode =
| Exp of phrase
| Module of { binder: Binder.with_pos; members: binding list }
| AlienBlock of Alien.multi Alien.t
| FreshLabel of Label.t list * binding list
| FreshLabel of Label.t list
and binding = bindingnode WithPos.t
and block_body = binding list * phrase
and cp_phrasenode =
Expand Down Expand Up @@ -818,12 +817,7 @@ struct
| Import _
| Open _
| Aliases _ -> empty, empty
| FreshLabel (_, decls) ->
List.fold_left
(fun (b,f) decl -> let b', f' = binding decl in
StringSet.union b b', StringSet.union f f')
(StringSet.empty, StringSet.empty)
decls
| FreshLabel _ -> empty, empty
(* This is technically a declaration, thus the name should
probably be treated as bound rather than free. *)
| Infix { name; _ } -> empty, singleton name
Expand Down
6 changes: 2 additions & 4 deletions core/transformSugar.ml
Original file line number Diff line number Diff line change
Expand Up @@ -905,11 +905,9 @@ class transform (env : Types.typing_environment) =
| (Infix _) as node ->
(o, node)
| Exp e -> let (o, e, _) = o#phrase e in (o, Exp e)
| FreshLabel(labels, decls) ->
| FreshLabel ls ->
(* do we wanna do something with labels ? *)
let o, decls = ListUtils.fold_left_map
(fun o d -> o#binding d) o decls in
(o, FreshLabel(labels, decls))
(o, FreshLabel ls)
| AlienBlock _ -> assert false
| Module _ -> assert false
| Import _ -> assert false
Expand Down
Loading