WIP

src/lib/AbstractSyntax.hs

@@ -112,7 +112,7 @@ topDecl = dropSrc topDecl' where
     tyConParams' <- aExplicitParams tyConParams
     givens' <- aOptGivens givens
     constructors' <- forM constructors \(v, ps) -> do
-      ps' <- toNest <$> mapM tyOptBinder ps
+      ps' <- toNest <$> mapM (tyOptBinder Explicit) ps
       return (v, ps')
     return $ UDataDefDecl
       (UDataDef name (givens' >>> tyConParams') $
@@ -134,8 +134,6 @@ topDecl = dropSrc topDecl' where
       return (fromString methodName, ty')
     return $ UInterface params' methodTys (fromString name) (toNest methodNames)
   topDecl' (CInstanceDecl def) = aInstanceDef def
-  topDecl' (CEffectDecl _ _) = error "not implemented"
-  topDecl' (CHandlerDecl _ _ _ _ _ _) = error "not implemented"
 
 decl :: LetAnn -> CSDecl -> SyntaxM (UDecl VoidS VoidS)
 decl ann = propagateSrcB \case
@@ -167,14 +165,14 @@ aInstanceDef (CInstanceDef clName args givens methods instNameAndParams) = do
 
 aDef :: CDef -> SyntaxM (SourceName, ULamExpr VoidS)
 aDef (CDef name params optRhs optGivens body) = do
-  explicitParams <- aExplicitParams params
+  explicitParams <- explicitBindersOptAnn params
   let rhsDefault = (ExplicitApp, Nothing, Nothing)
   (expl, effs, resultTy) <- fromMaybeM optRhs rhsDefault \(expl, optEffs, resultTy) -> do
     effs <- fromMaybeM optEffs UPure aEffects
     resultTy' <- expr resultTy
     return (expl, Just effs, Just resultTy')
   implicitParams <- aOptGivens optGivens
-  let allParams = fmapNest asOptAnn $ implicitParams >>> explicitParams
+  let allParams = fmapNest asOptAnn implicitParams >>> explicitParams
   body' <- block body
   return (name, ULamExpr allParams expl effs resultTy body')
 
@@ -185,53 +183,85 @@ stripParens :: Group -> Group
 stripParens (WithSrc _ (CParens [g])) = stripParens g
 stripParens g = g
 
+-- === combinators for different sorts of binder lists ===
+
+aOptGivens :: Maybe GivenClause -> SyntaxM (Nest UReqAnnBinder VoidS VoidS)
+aOptGivens optGivens = fromMaybeM optGivens Empty aGivens
+
+binderList
+  :: [Group] -> (Group -> SyntaxM (Nest (UAnnBinder req) VoidS VoidS))
+  -> SyntaxM (Nest (UAnnBinder req) VoidS VoidS)
+binderList gs cont = concatNests <$> forM gs \case
+  WithSrc _ (CGivens gs') -> aGivens gs'
+  g -> cont g
+
+withTrailingConstraints
+  :: Group -> (Group -> SyntaxM ((UAnnBinder req) VoidS VoidS))
+  -> SyntaxM (Nest (UAnnBinder req) VoidS VoidS)
+withTrailingConstraints g cont = case g of
+  Binary Pipe lhs c -> do
+    bs@(Nest (UAnnBinder _ b _) _) <- withTrailingConstraints lhs cont
+    (ctx, s) <- case b of
+      UBindSource ctx s -> return (ctx, s)
+      UIgnore     -> throw SyntaxErr "Can't constrain anonymous binders"
+      UBind _ _ _ -> error "Shouldn't have internal names until renaming pass"
+    c' <- expr c
+    let v = WithSrcE ctx $ UVar (SourceName ctx s)
+    return $ bs >>> UnaryNest (fromReqAnnBinder $ asConstraintBinder  v c')
+  _ -> UnaryNest <$> cont g
+  where
+    asConstraintBinder :: UExpr VoidS -> UConstraint VoidS -> UReqAnnBinder VoidS VoidS
+    asConstraintBinder v c = do
+      let t = ns $ UApp c [v] []
+      UAnnBinder (Inferred Nothing (Synth Full)) UIgnore (UAnn t)
+
+defaultAnn :: UExpr VoidS -> UOptAnnBinder VoidS VoidS -> UReqAnnBinder VoidS VoidS
+defaultAnn dAnn (UAnnBinder expl b ann) = do
+  let ann' = case ann of
+        UNoAnn -> dAnn
+        UAnn t -> t
+  UAnnBinder expl b (UAnn ann')
+
+aGivens :: GivenClause -> SyntaxM (Nest (UAnnBinder req) VoidS VoidS)
+aGivens (implicits, optConstraints) = do
+  implicits' <- concatNests <$> forM implicits \b -> withTrailingConstraints b implicitArgBinder
+  constraints <- fromMaybeM optConstraints Empty (\gs -> toNest <$> mapM synthBinder gs)
+  return $ fmapNest fromReqAnnBinder $ implicits' >>> constraints
+
+synthBinder :: Group -> SyntaxM (UReqAnnBinder VoidS VoidS)
+synthBinder g = tyOptBinder (Inferred Nothing (Synth Full)) g
+
+fromReqAnnBinder :: UReqAnnBinder n l -> UAnnBinder req n l
+fromReqAnnBinder (UAnnBinder expl b ann) = do
+  let ann' = case ann of
+        UAnn t -> UAnn t
+  UAnnBinder expl b ann'
+
+concatNests :: [Nest b VoidS VoidS] -> Nest b VoidS VoidS
+concatNests [] = Empty
+concatNests (b:bs) = b >>> concatNests bs
+
+implicitArgBinder :: Group -> SyntaxM (UReqAnnBinder VoidS VoidS)
+implicitArgBinder g = do
+  UAnnBinder _ b ann <- defaultAnn (ns tyKind) <$> binderOptTy (Inferred Nothing Unify) g
+  s <- case b of
+    UBindSource _ s -> return $ Just s
+    _               -> return Nothing
+  return $ UAnnBinder (Inferred s Unify) b ann
+
 aExplicitParams :: ExplicitParams -> SyntaxM (Nest UReqAnnBinder VoidS VoidS)
-aExplicitParams gs = generalBinders DataParam Explicit gs
+aExplicitParams bs = binderList bs \b -> withTrailingConstraints b \b' ->
+  defaultAnn (ns tyKind) <$> binderOptTy Explicit b'
 
-aOptAnnExplicitParams :: ExplicitParams -> SyntaxM (Nest UOptAnnBinder VoidS VoidS)
-aOptAnnExplicitParams gs = undefined
+aPiBinders :: ExplicitParams -> SyntaxM (Nest UReqAnnBinder VoidS VoidS)
+aPiBinders bs = binderList bs \b ->
+  UnaryNest <$> tyOptBinder Explicit b
 
-aOptGivens :: Maybe GivenClause -> SyntaxM (Nest UReqAnnBinder VoidS VoidS)
-aOptGivens optGivens = undefined
--- aOptGivens optGivens = do
---   (expls, implicitParams) <- unzip <$> fromMaybeM optGivens [] aGivens
---   return (expls, toNest implicitParams)
-
-aGivens :: GivenClause -> SyntaxM [Nest UReqAnnBinder VoidS VoidS]
-aGivens (implicits, optConstraints) = undefined
--- aGivens (implicits, optConstraints) = do
---   implicits' <- mapM (generalBinder DataParam (Inferred Nothing Unify)) implicits
---   constraints <- fromMaybeM optConstraints [] \gs -> do
---     mapM (generalBinder TypeParam (Inferred Nothing (Synth Full))) gs
---   return $ implicits' <> constraints
-
-generalBinders
-  :: ParamStyle -> Explicitness -> [Group]
-  -> SyntaxM (Nest UReqAnnBinder VoidS VoidS)
-generalBinders paramStyle expl params = undefined
--- generalBinders paramStyle expl params = do
---   (expls, bs) <- unzip . concat <$> forM params \case
---     WithSrc _ (CGivens gs) -> aGivens gs
---     p -> (:[]) <$> generalBinder paramStyle expl p
---   return (expls, toNest bs)
-
-optAnnBinder :: Group -> SyntaxM (UOptAnnBinder VoidS VoidS)
-optAnnBinder = undefined
-
-generalBinder :: ParamStyle -> Explicitness -> Group
-              -> SyntaxM (UReqAnnBinder VoidS VoidS)
-generalBinder paramStyle expl g = undefined
--- generalBinder paramStyle expl g = case expl of
---   Inferred _ (Synth _) -> (expl,) <$> tyOptBinder g
---   Inferred _ Unify -> do
---     b <- binderOptTy g
---     expl' <- return case b of
---       UAnnBinder (UBindSource _ s) _ _ -> Inferred (Just s) Unify
---       _ -> expl
---     return (expl', b)
---   Explicit -> (expl,) <$> case paramStyle of
---     TypeParam -> tyOptBinder g
---     DataParam -> binderOptTy g
+explicitBindersOptAnn :: ExplicitParams -> SyntaxM (Nest UOptAnnBinder VoidS VoidS)
+explicitBindersOptAnn bs = binderList bs \b -> withTrailingConstraints b \b' ->
+  binderOptTy Explicit b'
+
+-- ===
 
 -- Binder pattern with an optional type annotation
 patOptAnn :: Group -> SyntaxM (UPat VoidS VoidS, Maybe (UType VoidS))
@@ -290,45 +320,33 @@ pat = propagateSrcB pat' where
       _ -> error "unexpected postfix group (should be ruled out at grouping stage)"
   pat' _ = throw SyntaxErr "Illegal pattern"
 
-data ParamStyle
- = TypeParam  -- binder optional, used in pi types
- | DataParam  -- type optional  , used in lambda
-
-tyOptBinder :: Group -> SyntaxM (UAnnBinder req VoidS VoidS)
-tyOptBinder = \case
+tyOptBinder :: Explicitness -> Group -> SyntaxM (UAnnBinder req VoidS VoidS)
+tyOptBinder expl = \case
   Binary Pipe  _ _     -> throw SyntaxErr "Unexpected constraint"
   Binary Colon name ty -> do
     b <- uBinder name
     ann <- UAnn <$> expr ty
-    return $ UAnnBinder Explicit b ann
+    return $ UAnnBinder expl b ann
   g -> do
     ty <- expr g
-    return $ UAnnBinder Explicit UIgnore (UAnn ty)
-
-binderOptTy :: Group -> SyntaxM (UOptAnnBinder VoidS VoidS)
-binderOptTy g = undefined
--- binderOptTy g = do
---   (g', constraints) <- trailingConstraints g
---   case g' of
---     Binary Colon name ty -> do
---       b <- uBinder name
---       ann <- UAnn <$> expr ty
---       return $ UAnnBinder b ann constraints
---     _ -> do
---       b <- uBinder g'
---       return $ UAnnBinder b UNoAnn constraints
-
-binderReqTy :: Group -> SyntaxM (UReqAnnBinder VoidS VoidS)
-binderReqTy = undefined
-
-trailingConstraints :: Group -> SyntaxM (Group, [UConstraint VoidS])
-trailingConstraints gTop = go [] gTop where
-  go :: [UConstraint VoidS] -> Group -> SyntaxM (Group, [UConstraint VoidS])
-  go cs = \case
-    Binary Pipe lhs c -> do
-      c' <- expr c
-      go (c':cs) lhs
-    g -> return (g, cs)
+    return $ UAnnBinder expl UIgnore (UAnn ty)
+
+binderOptTy :: Explicitness -> Group -> SyntaxM (UOptAnnBinder VoidS VoidS)
+binderOptTy expl = \case
+  Binary Colon name ty -> do
+    b <- uBinder name
+    ann <- UAnn <$> expr ty
+    return $ UAnnBinder expl b ann
+  g -> do
+    b <- uBinder g
+    return $ UAnnBinder expl b UNoAnn
+
+binderReqTy :: Explicitness -> Group -> SyntaxM (UReqAnnBinder VoidS VoidS)
+binderReqTy expl (Binary Colon name ty) = do
+  b <- uBinder name
+  ann <- UAnn <$> expr ty
+  return $ UAnnBinder expl b ann
+binderReqTy _ _ = throw SyntaxErr $ "Expected an annotated binder"
 
 argList :: [Group] -> SyntaxM ([UExpr VoidS], [UNamedArg VoidS])
 argList gs = partitionEithers <$> mapM singleArg gs
@@ -391,7 +409,7 @@ blockDecls [WithSrc src d] = addSrcContext src case d of
   CExpr g -> (Empty,) <$> expr g
   _ -> throw SyntaxErr "Block must end in expression"
 blockDecls (WithSrc pos (CBind b rhs):ds) = do
-  b' <- optAnnBinder b
+  b' <- binderOptTy Explicit b
   rhs' <- asExpr <$> block rhs
   body <- block $ IndentedBlock ds
   let lam = ULam $ ULamExpr (UnaryNest b') ExplicitApp Nothing Nothing body
@@ -425,7 +443,7 @@ expr = propagateSrcE expr' where
   expr' (CArrow lhs effs rhs) = do
     case lhs of
       WithSrc _ (CParens gs) -> do
-        bs <- generalBinders TypeParam Explicit gs
+        bs <- aPiBinders gs
         effs' <- fromMaybeM effs UPure aEffects
         resultTy <- expr rhs
         return $ UPi $ UPiExpr bs ExplicitApp effs' resultTy
@@ -465,7 +483,7 @@ expr = propagateSrcE expr' where
       Colon         -> throw SyntaxErr "Colon separates binders from their type annotations, is not a standalone operator.\nIf you are trying to write a dependent type, use parens: (i:Fin 4) => (..i)"
       ImplicitArrow -> case lhs of
         WithSrc _ (CParens gs) -> do
-          bs <- generalBinders TypeParam Explicit gs
+          bs <- aPiBinders gs
           resultTy <- expr rhs
           return $ UPi $ UPiExpr bs ImplicitApp UPure resultTy
         _ -> throw SyntaxErr "Argument types should be in parentheses"
@@ -505,7 +523,7 @@ expr = propagateSrcE expr' where
       range :: UExpr VoidS -> UExpr VoidS -> UExpr' VoidS
       range rangeName lim = explicitApp rangeName [ns UHole, lim]
   expr' (CLambda params body) = do
-    params' <- aOptAnnExplicitParams $ map stripParens params
+    params' <- explicitBindersOptAnn $ map stripParens params
     body' <- block body
     return $ ULam $ ULamExpr params' ExplicitApp Nothing Nothing body'
   expr' (CFor kind indices body) = do
@@ -515,7 +533,7 @@ expr = propagateSrcE expr' where
           KRof  -> (Rev, False)
           KRof_ -> (Rev, True)
     -- TODO: Can we fetch the source position from the error context, to feed into `buildFor`?
-    e <- buildFor (0, 0) dir <$> mapM binderOptTy indices <*> block body
+    e <- buildFor (0, 0) dir <$> mapM (binderOptTy Explicit) indices <*> block body
     if trailingUnit
       then return $ UDo $ ns $ UBlock (UnaryNest (nsB $ UExprDecl e)) (ns unitExpr)
       else return $ dropSrcE e
@@ -534,7 +552,7 @@ expr = propagateSrcE expr' where
     ty <- expr lhs
     case rhs of
       [b] -> do
-        b' <- binderReqTy b
+        b' <- binderReqTy Explicit b
         return $ UDepPairTy $ UDepPairType ImplicitDepPair b' ty
       _ -> error "n-ary dependent pairs not implemented"
 
@@ -544,6 +562,9 @@ charExpr c = ULit $ Word8Lit $ fromIntegral $ fromEnum c
 unitExpr :: UExpr' VoidS
 unitExpr = UPrim (UCon $ P.ProdCon) []
 
+tyKind :: UExpr' VoidS
+tyKind = UPrim (UPrimTC P.TypeKind) []
+
 -- === Builders ===
 
 -- TODO Does this generalize?  Swap list for Nest?

src/lib/CheapReduction.hs

@@ -309,6 +309,9 @@ instance (CheaplyReducibleE r e1 e1', CheaplyReducibleE r e2 e2')
     cheapReduceE (LeftE e) = LeftE <$> cheapReduceE e
     cheapReduceE (RightE e) = RightE <$> cheapReduceE e
 
+instance CheaplyReducibleE r e e' => CheaplyReducibleE r (ListE e) (ListE e') where
+  cheapReduceE (ListE xs) = ListE <$> mapM cheapReduceE xs
+
 -- XXX: TODO: figure out exactly what our normalization invariants are. We
 -- shouldn't have to choose `normalizeProj` or `asNaryProj` on a
 -- case-by-case basis. This is here for now because it makes it easier to switch

src/lib/ConcreteSyntax.hs

@@ -199,7 +199,6 @@ topDecl' =
   <|> interfaceDef
   <|> (CInstanceDecl <$> instanceDef True)
   <|> (CInstanceDecl <$> instanceDef False)
-  <|> effectDef
 
 proseBlock :: Parser SourceBlock'
 proseBlock = label "prose block" $ char '\'' >> fmap (Misc . ProseBlock . fst) (withSource consumeTillBreak)
@@ -291,26 +290,6 @@ interfaceDef = do
       return (methodName, ty)
   return $ CInterface className params methodDecls
 
-effectDef :: Parser CTopDecl'
-effectDef = do
-  keyWord EffectKW
-  effName <- anyName
-  sigs <- opSigList
-  return $ CEffectDecl (fromString effName) sigs
-
-opSigList :: Parser [(SourceName, UResumePolicy, Group)]
-opSigList = onePerLine do
-  policy <- resumePolicy
-  v <- anyName
-  void $ sym ":"
-  ty <- cGroup
-  return (fromString v, policy, ty)
-
-resumePolicy :: Parser UResumePolicy
-resumePolicy =  (keyWord JmpKW $> UNoResume)
-            <|> (keyWord DefKW $> ULinearResume)
-            <|> (keyWord CtlKW $> UAnyResume)
-
 nameAndType :: Parser (SourceName, Group)
 nameAndType = do
   n <- anyName
@@ -693,11 +672,11 @@ ops =
   , [symOpL   "@"]
   , [symOpN  "::"]
   , [symOpR   "$"]
-  , [symOpL   "|"]
   , [symOpN  "+=", symOpN  ":="]
   -- Associate right so the mistaken utterance foo : i:Fin 4 => (..i)
   -- groups as a bad pi type rather than a bad binder
   , [symOpR   ":"]
+  , [symOpL   "|"]
   , [symOpR  ",>"]
   , [symOpR  "&>"]
   , [withClausePostfix]