diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt index c078e44..b4cab63 100644 --- a/src/Lib/CompileExp.newt +++ b/src/Lib/CompileExp.newt @@ -263,16 +263,14 @@ compileDCon ix (QN _ nm) info arity = mkArgs k (quant :: args) = (quant, "h\{show k}") :: mkArgs (S k) args mkArgs k Nil = Nil - - -- probably want to drop the Ref2 when we can defToCExp : {{Ref2 Defs St}} → (QName × Def) -> M (QName × CExp) -defToCExp (qn, Axiom) = pure $ (qn, CErased) +defToCExp (qn, Axiom) = pure (qn, CErased) defToCExp (qn, (PrimOp _)) = (_,_ qn) <$> compilePop qn -defToCExp (qn, DCon ix info arity _) = pure $ (qn, compileDCon ix qn info arity) +defToCExp (qn, DCon ix info arity _) = pure (qn, compileDCon ix qn info arity) -- We're not using these are runtime at the moment, no typecase -- we need to sort out tag number if we do that -defToCExp (qn, TCon arity conNames) = pure $ (qn, compileDCon Z qn NormalCon (replicate' (cast arity) Many)) -defToCExp (qn, PrimTCon arity) = pure $ (qn, compileDCon Z qn NormalCon (replicate' (cast arity) Many)) -defToCExp (qn, PrimFn src _ deps) = pure $ (qn, CRaw src deps) +defToCExp (qn, TCon arity conNames) = pure (qn, compileDCon Z qn NormalCon (replicate' (cast arity) Many)) +defToCExp (qn, PrimTCon arity) = pure (qn, compileDCon Z qn NormalCon (replicate' (cast arity) Many)) +defToCExp (qn, PrimFn src _ deps) = pure (qn, CRaw src deps) defToCExp (qn, Fn tm) = (_,_ qn) <$> compileFun tm diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index e2d1bb1..6d65e38 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -1413,7 +1413,7 @@ updateRec ctx fc clauses arg ty = do | _ => error fc "\{show nm} not in scope" let (Just (MkEntry _ _ ty (DCon _ _ _ _) _)) = lookup conname top | _ => error fc "\{show conname} not a dcon" - pure $ (conname, collect arg ty) + pure (conname, collect arg ty) -- getTele Nothing (VPi _ _ _ _ a b) = getTele (Just $ RVar fc "$ru") a getTele Nothing v = error (getFC v) "Expected a pi type, got \{show v}" @@ -1544,7 +1544,7 @@ infer ctx (RVar fc nm) = go 0 ctx.types vty <- eval Nil ty pure (Ref fc name, vty) Nothing => error fc "\{show nm} not in scope" - go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd fc i, ty) + go i ((x, ty) :: xs) = if x == nm then pure (Bnd fc i, ty) else go (i + 1) xs infer ctx (RApp fc t u icit) = do @@ -1595,7 +1595,7 @@ infer ctx (RLet fc nm ty v sc) = do vv <- eval ctx.env v' let ctx' = define ctx nm vv vty (sc',scty) <- infer ctx' sc - pure $ (Let fc nm v' sc', scty) + pure (Let fc nm v' sc', scty) infer ctx (RAnn fc tm rty) = do ty <- check ctx rty (VU fc) @@ -1609,7 +1609,7 @@ infer ctx (RLam _ (BI fc nm icit quant) tm) = do (tm', b) <- infer ctx' tm debug $ \ _ => "make lam for \{show nm} scope \{rpprint (names ctx) tm'} : \{show b}" tyb <- quote (1 + ctx.lvl) b - pure $ (Lam fc nm icit quant tm', VPi fc nm icit quant a (MkClosure ctx.env tyb)) + pure (Lam fc nm icit quant tm', VPi fc nm icit quant a (MkClosure ctx.env tyb)) infer ctx (RImplicit fc) = do ty <- freshMeta ctx fc (VU emptyFC) Normal diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index 7fd7516..82cd7b7 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -66,7 +66,7 @@ logMetas (Unsolved fc k ctx ty kind cons :: rest) = do let (VRef _ tyname _) = ty | _ => pure Nil let cands = fromMaybe Nil $ lookupMap' tyname top.hints matches <- findMatches ctx ty cands - pure $ (" \{show $ length' matches} Solutions: \{show matches}" :: Nil) + pure (" \{show $ length' matches} Solutions: \{show matches}" :: Nil) _ => pure Nil info fc $ unlines ((msg :: Nil) ++ msgs ++ sols) diff --git a/src/Lib/TCO.newt b/src/Lib/TCO.newt index 26175ac..a72135f 100644 --- a/src/Lib/TCO.newt +++ b/src/Lib/TCO.newt @@ -84,7 +84,7 @@ doOptimize fns = do let conquant = map (const Many) conargs let arg = CConstr (S ix) (show qn) conargs conquant let body = CAppRef bouncer (CRef recName :: arg :: Nil) (Many :: Many :: Nil) - pure $ (qn, CFun args body) + pure (qn, CFun args body) mkWrap _ (qn, _) = error emptyFC "error in mkWrap: \{show qn} not a CFun" mkRecName : List QName → M QName diff --git a/src/Main.newt b/src/Main.newt index cd32e52..a48f0c3 100644 --- a/src/Main.newt +++ b/src/Main.newt @@ -252,7 +252,7 @@ cmdLine (fn :: args) = do let (True) = isSuffixOf ".newt" fn | _ => error emptyFC "Bad argument \{show fn}" (out, files) <- cmdLine args - pure $ (out, fn :: files) + pure (out, fn :: files) main' : M Unit main' = do