0 | module Idrall.Resolve

  2 | import Idrall.Error

  3 | import Idrall.Expr

  4 | import Idrall.IOEither

  5 | import Idrall.ParserNew

  6 | import Idrall.Path

  8 | import System

  9 | import System.File

 11 | parseWith : Maybe String -> String -> Either String (Expr ImportStatement, Int)

 12 | parseWith x = Idrall.ParserNew.parseExprNew {od = x}

 14 | parseErrorHandler : FC -> String -> Error

 15 | parseErrorHandler fc x = ParseError fc x

 17 | fileErrorHandler : FC -> String -> FileError -> Error

 18 | fileErrorHandler fc x y = ReadFileError fc (show y ++ " " ++ x)

 20 | readEnvVar : FC -> String -> IOEither Error String

 21 | readEnvVar fc x =

 22 |   MkIOEither $ do

 23 |     Just x' <- getEnv x | Nothing => pure $ Left $ EnvVarError fc $ "Env var \{x} not found"

 24 |     pure $ pure x'

 26 | nextCurrentPath : (current : Maybe Path) -> (next : Path) -> Path

 27 | nextCurrentPath (Just (Home xs)) (Relative ys) = Home (xs ++ ys)

 28 | nextCurrentPath (Just (Absolute xs)) (Relative ys) = Absolute (xs ++ ys)

 29 | nextCurrentPath (Just (Relative xs)) (Relative ys) = Relative (xs ++ ys)

 30 | nextCurrentPath _ p = p

 32 | combinePaths : Maybe FilePath -> FilePath -> FilePath

 33 | combinePaths Nothing y = y

 34 | combinePaths (Just (MkFilePath pathX fileNameX)) (MkFilePath pathY fileNameY) =

 35 |   let nextPath = nextCurrentPath (Just pathX) pathY

 36 |   in

 37 |   MkFilePath nextPath fileNameY

 39 | canonicalFilePath : FilePath -> String -- TODO finish properly

 40 | canonicalFilePath x = filePathForIO x

 42 | alreadyImported : FC -> List FilePath -> FilePath -> Either Error () -- TODO check is correct

 43 | alreadyImported fc xs x = case elem x xs of

 44 |                             False => pure ()

 45 |                             True => Left (CyclicImportError fc ((show x) ++ " in " ++ (show xs)))

 48 | readFile' : FC -> String -> IOEither Error String

 49 | readFile' fc filePath =

 50 |   let contents = MkIOEither (readFile filePath) in

 51 |       mapErr (fileErrorHandler fc filePath) contents

 53 | record LocalFile where

 54 |   constructor MkLocalFile

 55 |   filePath : FilePath

 56 |   contents : String

 58 | readLocalFile : FC -> (history : List FilePath) -> (current : Maybe FilePath) -> (next : FilePath) -> IOEither Error LocalFile

 59 | readLocalFile fc h current next = do

 60 |   let combinedFilePaths = combinePaths current next

 61 |   liftEither (alreadyImported fc h (normaliseFilePath combinedFilePaths))

 62 |   let fp = canonicalFilePath combinedFilePaths

 63 |   MkLocalFile combinedFilePaths <$> readFile' fc fp

 67 |   export

 68 |   covering

 69 |   resolve : (history : List FilePath)

 70 |           -> Maybe FilePath

 71 |           -> Expr ImportStatement

 72 |           -> IOEither Error (Expr Void)

 73 |   resolve h p (EVar fc x i) = pure (EVar fc x i)

 74 |   resolve h p (EConst fc x) = pure (EConst fc x)

 75 |   resolve h p (EPi fc x y z) = do

 76 |     y' <- resolve h p y

 77 |     z' <- resolve h p z

 78 |     pure (EPi fc x y' z')

 79 |   resolve h p (ELam fc x y z) = do

 80 |     y' <- resolve h p y

 81 |     z' <- resolve h p z

 82 |     pure (ELam fc x y' z')

 83 |   resolve h p (EApp fc x y) = do

 84 |     x' <- resolve h p x

 85 |     y' <- resolve h p y

 86 |     pure (EApp fc x' y')

 87 |   resolve h p (ELet fc x Nothing z w) = do

 88 |     z' <- resolve h p z

 89 |     w' <- resolve h p w

 90 |     pure (ELet fc x Nothing z' w')

 91 |   resolve h p (ELet fc x (Just y) z w) = do

 92 |     y' <- resolve h p y

 93 |     z' <- resolve h p z

 94 |     w' <- resolve h p w

 95 |     pure (ELet fc x (Just y') z' w')

 96 |   resolve h p (EAnnot fc x y) = do

 97 |     x' <- resolve h p x

 98 |     y' <- resolve h p y

 99 |     pure (EAnnot fc x' y')

100 |   resolve h p (EEquivalent fc x y) = do

101 |     x' <- resolve h p x

102 |     y' <- resolve h p y

103 |     pure (EEquivalent fc x' y')

104 |   resolve h p (EAssert fc x) = do

105 |     x' <- resolve h p x

106 |     pure (EAssert fc x')

107 |   resolve h p (EBool fc) = pure $ EBool fc

108 |   resolve h p (EBoolLit fc x) = pure (EBoolLit fc x)

109 |   resolve h p (EBoolAnd fc x y) = do

110 |     x' <- resolve h p x

111 |     y' <- resolve h p y

112 |     pure (EBoolAnd fc x' y')

113 |   resolve h p (EBoolOr fc x y) = do

114 |     x' <- resolve h p x

115 |     y' <- resolve h p y

116 |     pure (EBoolOr fc x' y')

117 |   resolve h p (EBoolEQ fc x y) = do

118 |     x' <- resolve h p x

119 |     y' <- resolve h p y

120 |     pure (EBoolEQ fc x' y')

121 |   resolve h p (EBoolNE fc x y) = do

122 |     x' <- resolve h p x

123 |     y' <- resolve h p y

124 |     pure (EBoolNE fc x' y')

125 |   resolve h p (EBoolIf fc x y z) = do

126 |     x' <- resolve h p x

127 |     y' <- resolve h p y

128 |     z' <- resolve h p z

129 |     pure (EBoolIf fc x' y' z')

130 |   resolve h p (ENatural fc) = pure $ ENatural fc

131 |   resolve h p (ENaturalLit fc k) = pure $ ENaturalLit fc k

132 |   resolve h p (ENaturalBuild fc) = pure $ ENaturalBuild fc

133 |   resolve h p (ENaturalFold fc) = pure $ ENaturalFold fc

134 |   resolve h p (ENaturalIsZero fc) = pure $ ENaturalIsZero fc

135 |   resolve h p (ENaturalEven fc) = pure $ ENaturalEven fc

136 |   resolve h p (ENaturalOdd fc) = pure $ ENaturalOdd fc

137 |   resolve h p (ENaturalSubtract fc) = pure $ ENaturalSubtract fc

138 |   resolve h p (ENaturalToInteger fc) = pure $ ENaturalToInteger fc

139 |   resolve h p (ENaturalShow fc) = pure $ ENaturalShow fc

140 |   resolve h p (ENaturalPlus fc x y) = do

141 |     x' <- resolve h p x

142 |     y' <- resolve h p y

143 |     pure (ENaturalPlus fc x' y')

144 |   resolve h p (ENaturalTimes fc x y) = do

145 |     x' <- resolve h p x

146 |     y' <- resolve h p y

147 |     pure (ENaturalTimes fc x' y')

148 |   resolve h p (EInteger fc) = pure $ EInteger fc

149 |   resolve h p (EIntegerLit fc k) = pure $ EIntegerLit fc k

150 |   resolve h p (EIntegerShow fc) = pure $ EIntegerShow fc

151 |   resolve h p (EIntegerClamp fc) = pure $ EIntegerClamp fc

152 |   resolve h p (EIntegerNegate fc) = pure $ EIntegerNegate fc

153 |   resolve h p (EIntegerToDouble fc) = pure $ EIntegerToDouble fc

154 |   resolve h p (EDouble fc) = pure $ EDouble fc

155 |   resolve h p (EDoubleLit fc k) = pure $ EDoubleLit fc k

156 |   resolve h p (EDoubleShow fc) = pure $ EDoubleShow fc

157 |   resolve h p (EList fc) = pure $ EList fc

158 |   resolve h p (EListLit fc Nothing xs) = do

159 |     xs' <- resolveList h p xs

160 |     pure (EListLit fc Nothing xs')

161 |   resolve h p (EListLit fc (Just x) xs) = do

162 |     x' <- resolve h p x

163 |     xs' <- resolveList h p xs

164 |     pure (EListLit fc (Just x') xs')

165 |   resolve h p (EListAppend fc x y) = do

166 |     x' <- resolve h p x

167 |     y' <- resolve h p y

168 |     pure (EListAppend fc x' y')

169 |   resolve h p (EListBuild fc) = pure $ EListBuild fc

170 |   resolve h p (EListFold fc) = pure $ EListFold fc

171 |   resolve h p (EListLength fc) = pure $ EListLength fc

172 |   resolve h p (EListHead fc) = pure $ EListHead fc

173 |   resolve h p (EListLast fc) = pure $ EListLast fc

174 |   resolve h p (EListIndexed fc) = pure $ EListIndexed fc

175 |   resolve h p (EListReverse fc) = pure $ EListReverse fc

176 |   resolve h p (EText fc) = pure $ EText fc

177 |   resolve h p (ETextLit fc (MkChunks xs x)) = do

178 |     xs' <- resolveChunks h p xs

179 |     pure (ETextLit fc (MkChunks xs' x))

180 |   resolve h p (ETextAppend fc x y) = do

181 |     x' <- resolve h p x

182 |     y' <- resolve h p y

183 |     pure (ETextAppend fc x' y')

184 |   resolve h p (ETextShow fc) = pure $ ETextShow fc

185 |   resolve h p (ETextReplace fc) = pure $ ETextReplace fc

186 |   resolve h p (EOptional fc) = pure $ EOptional fc

187 |   resolve h p (ENone fc) = pure $ ENone fc

188 |   resolve h p (ESome fc x) = do

189 |     x' <- resolve h p x

190 |     pure (ESome fc x')

191 |   resolve h p (ERecord fc x) =

192 |     let kv = toList x in do

193 |       kv' <- resolveRecord h p kv

194 |       pure (ERecord fc (fromList kv'))

195 |   resolve h p (ERecordLit fc x) =

196 |     let kv = toList x in do

197 |       kv' <- resolveRecord h p kv

198 |       pure (ERecordLit fc (fromList kv'))

199 |   resolve h p (ECombine fc x y) = do

200 |     x' <- resolve h p x

201 |     y' <- resolve h p y

202 |     pure (ECombine fc x' y')

203 |   resolve h p (ECombineTypes fc x y) = do

204 |     x' <- resolve h p x

205 |     y' <- resolve h p y

206 |     pure (ECombineTypes fc x' y')

207 |   resolve h p (EPrefer fc x y) = do

208 |     x' <- resolve h p x

209 |     y' <- resolve h p y

210 |     pure (EPrefer fc x' y')

211 |   resolve h p (ERecordCompletion fc x y) = do

212 |     x' <- resolve h p x

213 |     y' <- resolve h p y

214 |     pure (ERecordCompletion fc x' y')

215 |   resolve h p (EMerge fc x y Nothing) = do

216 |     x' <- resolve h p x

217 |     y' <- resolve h p y

218 |     pure (EMerge fc x' y' Nothing)

219 |   resolve h p (EMerge fc x y (Just z)) = do

220 |     x' <- resolve h p x

221 |     y' <- resolve h p y

222 |     z' <- resolve h p z

223 |     pure (EMerge fc x' y' (Just z'))

224 |   resolve h p (EUnion fc x) =

225 |     let kv = toList x in do

226 |       kv' <- resolveUnion h p kv

227 |       pure (EUnion fc (fromList kv'))

228 |   resolve h p (EToMap fc x Nothing) = do

229 |     x' <- resolve h p x

230 |     pure (EToMap fc x' Nothing)

231 |   resolve h p (EToMap fc x (Just y)) = do

232 |     x' <- resolve h p x

233 |     y' <- resolve h p y

234 |     pure (EToMap fc x' (Just y'))

235 |   resolve h p (EField fc x y) = do

236 |     pure (EField fc !(resolve h p x) y)

237 |   resolve h p (EProject fc x (Left y)) = do

238 |     x' <- resolve h p x

239 |     pure (EProject fc x' (Left y))

240 |   resolve h p (EProject fc x (Right y)) = do

241 |     x' <- resolve h p x

242 |     y' <- resolve h p y

243 |     pure (EProject fc x' (Right y'))

244 |   resolve h p (EWith fc x ks y) = do

245 |     x' <- resolve h p x

246 |     y' <- resolve h p y

247 |     pure (EWith fc x' ks y')

248 |   resolve h p (EImportAlt fc x y) =

249 |     case resolve h p x of

250 |          (MkIOEither x') => MkIOEither $ do

251 |            case !x' of

252 |                 (Right x'') => pure $ Right x''

253 |                 (Left w) => case resolve h p y of

254 |                                  (MkIOEither y'') => y''

255 |   resolve h p (EEmbed fc (Raw (LocalFile x))) = resolveLocalFile fc h p x

256 |   resolve h p (EEmbed fc (Raw (EnvVar x))) = resolveEnvVar fc h p x

257 |   resolve h p (EEmbed fc (Raw (Http x))) = MkIOEither (pure (Left (ErrorMessage fc "TODO http imports not implemented")))

258 |   resolve h p (EEmbed fc (Raw Missing)) = MkIOEither (pure (Left (ErrorMessage fc "No valid imports")))

259 |   resolve h p (EEmbed fc (Text a)) = resolveImportAsText fc h p a

260 |   resolve h p (EEmbed fc (Location a)) = MkIOEither (pure (Left (ErrorMessage fc "TODO as Location not implemented")))

261 |   resolve h p (EEmbed fc (Resolved x)) = MkIOEither (pure (Left (ErrorMessage fc "Already resolved")))

263 |   resolveImportAsText : FC -> (history : List FilePath) -> Maybe FilePath -> ImportStatement -> IOEither Error (Expr Void)

264 |   resolveImportAsText fc h p importStatement = do

265 |       str <- resolveImportToStr fc h p importStatement

266 |       pure $ ETextLit fc (MkChunks [] str)

267 |     where

268 |       resolveImportToStr : FC -> (history : List FilePath) -> Maybe FilePath -> ImportStatement -> IOEither Error String

269 |       resolveImportToStr fc h p (LocalFile fp) = contents <$> readLocalFile fc h p fp

270 |       resolveImportToStr fc h p (EnvVar str) = readEnvVar fc str

271 |       resolveImportToStr fc h p (Http str) = MkIOEither (pure (Left (ErrorMessage fc "TODO http imports not implemented")))

272 |       resolveImportToStr fc h p Missing = MkIOEither (pure (Left (ErrorMessage fc "No valid imports")))

274 |   resolveEnvVar : FC -> (history : List FilePath) -> Maybe FilePath -> String -> IOEither Error (Expr Void)

275 |   resolveEnvVar fc h p x = do

276 |     str <- readEnvVar fc x

277 |     expr <- mapErr (parseErrorHandler fc) (liftEither (parseWith Nothing str))

278 |     resolve h p (fst expr)

280 |   resolveLocalFile : FC -> (history : List FilePath) -> (current : Maybe FilePath) -> (next : FilePath) -> IOEither Error (Expr Void)

281 |   resolveLocalFile fc h current next = do

282 |     MkLocalFile filePath contents <- readLocalFile fc h current next

283 |     expr <- mapErr (parseErrorHandler fc) (liftEither (parseWith (Just $ canonicalFilePath filePath) contents))

284 |     resolve (normaliseFilePath filePath :: h) (Just filePath) (fst expr)

286 |   resolveRecord :  (history : List FilePath)

287 |                -> Maybe FilePath

288 |                -> List (FieldName, Expr ImportStatement)

289 |                -> IOEither Error (List (FieldName, Expr Void))

290 |   resolveRecord h p [] =  MkIOEither (pure (Right []))

291 |   resolveRecord h p ((k, v) :: xs) = do

292 |     rest <- resolveRecord h p xs

293 |     MkIOEither (pure (Right ((k, !(resolve h p v)) :: rest)))

295 |   resolveUnion :  (history : List FilePath) -- TODO try use traverse instead?

296 |                -> Maybe FilePath

297 |                -> List (FieldName, Maybe (Expr ImportStatement))

298 |                -> IOEither Error (List (FieldName, Maybe (Expr Void)))

299 |   resolveUnion h p [] = MkIOEither (pure (Right []))

300 |   resolveUnion h p ((k,v) :: xs) = do

301 |     rest <- resolveUnion h p xs

302 |     case v of

303 |          Nothing => MkIOEither (pure (Right ((k, Nothing) :: rest)))

304 |          (Just x) => MkIOEither (pure (Right ((k, Just (!(resolve h p x))) :: rest)))

306 |   resolveList :  (history : List FilePath)

307 |               -> Maybe FilePath

308 |               -> List (Expr ImportStatement)

309 |               -> IOEither Error (List (Expr Void))

310 |   resolveList h p [] = MkIOEither (pure (Right []))

311 |   resolveList h p (x :: xs) =

312 |     do rest <- resolveList h p xs

313 |        x' <- resolve h p x

314 |        MkIOEither (pure (Right (x' :: rest)))

316 |   resolveChunks :  (history : List FilePath)

317 |                 -> Maybe FilePath

318 |                 -> List (String, Expr ImportStatement)

319 |                 -> IOEither Error (List (String, Expr Void))

320 |   resolveChunks h p [] = MkIOEither $ pure (Right [])

321 |   resolveChunks h p ((a, x) :: xs) = do

322 |     rest <- resolveChunks h p xs

323 |     x' <- resolve h p x

324 |     MkIOEither (pure (Right ((a, x') :: rest)))