Added subkind Numeric for ad hoc arithmetic operations

bin/dune

@@ -1,6 +1,6 @@
 (executable
   (name links)
-  (public_name linx)
+  (public_name links)
   (package links)
   (modes native)
   (libraries unix threads.posix dynlink ANSITerminal linenoise links.core))

core/commonTypes.ml

@@ -51,6 +51,7 @@ module Restriction = struct
   type t =
     | Any
     | Base
+    | Numeric
     | Mono
     | Session
     | Effect
@@ -64,6 +65,10 @@ module Restriction = struct
     | Base -> true
     | _    -> false
 
+  let is_numeric = function
+    | Numeric -> true
+    | _    -> false
+
   let is_mono = function
     | Mono -> true
     | _    -> false
@@ -77,20 +82,23 @@ module Restriction = struct
     | _      -> false
 
   let to_string = function
-    | Any     -> "Any"
-    | Base    -> "Base"
-    | Mono    -> "Mono"
-    | Session -> "Session"
-    | Effect  -> "Eff"
+    | Any      -> "Any"
+    | Base     -> "Base"
+    | Numeric  -> "Numeric"
+    | Mono     -> "Mono"
+    | Session  -> "Session"
+    | Effect   -> "Eff"
 
   let min l r =
     match l, r with
-    | Any, Any         -> Some Any
-    | Mono, Mono       -> Some Mono
-    | Session, Session -> Some Session
-    | Effect, Effect   -> Some Effect
-    | Base, Base       -> Some Base
+    | Any, Any             -> Some Any
+    | Mono, Mono           -> Some Mono
+    | Session, Session     -> Some Session
+    | Effect, Effect       -> Some Effect
+    | Base, Base           -> Some Base
+    | Numeric, Numeric     -> Some Numeric
     | x, Any | Any, x  -> Some x (* Any will narrow to anything. *)
