0 | module Idrall.Expr

  2 | import Data.List1

  4 | import Idrall.Path

  5 | import public Idrall.FC

  7 | import public Data.SortedMap

  9 | public export

 10 | Name : Type

 11 | Name = String

 13 | public export

 14 | data FieldName = MkFieldName String

 16 | public export

 17 | Show FieldName where

 18 |   show (MkFieldName x) = "(MkFieldName " ++ show x ++ ")"

 20 | public export

 21 | prettyFieldName : FieldName -> String

 22 | prettyFieldName (MkFieldName x) = x

 24 | public export

 25 | Eq FieldName where

 26 |   (==) (MkFieldName x) (MkFieldName y) = x == y

 28 | public export

 29 | Ord FieldName where

 30 |   compare (MkFieldName x) (MkFieldName y) = compare x y

 32 | public export

 33 | Namespace : Type

 34 | Namespace = List (Name, Integer)

 35 | %name Namespace ns1, ns2, ns3

 37 | public export

 38 | data U = CType | Sort | Kind

 41 | Eq U where

 42 |   (==) CType CType = True

 43 |   (==) Sort Sort = True

 44 |   (==) Kind Kind = True

 45 |   (==) _ _ = False

 48 | Show U where

 49 |   show CType = "CType"

 50 |   show Sort = "Sort"

 51 |   show Kind = "Kind"

 55 |   public export

 56 |   data ImportStatement

 57 |     = LocalFile FilePath

 58 |     | EnvVar String

 59 |     | Http String

 60 |     | Missing

 62 |   public export

 63 |   data Import a

 64 |     = Raw a

 65 |     | Text a

 66 |     | Location a

 67 |     | Resolved (Expr Void)

 69 |   public export

 70 |   data Chunks a = MkChunks (List (String, Expr a)) String

 72 |   public export

 73 |   data Expr a

 74 |     -- x

 75 |     = EConst FC U

 76 |     | EVar FC Name Int

 77 |     -- | ELam x A b ~ λ(x : A) -> b

 78 |     | ELam FC Name (Expr a) (Expr a)

 79 |     -- | EPi x A b ~ forall(x : A) -> b

 80 |     | EPi FC Name (Expr a) (Expr a)

 81 |     -- | > EApp f a ~ f a

 82 |     | EApp FC (Expr a) (Expr a)

 83 |     -- | > ELet x Nothing r e ~ let x = r in e

 84 |     --   > ELet x (Just t) r e ~ let x : t = r in e

 85 |     | ELet FC Name (Maybe (Expr a)) (Expr a) (Expr a)

 86 |     -- | > EAnnot x t ~ x : t

 87 |     | EAnnot FC (Expr a) (Expr a)

 88 |     -- | > EBool ~ Bool

 89 |     | EBool FC

 90 |     -- | > EBoolLit b ~ b

 91 |     | EBoolLit FC Bool

 92 |     -- | > EBoolAnd x y ~ x && y

 93 |     | EBoolAnd FC (Expr a) (Expr a)

 94 |     -- | > EBoolOr  x y ~  x || y

 95 |     | EBoolOr FC (Expr a) (Expr a)

 96 |     -- | > EBoolEQ  x y ~  x == y

 97 |     | EBoolEQ FC (Expr a) (Expr a)

 98 |     -- | > EBoolNE  x y ~  x != y

 99 |     | EBoolNE FC (Expr a) (Expr a)

100 |     -- | > EBoolIf x y z ~ if x then y else z

101 |     | EBoolIf FC (Expr a) (Expr a) (Expr a)

102 |     -- | > ENatural ~ Natural

103 |     | ENatural FC

104 |     -- | > ENaturalLit n ~ n

105 |     | ENaturalLit FC Nat

106 |     -- | > ENaturalFold ~ Natural/fold

107 |     | ENaturalFold FC

108 |     -- | > ENaturalBuild ~ Natural/build

109 |     | ENaturalBuild FC

110 |     -- | > ENaturalIsZero ~ Natural/isZero

111 |     | ENaturalIsZero FC

112 |     -- | > ENaturalEven ~  Natural/even

113 |     | ENaturalEven FC

114 |     -- | > ENaturalOdd ~  Natural/odd

115 |     | ENaturalOdd FC

116 |     -- | > ENaturalToInteger ~  Natural/toInteger

117 |     | ENaturalToInteger FC

