Skip to content

Commit 655dc77

Browse files
hew02hew02
committed
Added subkind Numeric.
+ Reconfigured lib.ml's arithmetic operations to use the numeric subkind as a primitive form of ad hoc polymorphism. + Moved `abs()` to `lib.ml` so it can be ad hoc by piggybacking of OCaml's type matching + The keyword `effect` is now reserved in OCaml, renamed a case in irCheck + Added a fix for the Emacs mode
1 parent c7a899c commit 655dc77

18 files changed

+276
-57
lines changed

‎bin/dune

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
(executable
22
(name links)
3-
(public_name linx)
3+
(public_name links)
44
(package links)
55
(modes native)
66
(libraries unix threads.posix dynlink ANSITerminal linenoise links.core))

‎core/commonTypes.ml

Lines changed: 19 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,7 @@ module Restriction = struct
5151
type t =
5252
| Any
5353
| Base
54+
| Numeric
5455
| Mono
5556
| Session
5657
| Effect
@@ -64,6 +65,10 @@ module Restriction = struct
6465
| Base -> true
6566
| _ -> false
6667

68+
let is_numeric = function
69+
| Numeric -> true
70+
| _ -> false
71+
6772
let is_mono = function
6873
| Mono -> true
6974
| _ -> false
@@ -77,20 +82,23 @@ module Restriction = struct
7782
| _ -> false
7883

7984
let to_string = function
80-
| Any -> "Any"
81-
| Base -> "Base"
82-
| Mono -> "Mono"
83-
| Session -> "Session"
84-
| Effect -> "Eff"
85+
| Any -> "Any"
86+
| Base -> "Base"
87+
| Numeric -> "Numeric"
88+
| Mono -> "Mono"
89+
| Session -> "Session"
90+
| Effect -> "Eff"
8591

