remove redundant $
This commit is contained in:
@@ -263,16 +263,14 @@ compileDCon ix (QN _ nm) info arity =
|
|||||||
mkArgs k (quant :: args) = (quant, "h\{show k}") :: mkArgs (S k) args
|
mkArgs k (quant :: args) = (quant, "h\{show k}") :: mkArgs (S k) args
|
||||||
mkArgs k Nil = Nil
|
mkArgs k Nil = Nil
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
-- probably want to drop the Ref2 when we can
|
-- probably want to drop the Ref2 when we can
|
||||||
defToCExp : {{Ref2 Defs St}} → (QName × Def) -> M (QName × CExp)
|
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, (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're not using these are runtime at the moment, no typecase
|
||||||
-- we need to sort out tag number if we do that
|
-- 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, 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, PrimTCon arity) = pure (qn, compileDCon Z qn NormalCon (replicate' (cast arity) Many))
|
||||||
defToCExp (qn, PrimFn src _ deps) = pure $ (qn, CRaw src deps)
|
defToCExp (qn, PrimFn src _ deps) = pure (qn, CRaw src deps)
|
||||||
defToCExp (qn, Fn tm) = (_,_ qn) <$> compileFun tm
|
defToCExp (qn, Fn tm) = (_,_ qn) <$> compileFun tm
|
||||||
|
|||||||
@@ -1413,7 +1413,7 @@ updateRec ctx fc clauses arg ty = do
|
|||||||
| _ => error fc "\{show nm} not in scope"
|
| _ => error fc "\{show nm} not in scope"
|
||||||
let (Just (MkEntry _ _ ty (DCon _ _ _ _) _)) = lookup conname top
|
let (Just (MkEntry _ _ ty (DCon _ _ _ _) _)) = lookup conname top
|
||||||
| _ => error fc "\{show conname} not a dcon"
|
| _ => 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 (VPi _ _ _ _ a b) = getTele (Just $ RVar fc "$ru") a
|
||||||
getTele Nothing v = error (getFC v) "Expected a pi type, got \{show v}"
|
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
|
vty <- eval Nil ty
|
||||||
pure (Ref fc name, vty)
|
pure (Ref fc name, vty)
|
||||||
Nothing => error fc "\{show nm} not in scope"
|
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
|
else go (i + 1) xs
|
||||||
|
|
||||||
infer ctx (RApp fc t u icit) = do
|
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'
|
vv <- eval ctx.env v'
|
||||||
let ctx' = define ctx nm vv vty
|
let ctx' = define ctx nm vv vty
|
||||||
(sc',scty) <- infer ctx' sc
|
(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
|
infer ctx (RAnn fc tm rty) = do
|
||||||
ty <- check ctx rty (VU fc)
|
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
|
(tm', b) <- infer ctx' tm
|
||||||
debug $ \ _ => "make lam for \{show nm} scope \{rpprint (names ctx) tm'} : \{show b}"
|
debug $ \ _ => "make lam for \{show nm} scope \{rpprint (names ctx) tm'} : \{show b}"
|
||||||
tyb <- quote (1 + ctx.lvl) 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
|
infer ctx (RImplicit fc) = do
|
||||||
ty <- freshMeta ctx fc (VU emptyFC) Normal
|
ty <- freshMeta ctx fc (VU emptyFC) Normal
|
||||||
|
|||||||
@@ -66,7 +66,7 @@ logMetas (Unsolved fc k ctx ty kind cons :: rest) = do
|
|||||||
let (VRef _ tyname _) = ty | _ => pure Nil
|
let (VRef _ tyname _) = ty | _ => pure Nil
|
||||||
let cands = fromMaybe Nil $ lookupMap' tyname top.hints
|
let cands = fromMaybe Nil $ lookupMap' tyname top.hints
|
||||||
matches <- findMatches ctx ty cands
|
matches <- findMatches ctx ty cands
|
||||||
pure $ (" \{show $ length' matches} Solutions: \{show matches}" :: Nil)
|
pure (" \{show $ length' matches} Solutions: \{show matches}" :: Nil)
|
||||||
|
|
||||||
_ => pure Nil
|
_ => pure Nil
|
||||||
info fc $ unlines ((msg :: Nil) ++ msgs ++ sols)
|
info fc $ unlines ((msg :: Nil) ++ msgs ++ sols)
|
||||||
|
|||||||
@@ -84,7 +84,7 @@ doOptimize fns = do
|
|||||||
let conquant = map (const Many) conargs
|
let conquant = map (const Many) conargs
|
||||||
let arg = CConstr (S ix) (show qn) conargs conquant
|
let arg = CConstr (S ix) (show qn) conargs conquant
|
||||||
let body = CAppRef bouncer (CRef recName :: arg :: Nil) (Many :: Many :: Nil)
|
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"
|
mkWrap _ (qn, _) = error emptyFC "error in mkWrap: \{show qn} not a CFun"
|
||||||
|
|
||||||
mkRecName : List QName → M QName
|
mkRecName : List QName → M QName
|
||||||
|
|||||||
@@ -252,7 +252,7 @@ cmdLine (fn :: args) = do
|
|||||||
let (True) = isSuffixOf ".newt" fn
|
let (True) = isSuffixOf ".newt" fn
|
||||||
| _ => error emptyFC "Bad argument \{show fn}"
|
| _ => error emptyFC "Bad argument \{show fn}"
|
||||||
(out, files) <- cmdLine args
|
(out, files) <- cmdLine args
|
||||||
pure $ (out, fn :: files)
|
pure (out, fn :: files)
|
||||||
|
|
||||||
main' : M Unit
|
main' : M Unit
|
||||||
main' = do
|
main' = do
|
||||||
|
|||||||
Reference in New Issue
Block a user