118 |     -- | > ENaturalSubtract ~  Natural/subtract

119 |     | ENaturalSubtract FC

120 |     -- | > ENaturalShow ~  Natural/show

121 |     | ENaturalShow FC

122 |      -- | > ENaturalPlus x y ~  x + y

123 |     | ENaturalPlus FC (Expr a) (Expr a)

124 |     -- | > ENaturalTimes x y ~  x * y

125 |     | ENaturalTimes FC (Expr a) (Expr a)

126 |     -- | > EInteger ~ Integer

127 |     | EInteger FC

128 |     -- | > EIntegerLit i ~ i

129 |     | EIntegerLit FC Integer

130 |     -- | > EIntegerShow ~  Integer/show

131 |     | EIntegerShow FC

132 |     -- | > EIntegerClamp ~ Integer/clamp

133 |     | EIntegerClamp FC

134 |     -- | > EIntegerNegate ~ EIntegerNegate

135 |     | EIntegerNegate FC

136 |     -- | > EIntegerToDouble ~ EIntegerToDouble

137 |     | EIntegerToDouble FC

138 |     -- | > EDouble ~ Double

139 |     | EDouble FC

140 |     -- | > EDoubleLit n ~ n

141 |     | EDoubleLit FC Double

142 |     -- | > EDoubleShow ~  Double/show

143 |     | EDoubleShow FC

144 |     -- | > EText ~ Text

145 |     | EText FC

146 |     -- | > ETextLit (Chunks [(t1, e1), (t2, e2)] t3) ~  "t1${e1}t2${e2}t3"

147 |     | ETextLit FC (Chunks a)

148 |     -- | > ETextAppend x y ~ x ++ y

149 |     | ETextAppend FC (Expr a) (Expr a)

150 |     -- | > ETextShow ~ Text/show

151 |     | ETextShow FC

152 |     -- | > ETextReplace ~ Text/replace

153 |     | ETextReplace FC

154 |     -- | > EList a ~ List a

155 |     | EList FC

