From 4fe124287c6bc148e91193d9d33778d9c55aef35 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?= Date: Wed, 6 May 2020 19:39:03 -0300 Subject: [PATCH] Remove built-in application operator (@@) edit: i'm double daft --- lib/amulet/base.ml | 2 ++ lib/data/traversable.ml | 4 ++-- src/Backend/Lua/Builtin.hs | 7 ------- src/Core/Builtin.hs | 12 ++---------- src/Core/Lower.hs | 2 +- src/Syntax/Builtin.hs | 7 +------ src/Syntax/Desugar.hs | 1 - src/Syntax/Expr/Instances.hs | 1 + tests/lua/default-method.lua | 2 +- tests/lua/default-method.ml | 2 ++ tests/lua/do_monad.lua | 2 +- tests/lua/emit_ifs.ml | 2 ++ tests/lua/field_order.ml | 2 ++ tests/lua/match_heuristic.lua | 2 +- tests/lua/monoid.lua | 6 +++--- tests/lua/nested_match.lua | 4 ++-- tests/lua/nested_match_basic.lua | 4 ++-- tests/lua/op_apply.lua | 8 +++----- tests/lua/op_apply.ml | 2 ++ tests/lua/opt_record_inline.lua | 6 +++--- tests/lua/opt_record_inline.ml | 2 ++ tests/lua/opt_sat.lua | 4 ++-- tests/lua/opt_sat_unsat.lua | 2 +- tests/lua/optimise_sink.lua | 4 ++-- tests/lua/or_pattern.lua | 6 +++--- tests/lua/or_pattern.ml | 2 ++ tests/lua/pattern_guard.lua | 2 +- tests/lua/precedence.ml | 2 ++ tests/types/class/mtpc-scope.ml | 2 ++ tests/types/class/mtpc-scope.out | 11 ++++++----- tests/types/class/tyfam-equality-instance.ml | 2 ++ tests/types/class/tyfam-equality-instance.out | 1 + tests/types/gadt/gadt09-pass.ml | 1 + tests/types/gadt/gadt09-pass.out | 7 ++++--- tests/types/gadt/pass_existential.ml | 2 ++ tests/types/gadt/pass_existential.out | 5 +++-- tests/types/tyfun/soundness.ml | 2 ++ tests/types/tyfun/soundness.out | 4 ++-- 38 files changed, 73 insertions(+), 66 deletions(-) diff --git a/lib/amulet/base.ml b/lib/amulet/base.ml index 6d29b6289..6a7b2b2d9 100644 --- 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 index 1c81f4607..fb0ba02d0 100644 --- 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 index 215f9de01..0e620b2cc 100644 --- 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 index 01407b7af..9527e0dfc 100644 --- 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 index 1a34738ca..772abe522 100644 --- 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 index cb29818ef..a5f1e314f 100644 --- 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 index 2389a26e4..f8a0bff1e 100644 --- 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 index f199d06fe..b73bc9ad4 100644 --- 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 index 60e148d1f..eca501b29 100644 --- 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 index 9095b093d..19b5298d1 100644 --- 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 index 70fc40189..eca14b63f 100644 --- 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 index 6c2c6dae5..3b3d2a9c0 100644 --- 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 index be0227422..a16e78773 100644 --- 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 index 253865e90..df7239430 100644 --- 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 index 41e6d5ae4..94cde7788 100644 --- 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 index 9cfc3faa2..9d9be3c67 100644 --- 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 index 7a4e8e567..43739e438 100644 --- 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 index f9e435114..b7b615f8a 100644 --- 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 index a9705a58e..552c2a245 100644 --- 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 index 81179ea73..e22f362bf 100644 --- 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 index 77e2b69e1..93294bbe7 100644 --- 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 index 8f76e3da5..d089be2cb 100644 --- a/tests/lua/opt_sat.lua +++ b/tests/lua/opt_sat.lua @@ -3,7 +3,7 @@ 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 @@ -11,7 +11,7 @@ do 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 index 8fe8a0f6a..1316b2ea0 100644 --- 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 index 9dc348061..38dbdb3a0 100644 --- 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 index 472d53e3f..30426b95e 100644 --- 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 index 2229ce214..f29869214 100644 --- 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 index 47ea3f8d4..dd049d8b5 100644 --- 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 index 572ae3ac5..7a13e6136 100644 --- 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 index 8a1177443..93054ac0c 100644 --- 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 index 012a4ac35..fb6c6e057 100644 --- 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 index 6e3f38915..1761fe674 100644 --- 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 diff --git a/tests/types/class/tyfam-equality-instance.out b/tests/types/class/tyfam-equality-instance.out index e4fe72be4..b9a45943a 100644 --- a/tests/types/class/tyfam-equality-instance.out +++ b/tests/types/class/tyfam-equality-instance.out @@ -16,4 +16,5 @@ rep : Req{'t : type}. type -> type from : Spec{'t : type}. recursive 't => fix (rep 't) -> 't into : Spec{'t : type}. recursive 't => 't -> fix (rep 't) unfix : Infer{'f : type -> type}. fix 'f -> 'f (fix 'f) +@@ : Infer{'a : type}. Infer{'b : type}. ('a -> 'b) -> 'a -> 'b cata : Infer{'a : type}. Infer{'b : type}. recursive 'a => (rep 'a 'b -> 'b) -> 'a -> 'b diff --git a/tests/types/gadt/gadt09-pass.ml b/tests/types/gadt/gadt09-pass.ml index db92f1191..45af62138 100644 --- a/tests/types/gadt/gadt09-pass.ml +++ b/tests/types/gadt/gadt09-pass.ml @@ -6,6 +6,7 @@ type repr 'a = | Int : repr int type option 'a = Some of 'a | None +let f @@ x = f x let (<$>) f = function | Some x -> Some (f x) diff --git a/tests/types/gadt/gadt09-pass.out b/tests/types/gadt/gadt09-pass.out index 8f802ad33..02743b220 100644 --- a/tests/types/gadt/gadt09-pass.out +++ b/tests/types/gadt/gadt09-pass.out @@ -1,11 +1,12 @@ print : string -> unit repr : type -> type -Unit : Infer{'cm : type}. Spec{'a : 'cm}. ('a ~ unit) ⊃ repr 'a -Pair : Infer{'dr : type}. Spec{'a : 'dr}. Spec{'a : type}. Spec{'b : type}. ('a ~ 'a * 'b) ⊃ (repr 'a * repr 'b) -> repr 'a -Int : Infer{'eu : type}. Spec{'a : 'eu}. ('a ~ int) ⊃ repr 'a +Unit : Infer{'cp : type}. Spec{'a : 'cp}. ('a ~ unit) ⊃ repr 'a +Pair : Infer{'du : type}. Spec{'a : 'du}. Spec{'a : type}. Spec{'b : type}. ('a ~ 'a * 'b) ⊃ (repr 'a * repr 'b) -> repr 'a +Int : Infer{'ex : type}. Spec{'a : 'ex}. ('a ~ int) ⊃ repr 'a option : type -> type Some : Spec{'a : type}. 'a -> option 'a None : Spec{'a : type}. option 'a +@@ : Infer{'a : type}. Infer{'b : type}. ('a -> 'b) -> 'a -> 'b <$> : Infer{'a : type}. Infer{'b : type}. ('b -> 'a) -> option 'b -> option 'a <*> : Infer{'a : type}. Infer{'b : type}. option ('b -> 'a) -> option 'b -> option 'a cast : Spec{'a : type}. Spec{'b : type}. repr 'a -> repr 'b -> 'a -> option 'b diff --git a/tests/types/gadt/pass_existential.ml b/tests/types/gadt/pass_existential.ml index 85ecb220a..a7f206944 100644 --- a/tests/types/gadt/pass_existential.ml +++ b/tests/types/gadt/pass_existential.ml @@ -12,6 +12,8 @@ type nat 'n = type some_nat = | SomeNat : nat 'n -> some_nat +let f @@ x = f x + let with_natural i (k : forall 'n. nat 'n -> 'b) = let rec go n = if n == 0 then diff --git a/tests/types/gadt/pass_existential.out b/tests/types/gadt/pass_existential.out index 1855fa6a2..104648e43 100644 --- a/tests/types/gadt/pass_existential.out +++ b/tests/types/gadt/pass_existential.out @@ -6,9 +6,10 @@ natural : type Z : natural S : natural -> natural nat : natural -> type -Zero : Infer{'dv : type}. Spec{'n : 'dv}. ('n ~ Z) ⊃ nat 'n -Succ : Infer{'ew : type}. Spec{'n : 'ew}. Spec{'k : natural}. ('n ~ S 'k) ⊃ nat 'k -> nat 'n +Zero : Infer{'dy : type}. Spec{'n : 'dy}. ('n ~ Z) ⊃ nat 'n +Succ : Infer{'ez : type}. Spec{'n : 'ez}. Spec{'k : natural}. ('n ~ S 'k) ⊃ nat 'k -> nat 'n some_nat : type SomeNat : Spec{'n : natural}. nat 'n -> some_nat +@@ : Infer{'a : type}. Infer{'b : type}. ('a -> 'b) -> 'a -> 'b with_natural : Infer{'a : type}. int -> (Spec{'n : natural}. nat 'n -> 'a) -> 'a main : unit diff --git a/tests/types/tyfun/soundness.ml b/tests/types/tyfun/soundness.ml index d3e7ffe48..7f052ae17 100644 --- a/tests/types/tyfun/soundness.ml +++ b/tests/types/tyfun/soundness.ml @@ -18,6 +18,8 @@ let sym (Dict : dict ('a ~ 'b)) : dict ('b ~ 'a) = Dict let sub (Dict : dict ('a ~ 'b)) (x : 'a) : 'b = x +let f @@ x = f x + let foo : forall 'a 'b. 'a ~ 'b :- (discrim 'a 'b ~ int) = Sub (fun _ -> Dict) let no : forall 'a 'b. trivial :- (discrim 'a 'b ~ string) = Sub (fun _ -> Dict) let oh_no : dict (string ~ int) = diff --git a/tests/types/tyfun/soundness.out b/tests/types/tyfun/soundness.out index 57bdf7b68..05f13df7b 100644 --- a/tests/types/tyfun/soundness.out +++ b/tests/types/tyfun/soundness.out @@ -1,5 +1,5 @@ -soundness.ml[22:1 ..22:80]: error (E2018) +soundness.ml[24:1 ..24:80]: error (E2018) │ -22 │ let no : forall 'a 'b. trivial :- (discrim 'a 'b ~ string) = Sub (fun _ -> Dict) +24 │ let no : forall 'a 'b. trivial :- (discrim 'a 'b ~ string) = Sub (fun _ -> Dict) │ ^^^^ No instance for discrim 'a 'b ~ string arising from this expression