Re-do idiom brackets in TC

This lets us do (| a + b |) as a shorthand for (| (+) a b |)

lib/data/traversable.ml

@@ -11,14 +11,14 @@ end
 
 instance traversable option begin
   let traverse cont = function
-    | Some x -> (| Some (cont x) |)
-    | None -> pure None
+    | Some x -> (| Some @@ cont x |)
+    | None -> (| None |)
 end
 
 instance traversable list begin
   let traverse cont =
     let loop = function
-      | Cons (x, xs) -> (| cons (cont x) (loop xs) |)
-      | [] -> pure []
+      | Cons (x, xs) -> (| cont x :: loop xs |)
+      | [] -> (| [] |)
     loop
 end

src/Control/Monad/Infer.hs

@@ -162,6 +162,7 @@ data TypeError where
 
   MightNotTerminate :: TyFunClause Typed -> Type Typed -> Type Typed -> TypeError
   TyFunInLhs :: SomeReason -> Type Typed -> TypeError
+  NotAnIdiom :: Pretty (Var p) => Expr p -> TypeError
 
 
 data WhatOverlaps = Overinst | Overeq Bool
@@ -581,6 +582,9 @@ instance Pretty TypeError where
   pretty (TyFunInLhs _ tau) =
     vsep [ "Type synonym application" <+> displayType tau <+> "is illegal in LHS of type function equation" ]
 
+  pretty (NotAnIdiom _) =
+    vsep [ "This expression can not be used in an idiom bracket because it is not a function application" ]
+
   pretty (WarningError x) = pretty x
 
   pretty (UnsatClassCon _ (ConImplicit _ _ _ t) _) = string "No instance for" <+> pretty t

src/Parser.y

@@ -338,7 +338,7 @@ Atom :: { Expr Parsed }
      | hole                                   { withPos1 $1 (Hole (Name (getHole $1))) }
      | '_'                                    { withPos1 $1 (Hole (Name (T.singleton '_'))) }
      | begin List1(CompStmt, ExprSep) end     { withPos2 $1 $3 $ DoExpr bindVar $2 }
-     | '(|' Expr0 ListE1(PreAtom) '|)'        { withPos2 $1 $4 $ Idiom pureVar apVar ($2:$3) }
+     | '(|' Expr '|)'                         { withPos2 $1 $3 $ Idiom pureVar apVar $2 }
      | '(' ')'                                { withPos2 $1 $2 $ Literal LiUnit }
      | '(' Section ')'                        { withPos2 $1 $3 $ Parens $2 }
      | '(' NullSection ',' List1(NullSection, ',') ')'

src/Syntax/Desugar.hs

@@ -129,15 +129,7 @@ expr (ListComp e qs an) = transListComp (e, qs, an) (ListExp [] an)
 expr (DoExpr bind qs an) = begin <$> transDoExpr (VarRef bind an) qs where
   begin = flip Begin an . (:[])
 
-expr (Idiom _ _ [] _) = error "parse error Idiom made it to Ds"
-expr (Idiom pure_v app_v (fn:args) an) =
-  do
-    fn <- expr fn
-    foldl mkapp (App pure fn an) <$> traverse expr args
-  where
-    mkapp f x = App (App app f an) x an
-    pure = VarRef pure_v an
-    app = VarRef app_v an
+expr (Idiom pure_v app_v fn an) = Idiom pure_v app_v <$> expr fn <*> pure an
 
 expr (OpenIn mod e an) = OpenIn <$> modTerm mod <*> expr e <*> pure an
 

src/Syntax/Expr.hs

@@ -93,7 +93,8 @@ data Expr p
   | ListComp (Expr p) [CompStmt p] (Ann p)
   -- Monads
   | DoExpr (Var p) [CompStmt p] (Ann p)
-  | Idiom (Var p) (Var p) [Expr p] (Ann p)
+  | Idiom (Var p) (Var p) (Expr p) (Ann p)
+  -- Idiom brackets just take a single Expr; the TC knows how to handle them
 
   | ExprWrapper (Wrapper p) (Expr p) (Ann p)
 

src/Syntax/Expr/Instances.hs

@@ -151,7 +151,7 @@ instance Pretty (Var p) => Pretty (Expr p) where
   pretty (ListExp es _) = brackets (hsep (punctuate comma (map pretty es)))
   pretty (ListComp e qs _) =
     brackets (pretty e <+> pipe <+> hsep (punctuate comma (map pretty qs)))
-  pretty (Idiom _ _ xs _) = "(|" <+> hsep (map parenArg xs) <+> "|)"
+  pretty (Idiom _ _ xs _) = "(|" <+> pretty xs <+> "|)"
 
   pretty (ExprWrapper wrap ex an) = go wrap ex where
     go (TypeLam v t) ex =

src/Syntax/Let.hs

@@ -62,7 +62,7 @@ freeIn (RightSection a b _) = freeIn a <> freeIn b
 freeIn (BothSection b _) = freeIn b
 freeIn AccessSection{} = mempty
 freeIn (Vta e _ _) = freeIn e
-freeIn (Idiom vp va es _) = Set.fromList [vp, va] <> foldMap freeIn es
+freeIn (Idiom vp va es _) = Set.fromList [vp, va] <> freeIn es
 freeIn (ListExp e _) = foldMap freeIn e
 freeIn (ListComp e qs _) = freeIn e <> freeInStmt qs
 freeIn (DoExpr v qs _) = freeInStmt qs <> bind where

src/Syntax/Resolve.hs

@@ -388,7 +388,7 @@ reExpr (ListComp e qs a) =
       go [] acc = ListComp <$> reExpr e <*> pure (reverse acc) <*> pure a
   in go qs []
 