156 |     -- | > EList (Some e) [e', ...] ~ [] : List a

157 |     | EListLit FC (Maybe (Expr a)) (List (Expr a))

158 |     -- | > EListAppend x y ~ x # y

159 |     | EListAppend FC (Expr a) (Expr a)

160 |     -- | > EListBuild ~ List/build

161 |     | EListBuild FC

162 |     -- | > EListFold ~ List/fold

163 |     | EListFold FC

164 |     -- | > EListLength ~ List/length

165 |     | EListLength FC

166 |     -- | > EListHead ~ List/head

167 |     | EListHead FC

168 |     -- | > EListLast ~ List/last

169 |     | EListLast FC

170 |     -- | > EListIndexed ~ List/indexed

171 |     | EListIndexed FC

172 |     -- | > EListReverse ~ List/reverse

173 |     | EListReverse FC

174 |     -- | > EOptional ~ Optional

175 |     | EOptional FC

176 |     -- | > ESome x ~ Some a

177 |     | ESome FC (Expr a)

178 |     -- | > ENone ~ None

179 |     | ENone FC

180 |     -- | > EEquivalent x y ~ x === y

181 |     | EEquivalent FC (Expr a) (Expr a)

182 |     -- | > EAssert x ~ assert : e

183 |     | EAssert FC (Expr a)

184 |     -- | > ERecord (fromList ((MkFieldName "Foo"), EBool)) ~ { Foo : Bool }

185 |     | ERecord FC (SortedMap FieldName (Expr a))

186 |     -- | > ERecordLit (fromList ((MkFieldName "Foo"), EBool)) ~ { Foo = Bool }

187 |     | ERecordLit FC (SortedMap FieldName (Expr a))

188 |     -- | > EUnion (fromList ((MkFieldName "Foo"), Nothing)) ~ < Foo >

189 |     -- | > EUnion (fromList ((MkFieldName "Foo"), Just EBool)) ~ < Foo : Bool >

190 |     | EUnion FC (SortedMap FieldName (Maybe (Expr a)))

191 |     -- | > ECombine x y ~ x /\ y

192 |     | ECombine FC (Expr a) (Expr a)

193 |     -- | > ECombineTypes x y ~ x //\\ y

194 |     | ECombineTypes FC (Expr a) (Expr a)

195 |     -- | > EPrefer x y ~  x ⫽ y

196 |     | EPrefer FC (Expr a) (Expr a)

197 |     -- | > ERecordCompletion x y ~  x::y

198 |     | ERecordCompletion FC (Expr a) (Expr a)

199 |     -- | > EMerge x y (Just t ) ~  merge x y : t

200 |     --   > EMerge x y  Nothing  ~  merge x y

201 |     | EMerge FC (Expr a) (Expr a) (Maybe (Expr a))

202 |     -- | > EToMap x (Just t) ~  toMap x : t

203 |     --   > EToMap x Nothing ~  toMap x

204 |     | EToMap FC (Expr a) (Maybe (Expr a))

205 |     -- | > EField (EVar "x" 0) (MkFieldName "Foo") ~ x.Foo

206 |     | EField FC (Expr a) FieldName

207 |     -- | > EProject e (Left xs) ~ e.{ xs }

208 |     --   > EProject e (Right t) ~ e.(t)

209 |     | EProject FC (Expr a) (Either (List FieldName) (Expr a))

210 |     -- | > EWith x y e ~  x with y = e

211 |     | EWith FC (Expr a) (List1 FieldName) (Expr a)

212 |     -- | > EImportAlt x y ~ x ? y

213 |     | EImportAlt FC (Expr a) (Expr a)

214 |     | EEmbed FC (Import a)

216 | public export

217 | HasFC (Expr a) where

218 |   getFC (EConst fc x) = fc

219 |   getFC (EVar fc x y) = fc

220 |   getFC (ELam fc x y z) = fc

221 |   getFC (EPi fc x y z) = fc

222 |   getFC (EApp fc x y) = fc

223 |   getFC (ELet fc x y z w) = fc

224 |   getFC (EAnnot fc x y) = fc

225 |   getFC (EBool fc) = fc

226 |   getFC (EBoolLit fc x) = fc

227 |   getFC (EBoolAnd fc x y) = fc

228 |   getFC (EBoolOr fc x y) = fc

229 |   getFC (EBoolEQ fc x y) = fc

230 |   getFC (EBoolNE fc x y) = fc

231 |   getFC (EBoolIf fc x y z) = fc

232 |   getFC (ENatural fc) = fc

233 |   getFC (ENaturalLit fc k) = fc

234 |   getFC (ENaturalFold fc) = fc

235 |   getFC (ENaturalBuild fc) = fc

236 |   getFC (ENaturalIsZero fc) = fc

237 |   getFC (ENaturalEven fc) = fc

238 |   getFC (ENaturalOdd fc) = fc

239 |   getFC (ENaturalToInteger fc) = fc

240 |   getFC (ENaturalSubtract fc) = fc

241 |   getFC (ENaturalShow fc) = fc

242 |   getFC (ENaturalPlus fc x y) = fc

243 |   getFC (ENaturalTimes fc x y) = fc

244 |   getFC (EInteger fc) = fc

245 |   getFC (EIntegerLit fc x) = fc

246 |   getFC (EIntegerShow fc) = fc

247 |   getFC (EIntegerClamp fc) = fc

248 |   getFC (EIntegerNegate fc) = fc

249 |   getFC (EIntegerToDouble fc) = fc

250 |   getFC (EDouble fc) = fc

251 |   getFC (EDoubleLit fc x) = fc

252 |   getFC (EDoubleShow fc) = fc

253 |   getFC (EText fc) = fc

254 |   getFC (ETextLit fc x) = fc

255 |   getFC (ETextAppend fc x y) = fc

256 |   getFC (ETextShow fc) = fc

257 |   getFC (ETextReplace fc) = fc

258 |   getFC (EList fc) = fc

259 |   getFC (EListLit fc x xs) = fc

260 |   getFC (EListAppend fc x y) = fc

261 |   getFC (EListBuild fc) = fc

262 |   getFC (EListFold fc) = fc

263 |   getFC (EListLength fc) = fc

264 |   getFC (EListHead fc) = fc

265 |   getFC (EListLast fc) = fc

266 |   getFC (EListIndexed fc) = fc

267 |   getFC (EListReverse fc) = fc

268 |   getFC (EOptional fc) = fc

269 |   getFC (ESome fc x) = fc

270 |   getFC (ENone fc) = fc

271 |   getFC (EEquivalent fc x y) = fc

272 |   getFC (EAssert fc x) = fc

273 |   getFC (ERecord fc x) = fc

274 |   getFC (ERecordLit fc x) = fc

275 |   getFC (EUnion fc x) = fc

276 |   getFC (ECombine fc x y) = fc

277 |   getFC (ECombineTypes fc x y) = fc

278 |   getFC (EPrefer fc x y) = fc

279 |   getFC (ERecordCompletion fc x y) = fc

280 |   getFC (EMerge fc x y z) = fc

281 |   getFC (EToMap fc x y) = fc

282 |   getFC (EField fc x y) = fc

283 |   getFC (EProject fc x y) = fc

284 |   getFC (EWith fc x xs y) = fc

285 |   getFC (EImportAlt fc x y) = fc

286 |   getFC (EEmbed fc x) = fc

289 | Show ImportStatement where

290 |   show (LocalFile x) = "(LocalFile " ++ show x ++ ")"

291 |   show (EnvVar x) = "(EnvVar " ++ x ++ ")"

292 |   show (Http x) = "(Http " ++ x ++ ")"

293 |   show Missing = "Missing"

296 | Show (Import ImportStatement) where

297 |   show (Raw x) = "(Raw \{show x}"

298 |   show (Text x) = "(Text \{show x}"

299 |   show (Location x) = "(Location \{show x}"

300 |   show (Resolved x) = "(Resolved x)"

303 |   export covering

304 |   Show (Import a) where

305 |     show (Raw x) = "(Raw)" -- TODO show x

306 |     show (Text x) = "(Text)" -- TODO show x

307 |     show (Location x) = "(Location)" -- TODO show x

308 |     show (Resolved x) = "(Resolved " ++ show x ++ ")"

310 |   export covering

311 |   Show (Expr a) where

312 |     show (EConst fc x) = "(EConst " ++ show x ++ ")"

313 |     show (EVar fc x i) = "(EVar " ++ show x ++ " " ++ show i ++ ")"

314 |     show (ELam fc x y z) = "(ELam " ++ x ++ " " ++ show y ++ " " ++ show z ++ ")"

315 |     show (EPi fc x y z) = "(EPi " ++ x ++ " " ++ show y ++ " " ++ show z ++ ")"

316 |     show (EApp fc x y) = "(EApp " ++ show x ++ " " ++ show y ++ ")"

317 |     show (ELet fc x y z w) = "(ELet " ++ show x ++ " " ++ show y ++ " " ++ show z ++ " " ++ show w ++ ")"

318 |     show (EAnnot fc x y) = "(EAnnot " ++ show x ++ " " ++ show y ++ ")"

319 |     show (EBool fc) = "EBool"

320 |     show (EBoolLit fc False) = "(EBoolLit False)"

321 |     show (EBoolLit fc True) = "(EBoolLit True)"

322 |     show (EBoolAnd fc x y) = "(EBoolAnd " ++ show x ++ " " ++ show y ++ ")"

323 |     show (EBoolOr fc x y) = "(EBoolOr " ++ show x ++ " " ++ show y ++ ")"

324 |     show (EBoolEQ fc x y) = "(EBoolEQ " ++ show x ++ " " ++ show y ++ ")"

325 |     show (EBoolNE fc x y) = "(EBoolNE " ++ show x ++ " " ++ show y ++ ")"

326 |     show (EBoolIf fc x y z) = "(EBoolIf " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"

327 |     show (ENatural fc) = "ENatural"

328 |     show (ENaturalLit fc k) = "(ENaturalLit " ++ show k ++ ")"

329 |     show (ENaturalFold fc) = "ENaturalFold"

330 |     show (ENaturalBuild fc) = "ENaturalBuild"

331 |     show (ENaturalIsZero fc) = "ENaturalIsZero"

332 |     show (ENaturalEven fc) = "ENaturalEven"

333 |     show (ENaturalOdd fc) = "ENaturalOdd"

334 |     show (ENaturalToInteger fc) = "ENaturalToInteger"

335 |     show (ENaturalSubtract fc) = "ENaturalSubtract"

336 |     show (ENaturalShow fc) = "NaturalShow"

337 |     show (ENaturalPlus fc x y) = "(ENaturalPlus " ++ show x ++ " " ++ show y ++ ")"

338 |     show (ENaturalTimes fc x y) = "(ENaturalTimes " ++ show x ++ " " ++ show y ++ ")"

339 |     show (EInteger fc) = "EInteger"

340 |     show (EIntegerLit fc x) = "(EIntegerLit " ++ show x ++ ")"

341 |     show (EIntegerClamp fc) = "EIntegerClamp"

342 |     show (EIntegerShow fc) = "EIntegerShow"

343 |     show (EIntegerNegate fc) = "EIntegerNegate"

344 |     show (EIntegerToDouble fc) = "EIntegerToDouble"

345 |     show (EDouble fc) = "EDouble"

346 |     show (EDoubleLit fc k) = "(EDoubleLit " ++ show k ++ ")"

347 |     show (EDoubleShow fc) = "EDoubleShow"

348 |     show (EText fc) = "EText"

349 |     show (ETextLit fc x) = "(ETextLit " ++ show x ++ ")"

350 |     show (ETextAppend fc x y) = "(ETextAppend " ++ show x ++ " " ++ show y ++ ")"

351 |     show (ETextShow fc) = "ETextShow"

352 |     show (ETextReplace fc) = "ETextReplace"

353 |     show (EList fc) = "EList"

354 |     show (EListLit fc Nothing xs) = "(EListLit Nothing " ++ show xs ++ ")"

355 |     show (EListLit fc (Just x) xs) = "(EListLit (Just " ++ show x ++ ") " ++ show xs ++ ")"

356 |     show (EListAppend fc x y) = "(EListAppend " ++ show x ++ " " ++ show y ++ ")"

357 |     show (EListBuild fc) = "EListBuild"

358 |     show (EListFold fc) = "EListFold"

359 |     show (EListHead fc) = "EListHead"

360 |     show (EListLength fc) = "EListLength"

361 |     show (EListLast fc) = "EListLast"

362 |     show (EListIndexed fc) = "EListIndexed"

363 |     show (EListReverse fc) = "EListReverse"

364 |     show (EOptional fc) = "EOptional"

365 |     show (ENone fc) = "ENone"

366 |     show (ESome fc x) = "(ESome " ++ show x ++ ")"

367 |     show (EEquivalent fc x y) = "(EEquivalent " ++ show x ++ " " ++ show y ++ ")"

368 |     show (EAssert fc x) = "(EAssert " ++ show x ++ ")"

369 |     show (ERecord fc x) = "(ERecord " ++ show x ++ ")"

370 |     show (ERecordLit fc x) = "(ERecordLit " ++ show x ++ ")"

371 |     show (EUnion fc x) = "(EUnion $ " ++ show x ++ ")"

372 |     show (ECombine fc x y) = "(ECombine " ++ show x ++ " " ++ show y ++ ")"

373 |     show (ECombineTypes fc x y) = "(ECombineTypes " ++ show x ++ " " ++ show y ++ ")"

374 |     show (EPrefer fc x y) = "(EPrefer " ++ show x ++ " " ++ show y ++ ")"

375 |     show (ERecordCompletion fc x y) = "(ERecordCompletion " ++ show x ++ " " ++ show y ++ ")"

376 |     show (EMerge fc x y z) = "(EMerge " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"

377 |     show (EToMap fc x y) = "(EToMap " ++ show x ++ " " ++ show y ++ ")"

378 |     show (EField fc x y) = "(EField " ++ show x ++ " " ++ show y ++ ")"

379 |     show (EProject fc x y) = "(EProject " ++ show x ++ " " ++ show y ++ ")"

380 |     show (EWith fc x ks y) = "(EWith " ++ show x ++ " " ++ show ks ++ " " ++ show y ++ ")"

381 |     show (EImportAlt fc x y) = "(EImportAlt " ++ show x ++ " " ++ show y ++ ")"

382 |     show (EEmbed fc x) = "(EEmbed " ++ show x ++ ")"

384 |   public export covering

385 |   Show (Chunks a) where

386 |     show (MkChunks xs x) = "MkChunks " ++ (show xs) ++ " " ++ show x

388 |   -- TODO add Traversible for Expr a

390 | public export

391 | Semigroup (Chunks a) where

392 |   (<+>) (MkChunks xysL zL) (MkChunks [] zR) = MkChunks xysL (zL <+> zR)

393 |   (<+>) (MkChunks xysL zL) (MkChunks ((x, y) :: xysR) zR) =

394 |     MkChunks (xysL ++ (zL <+> x, y)::xysR) zR

396 | public export

397 | Monoid (Chunks a) where

398 |   neutral = MkChunks [] neutral