Remove built-in application operator (@@)

edit: i'm double daft
amuletml · May 7, 2020 · 4fe1242 · 4fe1242
1 parent b5163d4
commit 4fe1242
Show file tree

Hide file tree

Showing 38 changed files with 73 additions and 66 deletions.
diff --git a/lib/amulet/base.ml b/lib/amulet/base.ml
@@ -11,6 +11,8 @@ let a || b =
 let a && b =
   if a then force b else false
 
+let f @@ x = f x
+
 let not a = if a then false else true
 
 (* Explicit type signatures for VTA: *)

diff --git a/lib/data/traversable.ml b/lib/data/traversable.ml
@@ -12,13 +12,13 @@ end
 
 instance traversable option begin
   let traverse cont = function
-    | Some x -> (| Some @@ cont x |)
+    | Some x -> (| Some (cont x) |)
     | None -> (| None |)
 end
 
 instance traversable (either 'a) begin
   let traverse cont = function
-    | Right a -> (| Right @@ cont a |)
+    | Right a -> (| Right (cont a) |)
     | Left b -> pure @@ Left b
 end
 

diff --git a/src/Backend/Lua/Builtin.hs b/src/Backend/Lua/Builtin.hs
@@ -91,13 +91,6 @@ builtins =
        end
       |] )
 