+    | Numeric, Mono | Mono, Numeric -> Some Numeric (* Mono can narrow to Numeric. *)
     | Base, Mono | Mono, Base -> Some Base (* Mono can narrow to Base. *)
     | Session, Mono | Mono, Session -> Some Session (* Super dubious, but we don't have another way*)
     | _ -> None
@@ -99,6 +107,7 @@ end
 (* Convenient aliases for constructing values *)
 let res_any     = Restriction.Any
 let res_base    = Restriction.Base
+let res_numeric = Restriction.Numeric
 let res_mono    = Restriction.Mono
 let res_session = Restriction.Session
 let res_effect  = Restriction.Effect

core/irCheck.ml

@@ -1053,11 +1053,11 @@ struct
           (* For each case branch, the corresponding entry goes directly into the field spec map of the inner effect row *)
           let inner_effects_map_from_branches = StringMap.map (fun x -> Present x) branch_presence_spec_types in
           (* We now add all entries from the outer effects that were not touched by the handler to the inner effects *)
-          let inner_effects_map = StringMap.fold (fun effect outer_presence_spec map ->
-              if StringMap.mem effect inner_effects_map_from_branches then
+          let inner_effects_map = StringMap.fold (fun effect' outer_presence_spec map ->
+              if StringMap.mem effect' inner_effects_map_from_branches then
                 map
               else
-                StringMap.add effect outer_presence_spec map
+                StringMap.add effect' outer_presence_spec map
             )  inner_effects_map_from_branches outer_effects_map in
           let inner_effects = Row (inner_effects_map, outer_effects_var, outer_effects_dualized) in
 

core/lib.ml

@@ -35,7 +35,7 @@ type primitive =
 [ Value.t
 | `PFun of RequestData.request_data -> Value.t list -> Value.t Lwt.t ]
 
-type pure = PURE | IMPURE
+type pure = PURE | IMPURE | F2 of (Value.t -> Value.t -> pure)
 
 type located_primitive = [ `Client | `Server of primitive | primitive ]
 
@@ -60,6 +60,21 @@ let string_op impl pure : located_primitive * Types.datatype * pure =
   datatype "(String, String) -> String",
   pure
 
+let numeric_op impli implf purei puref : located_primitive * Types.datatype * pure =
+  (`PFun (fun _ args -> match args with
+  | [x; y] ->
+        (match (x,y) with
+          | (`Int _, `Int _) -> Lwt.return (`Int (impli (Value.unbox_int x) (Value.unbox_int y)))
+          | (`Float _, `Float _) -> Lwt.return (`Float (implf (Value.unbox_float x) (Value.unbox_float y)))
+        | _ -> raise (runtime_type_error "type error in numeric operation"))
+  | _ -> raise (internal_error "arity error in numeric operation"))),
+  datatype "(a::Numeric, a) -> a",
+  F2 (fun l r -> match (l, r) with
+          | (`Int _, `Int _) -> purei
+          | (`Float _, `Float _) -> puref
+          | _ -> raise (internal_error ("cannot establish purity in numeric operations"))
+  )
+
 let conversion_op' ~unbox ~conv ~(box :'a->Value.t): Value.t list -> Value.t = function
     | [x] -> box (conv (unbox x))
     | _ -> assert false
@@ -228,18 +243,32 @@ let project_datetime (f: CalendarShow.t -> int) : located_primitive * Types.data
 
 
 let env : (string * (located_primitive * Types.datatype * pure)) list = [
-  "+", int_op (+) PURE;
-  "-", int_op (-) PURE;
-  "*", int_op ( * ) PURE;
-  "/", int_op (/) IMPURE;
-  "^", int_op pow PURE;
-  "mod", int_op (mod) IMPURE;
-  "+.", float_op (+.) PURE;
-  "-.", float_op (-.) PURE;
-  "*.", float_op ( *.) PURE;
-  "/.", float_op (/.) PURE;
-  "^.", float_op ( ** ) PURE;
-  "^^", string_op ( ^ ) PURE;
+  "+",         numeric_op ( + ) ( +. ) PURE PURE;
+  "-",         numeric_op ( - ) ( -. ) PURE PURE;
+  "*",         numeric_op ( * ) ( *. ) PURE PURE;
+  "/",         numeric_op ( / ) ( /. ) IMPURE PURE;
+  "^",         numeric_op (pow) ( ** ) PURE PURE;
+
+  "mod",       int_op     (mod)   IMPURE;
+
+  (* For backwards compatability *)
+  "+.",        float_op   ( +. )  PURE;
+  "-.",        float_op   ( -. )  PURE;
+  "*.",        float_op   ( *.)   PURE;
+  "/.",        float_op   ( /. )  PURE;
+  "^.",        float_op   ( ** )  PURE;
+
+  "^^",        string_op  ( ^ )   PURE;
+
+  (* moved abs to make use of ad hoc ability,
+     ideally there could be a way to bootstrap Prelude similar to #786 *)
+  "abs",
+  (p1 (fun n -> match n with
+  | `Int _ -> Value.box_int ( let x = (Value.unbox_int n) in if x > 0 then x else -x )
+  | `Float _ -> Value.box_float ( let x = (Value.unbox_float n) in if x > 0.0 then x else -.x )
+  | _ -> raise (runtime_type_error ("Cannot computer absolute value: " ^ Value.string_of_value n))),
+  datatype "(a::Numeric) -> a",
+  PURE);
 
   "max_int",
   (Value.box_int max_int,
@@ -718,7 +747,6 @@ let env : (string * (located_primitive * Types.datatype * pure)) list = [
 
   "print",
   (p1 (fun msg -> print_string (Value.unbox_string msg); flush stdout; `Record []),
-   (* datatype "(String) ~> ()", *)
    datatype "(String) ~> ()",
   IMPURE);
 
@@ -732,7 +760,15 @@ let env : (string * (located_primitive * Types.datatype * pure)) list = [
   PURE);
 
   "negate",
-  (p1 (Value.unbox_int ->- (~-) ->- Value.box_int), datatype "(Int) -> Int",
+  (p1 (fun n -> match n with
+  | `Int _ -> Value.box_int (- (Value.unbox_int n))
+  | `Float _ -> Value.box_float (-. (Value.unbox_float n))
+  | _ -> raise (runtime_type_error ("Cannot negate: " ^ Value.string_of_value n))),
+  datatype "(a::Numeric) -> a",
+  PURE);
+
+  "negatei",
+  (p1 (fun i -> Value.box_int (- (Value.unbox_int i))), datatype "(Int) -> Int",
   PURE);
 
   "negatef",

core/parser.mly

@@ -79,6 +79,7 @@ let restriction_of_string p =
   function
   | "Any"     -> res_any
   | "Base"    -> res_base
+  | "Numeric" -> res_numeric
   | "Session" -> res_session
   | "Mono"    -> res_mono
   | rest      ->
@@ -148,6 +149,7 @@ let kind_of p =
   (* subkind of type abbreviations *)
   | "Any"      -> (Some pk_type, Some (lin_any, res_any))
   | "Base"     -> (Some pk_type, Some (lin_unl, res_base))
+  | "Numeric" ->  (Some pk_type, Some (lin_unl, res_numeric))
   | "Session"  -> (Some pk_type, Some (lin_any, res_session))
   | "Eff"      -> (Some pk_row , Some (default_effect_lin, res_effect))
   | k          -> raise (ConcreteSyntaxError (pos p, "Invalid kind: " ^ k))
@@ -158,6 +160,7 @@ let subkind_of p =
   | "Any"     -> Some (lin_any, res_any)
   | "Lin"     -> Some (lin_unl, res_any) (* for linear effect vars *)
   | "Base"    -> Some (lin_unl, res_base)
+  | "Numeric" -> Some (lin_unl, res_numeric)
   | "Session" -> Some (lin_any, res_session)
   | "Eff"     -> Some (default_effect_lin, res_effect)
   | sk        -> raise (ConcreteSyntaxError (pos p, "Invalid subkind: " ^ sk))
@@ -198,7 +201,6 @@ let attach_presence_subkind (t, subkind) =
     | _ -> assert false
   in attach_subkind_helper update subkind
 
-
 let alias p name args aliasbody =
     with_pos p (Aliases [with_pos p (name, args, aliasbody)])
 

core/sugartoir.ml

@@ -909,20 +909,21 @@ struct
               I.apply (instantiate n tyargs, [ev e1; ev e2])
           | InfixAppl ((tyargs, BinaryOp.Cons), e1, e2) ->
               cofv (I.apply_pure (instantiate "Cons" tyargs, [ev e1; ev e2]))
-          | InfixAppl ((tyargs, BinaryOp.FloatMinus), e1, e2) ->
+          | InfixAppl ((tyargs, BinaryOp.FloatMinus), e1, e2) -> (* NOTE for legacy purposes *)
               cofv (I.apply_pure (instantiate "-." tyargs, [ev e1; ev e2]))
           | InfixAppl ((tyargs, BinaryOp.Minus), e1, e2) ->
-              cofv (I.apply_pure (instantiate "-" tyargs, [ev e1; ev e2]))
+              let v1 = (ev e1) and v2 = (ev e2) in
+              cofv (I.apply_pure (instantiate "-" tyargs, [v1; v2]))
           | InfixAppl ((_tyargs, BinaryOp.And), e1, e2) ->
               (* IMPORTANT: we compile boolean expressions to
                  conditionals in order to faithfully capture
                  short-circuit evaluation *)
               I.condition (ev e1, ec e2, cofv (I.constant (Constant.Bool false)))
           | InfixAppl ((_tyargs, BinaryOp.Or), e1, e2) ->
               I.condition (ev e1, cofv (I.constant (Constant.Bool true)), ec e2)
-          | UnaryAppl ((_tyargs, UnaryOp.Minus), e) ->
-              cofv (I.apply_pure(instantiate_mb "negate", [ev e]))
-          | UnaryAppl ((_tyargs, UnaryOp.FloatMinus), e) ->
+          | UnaryAppl ((tyargs, UnaryOp.Minus), e) ->
+              cofv (I.apply_pure (instantiate "negate" tyargs, [ev e]))
+          | UnaryAppl ((_, UnaryOp.FloatMinus), e) -> (* NOTE for legacy purposes *)
               cofv (I.apply_pure(instantiate_mb "negatef", [ev e]))
           | UnaryAppl ((tyargs, UnaryOp.Name n), e) when Lib.is_pure_primitive n ->
               cofv (I.apply_pure(instantiate n tyargs, [ev e]))

core/transformSugar.ml

@@ -31,14 +31,14 @@ let type_section env =
 
 let type_unary_op env tycon_env =
   let datatype = DesugarDatatypes.read ~aliases:tycon_env in function
-    | UnaryOp.Minus      -> datatype "(Int) -> Int"
-    | UnaryOp.FloatMinus -> datatype "(Float) -> Float"
+    | UnaryOp.Minus      -> datatype "(a::Numeric) -> a"
+    | UnaryOp.FloatMinus -> datatype "(Float) -> Float" (* keeping for compatability with previous version *)
     | UnaryOp.Name n     -> TyEnv.find n env
 
 let type_binary_op env tycon_env =
   let open BinaryOp in
   let datatype = DesugarDatatypes.read ~aliases:tycon_env in function
-  | Minus        -> TyEnv.find "-" env
+  | Minus        -> datatype "(a::Numeric, a) -> a"
   | FloatMinus   -> TyEnv.find "-." env
   | RegexMatch flags ->
       let nativep  = List.exists ((=) RegexNative)  flags
@@ -66,6 +66,10 @@ let type_binary_op env tycon_env =
                 Function (Types.make_tuple_type [a; a], e,
                           Primitive Primitive.Bool ))
   | Name "!"     -> TyEnv.find "Send" env
+  | Name "+"
+  | Name "*"
+  | Name "/"
+  | Name "^"     -> datatype "(a::Numeric, a) -> a"
   | Name n       -> TyEnv.find n env
 
 let fun_effects t pss =

core/typeSugar.ml

@@ -1979,8 +1979,8 @@ let add_empty_usages (p, t) = (p, t, Usage.empty)
 let type_unary_op pos env =
   let datatype = datatype env.tycon_env in
   function
-  | UnaryOp.Minus      -> add_empty_usages (datatype "(Int) { |_::Any}-> Int")
-  | UnaryOp.FloatMinus -> add_empty_usages (datatype "(Float) { |_::Any}-> Float")
+  | UnaryOp.Minus      -> add_empty_usages (datatype "(a::Numeric) -> a")
+  | UnaryOp.FloatMinus -> add_empty_usages (datatype "(Float) -> Float") (* keeping for compatability with previous version *)
   | UnaryOp.Name n     ->
      try
        add_usages (Utils.instantiate env.var_env n) (Usage.singleton n)
@@ -1992,7 +1992,7 @@ let type_binary_op pos ctxt =
   let open BinaryOp in
   let open Types in
   let datatype = datatype ctxt.tycon_env in function
-  | Minus        -> add_empty_usages (Utils.instantiate ctxt.var_env "-")
+  | Minus        -> add_empty_usages (datatype "(a::Numeric, a) -> a")
   | FloatMinus   -> add_empty_usages (Utils.instantiate ctxt.var_env "-.")
   | RegexMatch flags ->
       let nativep  = List.exists ((=) RegexNative)  flags
@@ -2021,6 +2021,10 @@ let type_binary_op pos ctxt =
          Function (Types.make_tuple_type [a; a], eff, Primitive Primitive.Bool),
          Usage.empty)
   | Name "!"     -> add_empty_usages (Utils.instantiate ctxt.var_env "Send")
+  | Name "+"
+  | Name "*"
+  | Name "/"
+  | Name "^"     -> add_empty_usages (datatype "(a::Numeric, a) -> a")
   | Name n       ->
      try
        add_usages (Utils.instantiate ctxt.var_env n) (Usage.singleton n)

core/types.ml

@@ -799,6 +799,50 @@ module Base : Constraint = struct
   let make_type, make_row = make_restriction_transform Base
 end
 
+module Numeric : Constraint = struct
+  open Restriction
+  open Primitive
+
+  module NumericPredicate = struct
+    class klass = object
+      inherit type_predicate as super
+
+      method! point_satisfies f vars point =
+        match Unionfind.find point with
+        | Recursive _ -> false
+        | _ -> super#point_satisfies f vars point
+
+      method! type_satisfies vars = function
+        (* Unspecified kind *)
+        | Not_typed -> assert false
+        | Var _ | Recursive _ | Closed ->
+           failwith ("[3] freestanding Var / Recursive / Closed not implemented yet (must be inside Meta)")
+        | Alias _  as t  -> super#type_satisfies vars t
+        | (Application _ | RecursiveApplication _) -> false
+        | Meta _ as t  -> super#type_satisfies vars t
+        (* Type *)
+        | Primitive (Int | Float) -> true
+        | Primitive _ -> false
+        | (Function _ | Lolli _ | Record _ | Variant _ | Table _ | Lens _ | ForAll (_::_, _)) -> false
+        | ForAll ([], t) -> super#type_satisfies vars t
+        (* Effect *)
+        | Effect _ as t -> super#type_satisfies vars t
+        | Operation _ -> failwith "TODO types.ml/766"
+        (* Row *)
+        | Row _ as t -> super#type_satisfies vars t
+        (* Presence *)
+        | Absent -> true
+        | Present _ as t -> super#type_satisfies vars t
+        (* Session *)
+        | Input _ | Output _ | Select _ | Choice _ | Dual _ | End -> false
+    end
+  end
+
+  let type_satisfies, row_satisfies = make_restriction_predicate (module NumericPredicate) Numeric false
+  let can_type_be, can_row_be = make_restriction_predicate (module NumericPredicate) Numeric true
+  let make_type, make_row = make_restriction_transform Numeric
+end
+
 (* unl type stuff *)
 module Unl : Constraint = struct
   class unl_predicate = object(o)
@@ -994,6 +1038,7 @@ let get_restriction_constraint : Restriction.t -> (module Constraint) option =
   let open Restriction in function
   | Any | Effect -> None
   | Base -> Some (module Base)
+  | Numeric -> Some (module Numeric)
   | Session -> Some (module Session)
   | Mono -> Some (module Mono)
 
@@ -2395,6 +2440,7 @@ struct
        | (Linearity.Unl, Restriction.Any)     -> ""
        | (Linearity.Any, Restriction.Any)     -> "Any"
        | (Linearity.Unl, Restriction.Base)    -> Restriction.to_string res_base
+       | (Linearity.Unl, Restriction.Numeric) -> Restriction.to_string res_numeric
        | (Linearity.Any, Restriction.Session) -> Restriction.to_string res_session
        | (Linearity.Unl, Restriction.Effect)  -> Restriction.to_string res_effect
        | (l, r) -> full (l, r)
@@ -2411,6 +2457,8 @@ struct
       | PrimaryKind.Type, (Linearity.Unl, Restriction.Any) -> ""
       | PrimaryKind.Type, (Linearity.Unl, Restriction.Base) ->
          Restriction.to_string res_base
+      | PrimaryKind.Type, (Linearity.Unl, Restriction.Numeric) ->
+         Restriction.to_string res_numeric
       | PrimaryKind.Type, (Linearity.Any, Restriction.Session) ->
          Restriction.to_string res_session
       | PrimaryKind.Type, sk ->
@@ -3498,6 +3546,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct
        | (L.Unl, R.Any)     -> if is_eff && lincont_enabled then constant "Lin" else Empty (* (1) see above *)
        | (L.Any, R.Any)     -> if is_eff && lincont_enabled then Empty else constant "Any"
        | (L.Unl, R.Base)    -> constant @@ R.to_string res_base
+       | (L.Unl, R.Numeric) -> constant @@ R.to_string res_numeric
        | (L.Any, R.Session) -> constant @@ R.to_string res_session
        | (L.Unl, R.Effect)  -> constant @@ R.to_string res_effect (* control-flow-linearity may also need changing this *)
        | _ -> full_name
@@ -3535,6 +3584,7 @@ module RoundtripPrinter : PRETTY_PRINTER = struct
                  match subknd with
                  | L.Unl, R.Any     -> assert false
                  | L.Unl, R.Base    -> StringBuffer.write buf (R.to_string res_base)
+                 | L.Unl, R.Numeric -> StringBuffer.write buf (R.to_string res_numeric)
                  | L.Any, R.Session -> StringBuffer.write buf (R.to_string res_session)
                  | subknd ->
                     let policy = Policy.set_kinds Policy.Full (Context.policy ctx) in