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.

Sign up for GitHub

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

Jump to bottom

Term-level type annotations for effectful operations. #1197

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Term-level type annotations for effectful operations. #1197

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
9 changes: 8 additions & 1 deletion core/desugarSessionExceptions.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,14 @@ object (o : 'self_type)
Types.fresh_type_variable (CommonTypes.lin_any, CommonTypes.res_any) in
let with_pos x = SourceCode.WithPos.make ~pos x in
(* FIXME: WT: I don't know whether should it be lindo or not *)
let doOp = DoOperation (with_pos (Operation failure_op_name), [], Some (Types.empty_type), DeclaredLinearity.Lin) in
let op =
let syntype = Datatype.Operation ([with_pos Datatype.Unit], with_pos (Datatype.Variant ([], Datatype.Closed)), DeclaredLinearity.Lin) in
let semtype = Types.Operation (Types.unit_type, Types.empty_type, DeclaredLinearity.Lin) in
Operation (failure_op_name,
Some (with_pos syntype
, Some semtype), Some semtype)
in
let doOp = DoOperation (with_pos op, [], Some (Types.empty_type), DeclaredLinearity.Lin) in
(o, with_pos (Switch (with_pos doOp, [], Some ty)), ty)
| { node = TryInOtherwise (_, _, _, _, None); _} -> assert false
| { node = TryInOtherwise (try_phr, pat, as_phr, otherwise_phr, (Some dt)); pos }
Expand Down
6 changes: 4 additions & 2 deletions core/parser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -708,8 +708,10 @@ unary_expression:
| MINUSDOT unary_expression { unary_appl ~ppos:$loc UnaryOp.FloatMinus $2 }
| OPERATOR unary_expression { unary_appl ~ppos:$loc (UnaryOp.Name $1) $2 }
| postfix_expression | constructor_expression { $1 }
| DOOP CONSTRUCTOR loption(arg_spec) { with_pos $loc (DoOperation (with_pos $loc($2) (Operation $2), $3, None, DeclaredLinearity.Unl)) }
| LINDOOP CONSTRUCTOR loption(arg_spec) { with_pos $loc (DoOperation (with_pos $loc($2) (Operation $2), $3, None, DeclaredLinearity.Lin)) }
| DOOP CONSTRUCTOR loption(arg_spec) { with_pos $loc (DoOperation (with_pos $loc($2) (Operation ($2, None, None)), $3, None, DeclaredLinearity.Unl)) }
| LINDOOP CONSTRUCTOR loption(arg_spec) { with_pos $loc (DoOperation (with_pos $loc($2) (Operation ($2, None, None)), $3, None, DeclaredLinearity.Lin)) }
| DOOP LPAREN CONSTRUCTOR COLON datatype RPAREN loption(arg_spec) { with_pos $loc (DoOperation (with_pos $loc($3) (Operation ($3, Some (datatype $5), None)), $7, None, DeclaredLinearity.Unl)) }
| LINDOOP LPAREN CONSTRUCTOR COLON datatype RPAREN loption(arg_spec) { with_pos $loc (DoOperation (with_pos $loc($3) (Operation ($3, Some (datatype $5), None)), $7, None, DeclaredLinearity.Lin)) }

infix_appl:
| unary_expression { $1 }
Expand Down
28 changes: 18 additions & 10 deletions core/sugarTraversals.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -322,11 +322,14 @@ class map =
| DoOperation (op, ps, t, b) ->
let op = o#phrase op in
let ps = o#list (fun o -> o#phrase) ps in
let t = o#option (fun o -> o#typ) t in
let t = o#option (fun o -> o#unknown) t in
let b = o#linearity b in
DoOperation (op, ps, t, b)
| Operation _x ->
| Operation (_x, t, t') ->
let _x = o#name _x in
Operation _x
let t = o#option (fun o -> o#datatype') t in
let t' = o#option (fun o -> o#unknown) t' in
Operation (_x, t, t')
| Linlet _x ->
let _x = o#phrase _x in Linlet _x
| Unlet _x ->
Expand Down Expand Up @@ -1146,13 +1149,15 @@ class fold =
| ConstructorLit ((_x, _x_i1, _x_i2)) ->
let o = o#name _x in
let o = o#option (fun o -> o#phrase) _x_i1 in o
| DoOperation (op,ps,t,b) ->
| DoOperation (op, ps, t, b) ->
let o = o#phrase op in
let o = o#option (fun o -> o#unknown) t in
let o = o#list (fun o -> o#phrase) ps in
let o = o#option (fun o -> o#unknown) t in
let o = o#linearity b in o
| Operation (_x) ->
let o = o#name _x in o
| Operation (_x, t, t') ->
let o = o#name _x in
let o = o#option (fun o -> o#datatype') t in
let o = o#option (fun o -> o#unknown) t' in o
| Linlet _x ->
let o = o#phrase _x in o
| Unlet _x ->
Expand Down Expand Up @@ -1975,12 +1980,15 @@ class fold_map =
(o, (ConstructorLit ((_x, _x_i1, _x_i2))))
| DoOperation (op, ps, t, b) ->
let (o, op) = o#phrase op in
let (o, t) = o#option (fun o -> o#typ) t in
let (o, ps) = o#list (fun o -> o#phrase) ps in
let (o, t) = o#option (fun o -> o#unknown) t in
let (o, b) = o#linearity b in
(o, DoOperation (op, ps, t, b))
| Operation _x ->
| Operation (_x, t, t') ->
let (o, _x) = o#name _x in
(o, Operation _x)
let (o, t) = o#option (fun o -> o#datatype') t in
let (o, t') = o#option (fun o -> o#unknown) t' in
(o, Operation (_x, t, t'))
| Linlet _x ->
let (o, _x) = o#phrase _x in
(o, Linlet _x)
Expand Down
2 changes: 1 addition & 1 deletion core/sugartoir.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -993,7 +993,7 @@ struct
| None -> failwith "Operation with no name"

method! phrasenode = function
| Operation name -> opname <- Some name ; o
| Operation (name, _, _) -> opname <- Some name ; o
| p -> super#phrasenode p
end)#phrase op in
o#opname
Expand Down
2 changes: 1 addition & 1 deletion core/sugartypes.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -483,7 +483,7 @@ and phrasenode =
| Generalise of phrase
| ConstructorLit of Name.t * phrase option * Types.datatype option
| DoOperation of phrase * phrase list * Types.datatype option * DeclaredLinearity.t
| Operation of Name.t
| Operation of Name.t * datatype' option * Types.datatype option
| Handle of handler
| Unlet of phrase
| Linlet of phrase
Expand Down
10 changes: 8 additions & 2 deletions core/transformSugar.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -491,9 +491,15 @@ class transform (env : Types.typing_environment) =
let (o, e, _) = option o (fun o -> o#phrase) e in
let (o, t) = o#datatype t in
(o, ConstructorLit (name, e, Some t), t)
| DoOperation (name, ps, Some t, b) ->
| DoOperation (p, ps, t, b) ->
let (o, p, _) = o#phrase p in
let (o, ps, _) = list o (fun o -> o#phrase) ps in
(o, DoOperation (name, ps, Some t, b), t)
let (o, t) = optionu o (fun o -> o#datatype) t in
(o, DoOperation (p, ps, t, b), val_of t)
| Operation (name, t, t') ->
let (o, t) = optionu o (fun o -> o#datatype') t in
let (o, t') = optionu o (fun o -> o#datatype) t' in
(o, Operation (name, t, t'), val_of t')
| Handle { sh_expr; sh_effect_cases; sh_value_cases; sh_descr } ->
let (input_row, input_t, output_row, output_t) = sh_descr.shd_types in
let (o, expr, _) = o#phrase sh_expr in
Expand Down
Loading
Loading