-  , ( vOpApp, "__builtin_app", [], Just (2, \[f, x] -> (mempty, [[lua| %f(%x) |]]))
-    , [luaStmts|
-      local function __builtin_app(f, x)
-        return f(x)
-      end
-    |] )
-
   , ( vRef, "__builtin_ref", []
     , Just (1, \[var] -> ( mempty, [ [lua| { %var, __tag = 'Ref' } |] ]))
     , [luaStmts|

diff --git a/src/Core/Builtin.hs b/src/Core/Builtin.hs
@@ -16,7 +16,6 @@ vBool, vInt, vString, vFloat, vUnit, vLazy, vArrow, vProduct, vList, vRefTy, vKS
 vError :: CoVar
 vLAZY, vForce :: CoVar
 tyvarA, tyvarB, argvarX :: CoVar
-vOpApp :: CoVar
 vCONS, vNIL :: CoVar
 vAssign, vDeref, vRef :: CoVar
 vStrVal, vIntVal :: CoVar
@@ -34,7 +33,7 @@ tyvarProxy :: CoVar
 
 tcTypeableApp, tcTypeableKnownKnown :: CoVar
 
-[ vBool, vInt, vString, vFloat, vUnit, vLazy, vArrow, vProduct, vList, vRefTy, vKStrTy, vKIntTy, vRowCons, vError, vLAZY, vForce, tyvarA, tyvarB, argvarX, vOpApp, vCONS, vNIL, vAssign, vDeref, vRef, vStrVal, vIntVal, vExtend, vRestrict, vKSTR, vKINT, vROWCONS, tyvarRecord, tyvarNew, tyvarKey, tyvarType, vEq, vEQ, backendRet, backendClone, tcTypeError, tcErrKind, tcString, tcHCat, tcVCat, tcShowType, tcTypeable, tcUnTypeable, tcTypeRep, tcTYPEABLE, tcTYPEREP, tcEqTypeRep, tcTypeableApp, tcTypeableKnownKnown, tyvarKind, tyvarProxy ] = makeBuiltins
+[ vBool, vInt, vString, vFloat, vUnit, vLazy, vArrow, vProduct, vList, vRefTy, vKStrTy, vKIntTy, vRowCons, vError, vLAZY, vForce, tyvarA, tyvarB, argvarX, vCONS, vNIL, vAssign, vDeref, vRef, vStrVal, vIntVal, vExtend, vRestrict, vKSTR, vKINT, vROWCONS, tyvarRecord, tyvarNew, tyvarKey, tyvarType, vEq, vEQ, backendRet, backendClone, tcTypeError, tcErrKind, tcString, tcHCat, tcVCat, tcShowType, tcTypeable, tcUnTypeable, tcTypeRep, tcTYPEABLE, tcTYPEREP, tcEqTypeRep, tcTypeableApp, tcTypeableKnownKnown, tyvarKind, tyvarProxy ] = makeBuiltins
   [ ("bool", TypeConVar)
   , ("int", TypeConVar)
   , ("string", TypeConVar)
@@ -58,8 +57,6 @@ tcTypeableApp, tcTypeableKnownKnown :: CoVar
   , ("b", TypeVar)
   , ("x", ValueVar)
 
-  , ("@@", ValueVar)
-
 -- Lists
   , ("Cons", DataConVar)
   , ("Nil", DataConVar)
@@ -171,12 +168,7 @@ builtinVarList = vars where
   appsTy = foldl1 AppTy
 
   vars :: [(a, Type)]
-  vars = [ op vOpApp
-            (ForallTy (Relevant name) StarTy $
-               ForallTy (Relevant name') StarTy $
-                 ValuesTy [VarTy name `arrTy` VarTy name', VarTy name] `arrTy` VarTy name')
-
-         , op vError (ForallTy (Relevant name) StarTy $ tyString `arrTy` VarTy name)
+  vars = [ op vError (ForallTy (Relevant name) StarTy $ tyString `arrTy` VarTy name)
          , op vLAZY (ForallTy (Relevant name) StarTy $
             (tyUnit `arrTy` VarTy name) `arrTy` AppTy tyLazy (VarTy name))
          , op vForce (ForallTy (Relevant name) StarTy $ AppTy tyLazy (VarTy name) `arrTy` VarTy name)

diff --git a/src/Core/Lower.hs b/src/Core/Lower.hs
@@ -565,7 +565,7 @@ boxedTys = VarMap.fromList
            . filter (flip VarSet.member boxed . fst)
            $ C.builtinVarList where
   boxed = VarSet.fromList
-    [ C.vOpApp, C.vAssign, C.vExtend, C.vRestrict
+    [ C.vAssign, C.vExtend, C.vRestrict
     , C.tcEqTypeRep
     , C.tcTypeableApp, C.tcTypeableKnownKnown
     ]
diff --git a/src/Syntax/Builtin.hs b/src/Syntax/Builtin.hs
@@ -26,7 +26,6 @@ module Syntax.Builtin
   , assignName, derefName, refName
 
   , cONSName, nILName, cONSTy, nILTy, cONSTy', nILTy'
-  , opAppName
 
   , strValName, strValTy, intValName, intValTy
   , knownStrName, knownStrTy, knownStrTy'
@@ -133,9 +132,6 @@ lAZYTy' x = TyArr tyUnit x ~> TyApp tyLazy x
 cONSTy' x = TyTuple x (TyApp tyList x) ~> TyApp tyList x
 nILTy' = TyApp tyList
 
-opAppName :: Var Typed
-opAppName = ofCore C.vOpApp
-
 strValName, knownStrName :: Var Typed
 strValName = ofCore C.vStrVal
 knownStrName = ofCore C.vKSTR
@@ -215,8 +211,7 @@ instance Monoid BuiltinPowule where
 builtins :: BuiltinPowule
 builtins =
   mempty
-  { vars = [ (opAppName, a *. b *. (var a ~> var b) ~> var a ~> var b)
-           , (lAZYName, lAZYTy)
+  { vars = [ (lAZYName, lAZYTy)
            , (forceName, forceTy)
            , (cONSName, cONSTy)
            , (nILName, nILTy)

diff --git a/src/Syntax/Desugar.hs b/src/Syntax/Desugar.hs
@@ -83,7 +83,6 @@ expr (Function bs p a) = do
     (Match rhs <$> traverse arm bs <*> pure p <*> pure a)
     <*> pure a
 -- Special case @@ so we can work on skolem variables
-expr (BinOp l (VarRef v _) r a) | v == opAppName = App <$> expr l <*> expr r <*> pure a
 expr (BinOp l o r a) = BinOp <$> expr l <*> expr o <*> expr r <*> pure a
 expr (Ascription e t a) = Ascription <$> expr e <*> pure (ty t) <*> pure a
 expr (Record rs a) = Record <$> traverse field rs <*> pure a

diff --git a/src/Syntax/Expr/Instances.hs b/src/Syntax/Expr/Instances.hs
@@ -100,6 +100,7 @@ deriving via AnnotatedVia (CompStmt p)  (Ann p)    instance Spanned (Ann p)    =
 parenFun :: Pretty (Var p) => Expr p -> Doc
 parenFun f = case f of
   Fun{} -> parens (pretty f)
+  Function{} -> parens (pretty f)
   Let{} -> parens (pretty f)
   Match{} -> parens (pretty f)
   _ -> pretty f

diff --git a/tests/lua/default-method.lua b/tests/lua/default-method.lua
@@ -1,4 +1,4 @@
 do
   local use = print
-  use(function(hc) return "tail" .. "()" end)
+  use(function(hf) return "tail" .. "()" end)
 end
diff --git a/tests/lua/default-method.ml b/tests/lua/default-method.ml
@@ -14,4 +14,6 @@ instance show () begin
   let show () = "()"
 end
 
+let f @@ x = f x
+
 let _ = use @@ (show_tail : unit -> string)
diff --git a/tests/lua/do_monad.lua b/tests/lua/do_monad.lua
@@ -1,6 +1,6 @@
 do
-  local function Cons(x) return { x, __tag = "Cons" } end
   local Nil = { __tag = "Nil" }
+  local function Cons(x) return { x, __tag = "Cons" } end
   local _greater_greater_equals = bind
   local pure = pure
   _greater_greater_equals({

diff --git a/tests/lua/emit_ifs.ml b/tests/lua/emit_ifs.ml
@@ -2,6 +2,8 @@ external val ignore : 'a -> () = "nil"
 external val print : 'a -> () = "print"
 external val bool : bool = "true"
 
+let f @@ x = f x
+
 let a && b = if a then b else false
 let a || b = if a then true else b
 let not a = if a then false else true

diff --git a/tests/lua/field_order.ml b/tests/lua/field_order.ml
@@ -1,5 +1,7 @@
 external val ignore : 'a -> () = "nil"
 
+let f @@ x = f x
+
 let () = ignore @@ fun f ->
   let a = f 1
   { b = f 2,

diff --git a/tests/lua/match_heuristic.lua b/tests/lua/match_heuristic.lua
@@ -35,7 +35,7 @@ do
       if tmp1.__tag == "Cons" then return 3 end
       return error("Pattern matching failure in match expression at match_heuristic.ml[11:15 ..14:21]")
     else
-      if tmp1.__tag ~= "Nil" then return 3 end
+      if tmp1.__tag == "Cons" then return 3 end
       if tmp0 == 2 then return 2 end
       return error("Pattern matching failure in match expression at match_heuristic.ml[11:15 ..14:21]")
     end

diff --git a/tests/lua/monoid.lua b/tests/lua/monoid.lua
@@ -13,18 +13,18 @@ do
     return function(y) return { { _1 = x, _2 = y }, __tag = "Cons" } end
   end
   local function _dollartraverse(cak, tmp, k, x)
-    if x.__tag == "Nil" then return tmp.pure(Nil) end
+    if x.__tag ~= "Cons" then return tmp.pure(Nil) end
     local tmp0 = x[1]
     return tmp["<*>"](tmp["Applicative$ky"](_colon_colon)(k(tmp0._1)))(_dollartraverse(nil, tmp, k, tmp0._2))
   end
   local function _dollar_d7(cgs, x, ys)
-    if x.__tag == "Nil" then return ys end
+    if x.__tag ~= "Cons" then return ys end
     local tmp = x[1]
     return { { _2 = _dollar_d7(nil, tmp._2, ys), _1 = tmp._1 }, __tag = "Cons" }
   end
   local tmp = { _1 = 1, _2 = nil }
   local function _dollarshow_sat(x)
-    if x.__tag == "Nil" then return "Nil" end
+    if x.__tag ~= "Cons" then return "Nil" end
     local tmp = x[1]
     return _tostring(tmp._1) .. " :: " .. _dollarshow_sat(tmp._2)
   end

diff --git a/tests/lua/nested_match.lua b/tests/lua/nested_match.lua
@@ -2,9 +2,9 @@ do
   local Nil = { __tag = "Nil" }
   local function zip(f)
     local function zip_sat(xs, ys)
-      if xs.__tag == "Nil" then return { { _1 = 1, _2 = Nil }, __tag = "Cons" } end
+      if xs.__tag ~= "Cons" then return { { _1 = 1, _2 = Nil }, __tag = "Cons" } end
       local tmp = xs[1]
-      if ys.__tag == "Nil" then return { { _1 = 2, _2 = Nil }, __tag = "Cons" } end
+      if ys.__tag ~= "Cons" then return { { _1 = 2, _2 = Nil }, __tag = "Cons" } end
       local tmp0, tmp1 = tmp._1, tmp._2
       local tmp2 = ys[1]
       local tmp3, tmp4 = tmp2._1, tmp2._2

diff --git a/tests/lua/nested_match_basic.lua b/tests/lua/nested_match_basic.lua
@@ -2,9 +2,9 @@ do
   local Nil = { __tag = "Nil" }
   local function zip(f)
     local function zip_sat(xs, ys)
-      if xs.__tag == "Nil" then return { { _1 = 1, _2 = Nil }, __tag = "Cons" } end
+      if xs.__tag ~= "Cons" then return { { _1 = 1, _2 = Nil }, __tag = "Cons" } end
       local tmp = xs[1]
-      if ys.__tag == "Nil" then return { { _1 = 2, _2 = Nil }, __tag = "Cons" } end
+      if ys.__tag ~= "Cons" then return { { _1 = 2, _2 = Nil }, __tag = "Cons" } end
       local tmp0 = ys[1]
       return { { _1 = f(tmp._1)(tmp0._1), _2 = zip_sat(tmp._2, tmp0._2) }, __tag = "Cons" }
     end

diff --git a/tests/lua/op_apply.lua b/tests/lua/op_apply.lua
@@ -1,10 +1,8 @@
 do
-  local function _at_at(tmp) return function(tmp0) return tmp(tmp0) end end
-  local function tmp(x) return x end
   (nil)({
-    op = _at_at,
+    op = function(f) return f end,
+    app = 2,
     rsec = function(r) return r(2) end,
-    lsec = function(tmp0) return tmp(tmp0) end,
-    app = 2
+    lsec = function(x) return x end
   })
 end
diff --git a/tests/lua/op_apply.ml b/tests/lua/op_apply.ml
@@ -1,5 +1,7 @@
 let id x = x
 
+let f @@ x = f x
+
 external val ignore : 'a -> () = "nil"
 let () = ignore { op = (@@)
                 , app = id @@ 2

diff --git a/tests/lua/opt_record_inline.lua b/tests/lua/opt_record_inline.lua
@@ -19,10 +19,10 @@ do
     return { _1 = x0, _2 = x0 }
   end);
   (nil)(function(x)
-    local gm = __builtin_clone(x)
-    gm.a = 2
+    local iz = __builtin_clone(x)
+    iz.a = 2
     local x0 = __builtin_clone(x)
     x0.a = 1
-    return { _1 = x0, _2 = gm }
+    return { _1 = x0, _2 = iz }
   end)
 end
diff --git a/tests/lua/opt_record_inline.ml b/tests/lua/opt_record_inline.ml
@@ -1,5 +1,7 @@
 external val ignore : 'a -> () = "nil"
 
+let f @@ x = f x
+
 (* Flatten nested record updates *)
 let () = ignore @@ fun x ->
   let x = { x with a = 1, c = 2 }

diff --git a/tests/lua/opt_sat.lua b/tests/lua/opt_sat.lua
@@ -3,15 +3,15 @@ do
   local use = print
   local function map(f)
     local function map_sat(x)
-      if x.__tag == "Nil" then return Nil end
+      if x.__tag ~= "Cons" then return Nil end
       local tmp = x[1]
       return { { _1 = f(tmp._1), _2 = map_sat(tmp._2) }, __tag = "Cons" }
     end
     return map_sat
   end
   use(map)
   local function map_no_sat(f, x)
-    if x.__tag == "Nil" then return Nil end
+    if x.__tag ~= "Cons" then return Nil end
     local tmp = x[1]
     map_no_sat(nil, Nil)
     return { { _1 = f(tmp._1), _2 = map(f)(tmp._2) }, __tag = "Cons" }

diff --git a/tests/lua/opt_sat_unsat.lua b/tests/lua/opt_sat_unsat.lua
@@ -2,7 +2,7 @@ do
   local Nil = { __tag = "Nil" }
   local map, map0
   map = function(f, x)
-    if x.__tag == "Nil" then return Nil end
+    if x.__tag ~= "Cons" then return Nil end
     map0(function(x0) return x0 end)({ { _1 = 1, _2 = Nil }, __tag = "Cons" })
     local tmp = x[1]
     return { { _1 = f(tmp._1), _2 = map(f, tmp._2) }, __tag = "Cons" }

diff --git a/tests/lua/optimise_sink.lua b/tests/lua/optimise_sink.lua
@@ -1,8 +1,8 @@
 do
   local Nil = { __tag = "Nil" }
   local function main(x)
-    if x.__tag == "Nil" then return function(tmp) return { _1 = 1, _2 = x } end end
-    return function(x0) return { _1 = x0, _2 = Nil } end
+    if x.__tag == "Cons" then return function(x0) return { _1 = x0, _2 = Nil } end end
+    return function(tmp) return { _1 = 1, _2 = x } end
   end
   (nil)(main)
 end
diff --git a/tests/lua/or_pattern.lua b/tests/lua/or_pattern.lua
@@ -5,25 +5,25 @@ do
   ignore(function(tmp)
     local num, opt = tmp.num, tmp.opt
     if num == 1 then
-      ignore(0)
       local tmp0 = opt._1
       local tmp1 = opt._2
+      ignore(0)
       if tmp0.__tag == "None" then return ignore(None) end
       local x = tmp0[1]
       if tmp1.__tag == "None" then return ignore(None) end
       return ignore(Some({ _1 = x, _2 = tmp1[1] }))
     elseif num == 2 then
-      ignore(0)
       local tmp0 = opt._1
       local tmp1 = opt._2
+      ignore(0)
       if tmp0.__tag == "None" then return ignore(None) end
       local x = tmp0[1]
       if tmp1.__tag == "None" then return ignore(None) end
       return ignore(Some({ _1 = x, _2 = tmp1[1] }))
     elseif num == 3 then
-      ignore(0)
       local tmp0 = opt._1
       local tmp1 = opt._2
+      ignore(0)
       if tmp0.__tag == "None" then return ignore(None) end
       local x = tmp0[1]
       if tmp1.__tag == "None" then return ignore(None) end

diff --git a/tests/lua/or_pattern.ml b/tests/lua/or_pattern.ml
@@ -2,6 +2,8 @@ type option 'a = None | Some of 'a
 
 external val ignore : 'a -> () = "ignore"
 
+let f @@ x = f x
+
 let () = ignore @@ fun { num, opt }->
   ignore @@ match num with
   | 1 | 2 | 3 -> 0

diff --git a/tests/lua/pattern_guard.lua b/tests/lua/pattern_guard.lua
@@ -2,7 +2,7 @@ do
   local Nil = { __tag = "Nil" }
   local function filter(f)
     local function filter_sat(x)
-      if x.__tag == "Nil" then return Nil end
+      if x.__tag ~= "Cons" then return Nil end
       local tmp = x[1]
       local x0, xs = tmp._1, tmp._2
       if f(x0) then return { { _1 = x0, _2 = filter_sat(xs) }, __tag = "Cons" } end

diff --git a/tests/lua/precedence.ml b/tests/lua/precedence.ml
@@ -4,6 +4,8 @@ external val ( *. )  : float -> float -> float = "function(x, y) return x * y en
 external val ( /. )  : float -> float -> float = "function(x, y) return x / y end"
 external val ignore : 'a -> () = "nil"
 
+let f @@ x = f x
+
 let main { a, b, c } =
   (* Lower precedence *)
   ignore @@ (a +. b) *. c

diff --git a/tests/types/class/mtpc-scope.ml b/tests/types/class/mtpc-scope.ml
@@ -2,6 +2,8 @@ class functor 'f begin
   val map : ('a -> 'b) -> 'f 'a -> 'f 'b
 end
 
+let f @@ x = f x
+
 class functor 'f => foldable 'f begin
 end
 

diff --git a/tests/types/class/mtpc-scope.out b/tests/types/class/mtpc-scope.out
@@ -1,10 +1,11 @@
 functor : Req{'f : type -> type}. constraint
 map : Spec{'f : type -> type}. functor 'f => Spec{'a : type}. Spec{'b : type}. ('a -> 'b) -> 'f 'a -> 'f 'b
+@@ : Infer{'a : type}. Infer{'b : type}. ('a -> 'b) -> 'a -> 'b
 foldable : Req{'f : type -> type}. constraint
-iapplicative : Infer{'kn : type}. Req{'f : 'kn -> 'kn -> type -> type}. constraint
-<*> : Spec{'f : 'kn -> 'kn -> type -> type}. iapplicative 'f => Infer{'kn : type}. Spec{'a : type}. Spec{'b : type}. Spec{'i : 'kn}. Spec{'j : 'kn}. Spec{'k : 'kn}. 'f 'i 'j ('a -> 'b) -> 'f 'j 'k 'a -> 'f 'i 'k 'b
-pure : Spec{'f : 'kn -> 'kn -> type -> type}. iapplicative 'f => Infer{'kn : type}. Spec{'a : type}. Spec{'i : 'kn}. 'a -> 'f 'i 'i 'a
-imonad : Infer{'aac : type}. Req{'m : 'aac -> 'aac -> type -> type}. constraint
->>= : Spec{'m : 'aac -> 'aac -> type -> type}. imonad 'm => Infer{'aac : type}. Spec{'a : type}. Spec{'b : type}. Spec{'i : 'aac}. Spec{'j : 'aac}. Spec{'k : 'aac}. ('a -> 'm 'j 'k 'b) -> 'm 'i 'j 'a -> 'm 'i 'k 'b
+iapplicative : Infer{'mc : type}. Req{'f : 'mc -> 'mc -> type -> type}. constraint
+<*> : Spec{'f : 'mc -> 'mc -> type -> type}. iapplicative 'f => Infer{'mc : type}. Spec{'a : type}. Spec{'b : type}. Spec{'i : 'mc}. Spec{'j : 'mc}. Spec{'k : 'mc}. 'f 'i 'j ('a -> 'b) -> 'f 'j 'k 'a -> 'f 'i 'k 'b
+pure : Spec{'f : 'mc -> 'mc -> type -> type}. iapplicative 'f => Infer{'mc : type}. Spec{'a : type}. Spec{'i : 'mc}. 'a -> 'f 'i 'i 'a
+imonad : Infer{'aar : type}. Req{'m : 'aar -> 'aar -> type -> type}. constraint
+>>= : Spec{'m : 'aar -> 'aar -> type -> type}. imonad 'm => Infer{'aar : type}. Spec{'a : type}. Spec{'b : type}. Spec{'i : 'aar}. Spec{'j : 'aar}. Spec{'k : 'aar}. ('a -> 'm 'j 'k 'b) -> 'm 'i 'j 'a -> 'm 'i 'k 'b
 iio : Infer{'a : type}. Infer{'b : type}. 'b -> 'a -> type -> type
 IIO : Infer{'a : type}. Infer{'b : type}. Spec{'before : 'b}. Spec{'after : 'a}. Spec{'a : type}. (unit -> 'a) -> iio 'before 'after 'a
diff --git a/tests/types/class/tyfam-equality-instance.ml b/tests/types/class/tyfam-equality-instance.ml
@@ -47,6 +47,8 @@ end
 
 let unfix (Fix f) = f
 
+let f @@ x = f x
+
 let cata phi x =
   let rec cata_base phi x =
     phi @@ (cata_base phi <$>) @@ unfix x
-Original file line number
+Diff line change
@@ Expand Up / @@ -2,6 +2,8 @@ class functor 'f begin @@
       val map : ('a -> 'b) -> 'f 'a -> 'f 'b
     end
+    let f @@ x = f x
     class functor 'f => foldable 'f begin
     end
@@ Expand Down @@