-reExpr r@(Idiom vp va es a) = Idiom <$> lookupEx' vp <*> lookupEx' va <*> traverse reExpr es <*> pure a where
+reExpr r@(Idiom vp va es a) = Idiom <$> lookupEx' vp <*> lookupEx' va <*> reExpr es <*> pure a where
   lookupEx' v = lookupEx v `catchJunk` r
 
 reExpr (DoExpr var qs a) =

src/Syntax/Transform.hs

@@ -105,7 +105,7 @@ transformExpr fe = goE where
   transE (ListExp e a) = ListExp (map goE e) a
   transE (ListComp e qs a) = ListComp (goE e) (map goQ qs) a
   transE (DoExpr v qs a) = DoExpr v (map goQ qs) a
-  transE (Idiom vp va es a) = Idiom vp va (map goE es) a
+  transE (Idiom vp va es a) = Idiom vp va (goE es) a
 
   goB (Binding v e c a) = Binding v (goE e) c a
   goB (TypedMatching v e a b) = TypedMatching v (goE e) a b
@@ -159,7 +159,7 @@ transformExprTyped fe fc ft = goE where
   transE (ListExp e a) = ListExp (map goE e) (goA a)
   transE (ListComp e qs a) = ListComp (transE e) (map goQ qs) (goA a)
   transE (DoExpr v qs a) = DoExpr v (map goQ qs) (goA a)
-  transE (Idiom vp va es a) = Idiom vp va (map goE es) (goA a)
+  transE (Idiom vp va es a) = Idiom vp va (goE es) (goA a)
 
   transBind (Binding v e b a) = Binding v (goE e) b (goA a)
   transBind (Matching p e a) = Matching (goP p) (goE e) (goA a)

src/Syntax/Verify.hs

@@ -165,7 +165,7 @@ verifyExpr (Vta e _ _) = verifyExpr e
 verifyExpr (OpenIn _ e _) = verifyExpr e
 verifyExpr (ListExp e _) = traverse_ verifyExpr e
 verifyExpr (ListComp e qs _) = verifyExpr e *> traverse_ verifyCompStmt qs
-verifyExpr (Idiom _ _ es _) = traverse_ verifyExpr es
+verifyExpr (Idiom _ _ es _) = verifyExpr es
 verifyExpr (DoExpr _ qs _) = traverse_ verifyCompStmt qs
 verifyExpr (ExprWrapper w e a) =
   case w of

src/Types/Infer.hs

@@ -315,6 +315,23 @@ infer (OpenIn mod expr a) = do
     (expr', ty) <- infer expr
     pure (ExprWrapper (TypeAsc ty) (OpenIn mod' (ExprWrapper (TypeAsc ty) expr' (a, ty)) (a, ty)) (a, ty), ty)
 
+infer (Idiom pure_v app_v expr ann) =
+  do
+    ~(fn:as) <- reverse <$> spine expr
+    infer (make_idiom fn as)
+  where
+    spine (BinOp l o r _) = pure [ r, l, o ]
+    spine (App f x _) = do
+      sp <- spine f
+      pure (x:sp)
+    spine ex@Fun{} = pure [ex]
+    spine ex@VarRef{} = pure [ex]
+    spine ex@ListExp{} = pure [ex]
+    spine x = confesses (addBlame (becauseExp expr) (NotAnIdiom x))
+
+    make_idiom fun =
+      foldl (\f x -> BinOp f (VarRef app_v ann) x ann) (App (VarRef pure_v ann) fun ann)
+
 infer ex = do
   x <- freshTV
   ex' <- check ex x

tests/amc/prelude.t

@@ -8,26 +8,27 @@ Repl will be launched with the prelude
 
 Not using the prelude will fail
 
-  $ echo 'print "Hello"' | amc repl --port 0 --no-prelude
+  $ echo 'print "Hello"' | amc repl --no-prelude
+  Listening on port 5478
   > =stdin[1:1 ..1:5]: error
     Variable not in scope: `print`
 
     Arising from use of the expression
     │ 
   1 │ print "Hello"
     │ ^^^^^
-  > amc: thread killed
+  > 
 
 One can use a custom prelude
 
-  $ echo 'print "Hello"' | amc repl --port 0 --prelude=tests/amc/lib/prelude.ml
+  $ echo 'print "Hello"' | amc repl --prelude=tests/amc/lib/prelude.ml
   Listening on port 5478
   > =stdin:2: Hello
   > 
 
 Prelude is found from the library path
 
-  $ echo 'print "Hello"' | amc repl --port 0 --lib=tests/amc/lib
+  $ echo 'print "Hello"' | amc repl --lib=tests/amc/lib
   Listening on port 5478
   > =stdin:2: Hello
   > 

tests/types/idioms.ml

@@ -2,3 +2,11 @@ let pure x = [x]
 let fs <*> xs = [ f x | with f <- fs, with x <- xs ]
 
 let cartesian xs ys = (| (,) xs ys |)
+
+let x :: xs = Cons (x, xs)
+
+let traverse cont =
+  let loop = function
+    | Cons (x, xs) -> (| cont x :: loop xs |)
+    | [] -> (| [] |)
+  loop

tests/types/idioms.out

@@ -1,3 +1,5 @@
 pure : Infer{'a : type}. 'a -> list 'a
 <*> : Infer{'a : type}. Infer{'b : type}. list ('b -> 'a) -> list 'b -> list 'a
 cartesian : Infer{'b : type}. Infer{'a : type}. list 'a -> list 'b -> list ('a * 'b)
+:: : Infer{'a : type}. 'a -> list 'a -> list 'a
+traverse : Infer{'b : type}. Infer{'a : type}. ('a -> list 'b) -> list 'a -> list (list 'b)