8692
let min l r =
8793
match l, r with
88-
| Any, Any -> Some Any
89-
| Mono, Mono -> Some Mono
90-
| Session, Session -> Some Session
91-
| Effect, Effect -> Some Effect
92-
| Base, Base -> Some Base
94+
| Any, Any -> Some Any
95+
| Mono, Mono -> Some Mono
96+
| Session, Session -> Some Session
97+
| Effect, Effect -> Some Effect
98+
| Base, Base -> Some Base
99+
| Numeric, Numeric -> Some Numeric
93100
| x, Any | Any, x -> Some x (* Any will narrow to anything. *)
101+
| Numeric, Mono | Mono, Numeric -> Some Numeric (* Mono can narrow to Numeric. *)
94102
| Base, Mono | Mono, Base -> Some Base (* Mono can narrow to Base. *)
95103
| Session, Mono | Mono, Session -> Some Session (* Super dubious, but we don't have another way*)
96104
| _ -> None
@@ -99,6 +107,7 @@ end
99107
(* Convenient aliases for constructing values *)
100108
let res_any = Restriction.Any
101109
let res_base = Restriction.Base
110+
let res_numeric = Restriction.Numeric
102111
let res_mono = Restriction.Mono
103112
let res_session = Restriction.Session
104113
let res_effect = Restriction.Effect

‎core/irCheck.ml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1053,11 +1053,11 @@ struct
10531053
(* For each case branch, the corresponding entry goes directly into the field spec map of the inner effect row *)
10541054
let inner_effects_map_from_branches = StringMap.map (fun x -> Present x) branch_presence_spec_types in
10551055
(* We now add all entries from the outer effects that were not touched by the handler to the inner effects *)
1056-
let inner_effects_map = StringMap.fold (fun effect outer_presence_spec map ->
1057-
if StringMap.mem effect inner_effects_map_from_branches then
1056+
let inner_effects_map = StringMap.fold (fun effect' outer_presence_spec map ->
1057+
if StringMap.mem effect' inner_effects_map_from_branches then
10581058
map
10591059
else
1060-
StringMap.add effect outer_presence_spec map
1060+
StringMap.add effect' outer_presence_spec map
10611061
) inner_effects_map_from_branches outer_effects_map in
10621062
let inner_effects = Row (inner_effects_map, outer_effects_var, outer_effects_dualized) in
10631063

‎core/lib.ml

Lines changed: 51 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ type primitive =
3535
[ Value.t
3636
| `PFun of RequestData.request_data -> Value.t list -> Value.t Lwt.t ]
3737

38-
type pure = PURE | IMPURE
38+
type pure = PURE | IMPURE | F2 of (Value.t -> Value.t -> pure)
3939

4040
type located_primitive = [ `Client | `Server of primitive | primitive ]
4141

@@ -60,6 +60,21 @@ let string_op impl pure : located_primitive * Types.datatype * pure =
6060
datatype "(String, String) -> String",
6161
pure
6262

63+
let numeric_op impli implf purei puref : located_primitive * Types.datatype * pure =
64+
(`PFun (fun _ args -> match args with
65+
| [x; y] ->
66+
(match (x,y) with
67+
| (`Int _, `Int _) -> Lwt.return (`Int (impli (Value.unbox_int x) (Value.unbox_int y)))
68+
| (`Float _, `Float _) -> Lwt.return (`Float (implf (Value.unbox_float x) (Value.unbox_float y)))
69+
| _ -> raise (runtime_type_error "type error in numeric operation"))
70+
| _ -> raise (internal_error "arity error in numeric operation"))),
71+
datatype "(a::Numeric, a) -> a",
72+
F2 (fun l r -> match (l, r) with
73+
| (`Int _, `Int _) -> purei
74+
| (`Float _, `Float _) -> puref
75+
| _ -> raise (internal_error ("cannot establish purity in numeric operations"))
76+
)
77+
6378
let conversion_op' ~unbox ~conv ~(box :'a->Value.t): Value.t list -> Value.t = function
6479
| [x] -> box (conv (unbox x))
6580
| _ -> assert false
@@ -228,18 +243,32 @@ let project_datetime (f: CalendarShow.t -> int) : located_primitive * Types.data
228243

229244

230245
let env : (string * (located_primitive * Types.datatype * pure)) list = [
231-
"+", int_op (+) PURE;
232-
"-", int_op (-) PURE;
233-
"*", int_op ( * ) PURE;
234-
"/", int_op (/) IMPURE;
235-
"^", int_op pow PURE;
236-
"mod", int_op (mod) IMPURE;
237-
"+.", float_op (+.) PURE;
238-
"-.", float_op (-.) PURE;
239-
"*.", float_op ( *.) PURE;
240-
"/.", float_op (/.) PURE;
241-
"^.", float_op ( ** ) PURE;
242-
"^^", string_op ( ^ ) PURE;
246+
"+", numeric_op ( + ) ( +. ) PURE PURE;
247+
"-", numeric_op ( - ) ( -. ) PURE PURE;
248+
"*", numeric_op ( * ) ( *. ) PURE PURE;
249+
"/", numeric_op ( / ) ( /. ) IMPURE PURE;
250+
"^", numeric_op (pow) ( ** ) PURE PURE;
251+
252+
"mod", int_op (mod) IMPURE;
253+
254+
(* For backwards compatability *)
255+
"+.", float_op ( +. ) PURE;
256+
"-.", float_op ( -. ) PURE;
257+
"*.", float_op ( *.) PURE;
258+
"/.", float_op ( /. ) PURE;
259+
"^.", float_op ( ** ) PURE;
260+
261+
"^^", string_op ( ^ ) PURE;
262+
263+
(* moved abs to make use of ad hoc ability,
264+
ideally there could be a way to bootstrap Prelude similar to #786 *)
265+
"abs",
266+
(p1 (fun n -> match n with
267+
| `Int _ -> Value.box_int ( let x = (Value.unbox_int n) in if x > 0 then x else -x )
268+
| `Float _ -> Value.box_float ( let x = (Value.unbox_float n) in if x > 0.0 then x else -.x )
269+
| _ -> raise (runtime_type_error ("Cannot computer absolute value: " ^ Value.string_of_value n))),
270+
datatype "(a::Numeric) -> a",
271+
PURE);
243272

244273
"max_int",
245274
(Value.box_int max_int,
@@ -718,7 +747,6 @@ let env : (string * (located_primitive * Types.datatype * pure)) list = [
718747

719748
"print",
720749
(p1 (fun msg -> print_string (Value.unbox_string msg); flush stdout; `Record []),
721-
(* datatype "(String) ~> ()", *)
722750
datatype "(String) ~> ()",
723751
IMPURE);
724752

@@ -732,7 +760,15 @@ let env : (string * (located_primitive * Types.datatype * pure)) list = [
732760
PURE);
733761

734762
"negate",
735-
(p1 (Value.unbox_int ->- (~-) ->- Value.box_int), datatype "(Int) -> Int",
763+
(p1 (fun n -> match n with
764+
| `Int _ -> Value.box_int (- (Value.unbox_int n))
765+
| `Float _ -> Value.box_float (-. (Value.unbox_float n))
766+
| _ -> raise (runtime_type_error ("Cannot negate: " ^ Value.string_of_value n))),
767+
datatype "(a::Numeric) -> a",
768+
PURE);
769+
770+
"negatei",
771+
(p1 (fun i -> Value.box_int (- (Value.unbox_int i))), datatype "(Int) -> Int",
736772
PURE);
737773

738774
"negatef",

‎core/parser.mly

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,7 @@ let restriction_of_string p =
7979
function
8080
| "Any" -> res_any
8181
| "Base" -> res_base
82+
| "Numeric" -> res_numeric
8283
| "Session" -> res_session
8384
| "Mono" -> res_mono
8485
| rest ->
@@ -148,6 +149,7 @@ let kind_of p =
148149
(* subkind of type abbreviations *)
149150
| "Any" -> (Some pk_type, Some (lin_any, res_any))
150151
| "Base" -> (Some pk_type, Some (lin_unl, res_base))
152+
| "Numeric" -> (Some pk_type, Some (lin_unl, res_numeric))
151153
| "Session" -> (Some pk_type, Some (lin_any, res_session))
152154
| "Eff" -> (Some pk_row , Some (default_effect_lin, res_effect))
153155
| k -> raise (ConcreteSyntaxError (pos p, "Invalid kind: " ^ k))
@@ -158,6 +160,7 @@ let subkind_of p =
158160
| "Any" -> Some (lin_any, res_any)
159161
| "Lin" -> Some (lin_unl, res_any) (* for linear effect vars *)
160162
| "Base" -> Some (lin_unl, res_base)
163+
| "Numeric" -> Some (lin_unl, res_numeric)
161164
| "Session" -> Some (lin_any, res_session)
162165
| "Eff" -> Some (default_effect_lin, res_effect)
163166
| sk -> raise (ConcreteSyntaxError (pos p, "Invalid subkind: " ^ sk))
@@ -198,7 +201,6 @@ let attach_presence_subkind (t, subkind) =
198201
| _ -> assert false
199202
in attach_subkind_helper update subkind
200203

201-
202204
let alias p name args aliasbody =
203205
with_pos p (Aliases [with_pos p (name, args, aliasbody)])
204206

‎core/sugartoir.ml

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -909,20 +909,21 @@ struct
909909
I.apply (instantiate n tyargs, [ev e1; ev e2])
910910
| InfixAppl ((tyargs, BinaryOp.Cons), e1, e2) ->
911911
cofv (I.apply_pure (instantiate "Cons" tyargs, [ev e1; ev e2]))
912-
| InfixAppl ((tyargs, BinaryOp.FloatMinus), e1, e2) ->
912+
| InfixAppl ((tyargs, BinaryOp.FloatMinus), e1, e2) -> (* NOTE for legacy purposes *)
913913
cofv (I.apply_pure (instantiate "-." tyargs, [ev e1; ev e2]))
914914
| InfixAppl ((tyargs, BinaryOp.Minus), e1, e2) ->
915-
cofv (I.apply_pure (instantiate "-" tyargs, [ev e1; ev e2]))
915+
let v1 = (ev e1) and v2 = (ev e2) in
916+
cofv (I.apply_pure (instantiate "-" tyargs, [v1; v2]))
916917
| InfixAppl ((_tyargs, BinaryOp.And), e1, e2) ->
917918
(* IMPORTANT: we compile boolean expressions to
918919
conditionals in order to faithfully capture
919920
short-circuit evaluation *)
920921
I.condition (ev e1, ec e2, cofv (I.constant (Constant.Bool false)))
921922
| InfixAppl ((_tyargs, BinaryOp.Or), e1, e2) ->
922923
I.condition (ev e1, cofv (I.constant (Constant.Bool true)), ec e2)
923-
| UnaryAppl ((_tyargs, UnaryOp.Minus), e) ->
924-
cofv (I.apply_pure(instantiate_mb "negate", [ev e]))
925-
| UnaryAppl ((_tyargs, UnaryOp.FloatMinus), e) ->
924+
| UnaryAppl ((tyargs, UnaryOp.Minus), e) ->
925+
cofv (I.apply_pure (instantiate "negate" tyargs, [ev e]))
926+
| UnaryAppl ((_, UnaryOp.FloatMinus), e) -> (* NOTE for legacy purposes *)
926927
cofv (I.apply_pure(instantiate_mb "negatef", [ev e]))
927928
| UnaryAppl ((tyargs, UnaryOp.Name n), e) when Lib.is_pure_primitive n ->
928929
cofv (I.apply_pure(instantiate n tyargs, [ev e]))

‎core/transformSugar.ml

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -31,14 +31,14 @@ let type_section env =
3131

3232
let type_unary_op env tycon_env =
3333
let datatype = DesugarDatatypes.read ~aliases:tycon_env in function
34-
| UnaryOp.Minus -> datatype "(Int) -> Int"
35-
| UnaryOp.FloatMinus -> datatype "(Float) -> Float"
34+
| UnaryOp.Minus -> datatype "(a::Numeric) -> a"
35+
| UnaryOp.FloatMinus -> datatype "(Float) -> Float" (* keeping for compatability with previous version *)
3636
| UnaryOp.Name n -> TyEnv.find n env
3737

3838
let type_binary_op env tycon_env =
3939
let open BinaryOp in
4040
let datatype = DesugarDatatypes.read ~aliases:tycon_env in function
41-
| Minus -> TyEnv.find "-" env
41+
| Minus -> datatype "(a::Numeric, a) -> a"
4242
| FloatMinus -> TyEnv.find "-." env
4343
| RegexMatch flags ->
4444
let nativep = List.exists ((=) RegexNative) flags
@@ -66,6 +66,10 @@ let type_binary_op env tycon_env =
6666
Function (Types.make_tuple_type [a; a], e,
6767
Primitive Primitive.Bool ))
6868
| Name "!" -> TyEnv.find "Send" env
69+
| Name "+"
70+
| Name "*"
71+
| Name "/"
72+
| Name "^" -> datatype "(a::Numeric, a) -> a"
6973
| Name n -> TyEnv.find n env
7074

7175
let fun_effects t pss =

‎core/typeSugar.ml

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1979,8 +1979,8 @@ let add_empty_usages (p, t) = (p, t, Usage.empty)
19791979
let type_unary_op pos env =
19801980
let datatype = datatype env.tycon_env in
19811981
function
1982-
| UnaryOp.Minus -> add_empty_usages (datatype "(Int) { |_::Any}-> Int")
1983-
| UnaryOp.FloatMinus -> add_empty_usages (datatype "(Float) { |_::Any}-> Float")
1982+
| UnaryOp.Minus -> add_empty_usages (datatype "(a::Numeric) -> a")
1983+
| UnaryOp.FloatMinus -> add_empty_usages (datatype "(Float) -> Float") (* keeping for compatability with previous version *)
19841984
| UnaryOp.Name n ->
19851985
try
19861986
add_usages (Utils.instantiate env.var_env n) (Usage.singleton n)
@@ -1992,7 +1992,7 @@ let type_binary_op pos ctxt =
19921992
let open BinaryOp in
19931993
let open Types in
19941994
let datatype = datatype ctxt.tycon_env in function
1995-
| Minus -> add_empty_usages (Utils.instantiate ctxt.var_env "-")
1995+
| Minus -> add_empty_usages (datatype "(a::Numeric, a) -> a")
19961996
| FloatMinus -> add_empty_usages (Utils.instantiate ctxt.var_env "-.")
19971997
| RegexMatch flags ->
19981998
let nativep = List.exists ((=) RegexNative) flags
@@ -2021,6 +2021,10 @@ let type_binary_op pos ctxt =
20212021
Function (Types.make_tuple_type [a; a], eff, Primitive Primitive.Bool),
20222022
Usage.empty)
20232023
| Name "!" -> add_empty_usages (Utils.instantiate ctxt.var_env "Send")
2024+
| Name "+"
2025+
| Name "*"
2026+
| Name "/"
2027+
| Name "^" -> add_empty_usages (datatype "(a::Numeric, a) -> a")
20242028
| Name n ->
20252029
try
20262030
add_usages (Utils.instantiate ctxt.var_env n) (Usage.singleton n)

‎core/types.ml

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -799,6 +799,50 @@ module Base : Constraint = struct
799799
let make_type, make_row = make_restriction_transform Base
800800
end
801801

802+
module Numeric : Constraint = struct
803+
open Restriction
804+
open Primitive
805+
806+
module NumericPredicate = struct
807+
class klass = object
808+
inherit type_predicate as super
809+
810+
method! point_satisfies f vars point =
811+
match Unionfind.find point with
812+
| Recursive _ -> false
813+
| _ -> super#point_satisfies f vars point
814+
815+
method! type_satisfies vars = function
816+
(* Unspecified kind *)
817+
| Not_typed -> assert false
818+
| Var _ | Recursive _ | Closed ->
819+
failwith ("[3] freestanding Var / Recursive / Closed not implemented yet (must be inside Meta)")
820+
| Alias _ as t -> super#type_satisfies vars t
821+
| (Application _ | RecursiveApplication _) -> false
822+
| Meta _ as t -> super#type_satisfies vars t
823+
(* Type *)
824+
| Primitive (Int | Float) -> true
825+
| Primitive _ -> false
826+
| (Function _ | Lolli _ | Record _ | Variant _ | Table _ | Lens _ | ForAll (_::_, _)) -> false
827+
| ForAll ([], t) -> super#type_satisfies vars t
828+
(* Effect *)
829+
| Effect _ as t -> super#type_satisfies vars t
830+
| Operation _ -> failwith "TODO types.ml/766"
831+
(* Row *)
832+
| Row _ as t -> super#type_satisfies vars t
833+
(* Presence *)
834+
| Absent -> true
835+
| Present _ as t -> super#type_satisfies vars t
836+
(* Session *)
837+
| Input _ | Output _ | Select _ | Choice _ | Dual _ | End -> false
838+
end
839+
end
840+
841+
let type_satisfies, row_satisfies = make_restriction_predicate (module NumericPredicate) Numeric false
842+
let can_type_be, can_row_be = make_restriction_predicate (module NumericPredicate) Numeric true
843+
let make_type, make_row = make_restriction_transform Numeric
844+
end
845+
802846
(* unl type stuff *)
803847
module Unl : Constraint = struct
804848
class unl_predicate = object(o)
@@ -994,6 +1038,7 @@ let get_restriction_constraint : Restriction.t -> (module Constraint) option =
9941038
let open Restriction in function
9951039
| Any | Effect -> None
9961040
| Base -> Some (module Base)
1041+
| Numeric -> Some (module Numeric)
9971042
| Session -> Some (module Session)
9981043
| Mono -> Some (module Mono)
9991044

@@ -2395,6 +2440,7 @@ struct
23952440
| (Linearity.Unl, Restriction.Any) -> ""
23962441
| (Linearity.Any, Restriction.Any) -> "Any"
23972442
| (Linearity.Unl, Restriction.Base) -> Restriction.to_string res_base
2443+
| (Linearity.Unl, Restriction.Numeric) -> Restriction.to_string res_numeric
23982444
| (Linearity.Any, Restriction.Session) -> Restriction.to_string res_session
23992445
| (Linearity.Unl, Restriction.Effect) -> Restriction.to_string res_effect
24002446
| (l, r) -> full (l, r)
@@ -2411,6 +2457,8 @@ struct
24112457
| PrimaryKind.Type, (Linearity.Unl, Restriction.Any) -> ""
24122458
| PrimaryKind.Type, (Linearity.Unl, Restriction.Base) ->
24132459
Restriction.to_string res_base
2460+
| PrimaryKind.Type, (Linearity.Unl, Restriction.Numeric) ->
2461+
Restriction.to_string res_numeric
24142462
| PrimaryKind.Type, (Linearity.Any, Restriction.Session) ->
24152463
Restriction.to_string res_session
24162464
| PrimaryKind.Type, sk ->
@@ -3498,6 +3546,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct
34983546
| (L.Unl, R.Any) -> if is_eff && lincont_enabled then constant "Lin" else Empty (* (1) see above *)
34993547
| (L.Any, R.Any) -> if is_eff && lincont_enabled then Empty else constant "Any"
35003548
| (L.Unl, R.Base) -> constant @@ R.to_string res_base
3549+
| (L.Unl, R.Numeric) -> constant @@ R.to_string res_numeric
35013550
| (L.Any, R.Session) -> constant @@ R.to_string res_session
35023551
| (L.Unl, R.Effect) -> constant @@ R.to_string res_effect (* control-flow-linearity may also need changing this *)
35033552
| _ -> full_name
@@ -3535,6 +3584,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct
35353584
match subknd with
35363585
| L.Unl, R.Any -> assert false
35373586
| L.Unl, R.Base -> StringBuffer.write buf (R.to_string res_base)
3587+
| L.Unl, R.Numeric -> StringBuffer.write buf (R.to_string res_numeric)
35383588
| L.Any, R.Session -> StringBuffer.write buf (R.to_string res_session)
35393589
| subknd ->
35403590
let policy = Policy.set_kinds Policy.Full (Context.policy ctx) in

0 commit comments

Comments
 (0)