@@ -153,13 +153,18 @@ elab ist info pattern opts fn tm
154 local f = do e <- get_env
154 local f = do e <- get_env
155 return (f `elem` map fst e)
155 return (f `elem` map fst e)
157+ -- | Is a constant a type?
158+ constType :: Const -> Bool
157 constType (AType _) = True
159 constType (AType _) = True
158 constType StrType = True
160 constType StrType = True
159 constType PtrType = True
161 constType PtrType = True
160 constType VoidType = True
162 constType VoidType = True
161 constType _ = False
163 constType _ = False
165+ elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
166+ -> PTerm -- ^ The term to elaborate
163 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
168 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
164 elab' ina PType = do apply RType []; solve
169 elab' ina PType = do apply RType []; solve
165 elab' (_,_,inty) (PConstant c)
170 elab' (_,_,inty) (PConstant c)
@@ -607,6 +612,14 @@ elab ist info pattern opts fn tm
607 mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!
612 mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!
608 addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])
613 addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])
615+ -- | Elaborate the arguments to a function
616+ elabArgs :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
618+ -> FC -- ^ Source location
620+ -> [Name] -- ^ Names of arguments - these identify the holes to be filled
621+ -> [(Bool, PTerm)] -- ^ (Laziness, argument)
610 elabArgs ina failed fc retry [] _
623 elabArgs ina failed fc retry [] _
611-- | retry = let (ns, ts) = unzip (reverse failed) in
624-- | retry = let (ns, ts) = unzip (reverse failed) in
612-- elabArgs ina [] False ns ts
625-- elabArgs ina [] False ns ts