Skip to content

Commit ec1e816

Browse files
hyperpolymathhyperpolymath
authored
Merge branch 'main' into proof-debt/standards-134-coq-preservation-admit
2 parents e1a877a + 69a0d29 commit ec1e816

3 files changed

Lines changed: 73 additions & 63 deletions

File tree

‎idris2/src/Ephapax/IR/AST.idr‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
module Ephapax.IR.AST
22

3-
%default partial
3+
%default total
44

55
public export
66
data Linearity = Linear | Unrestricted

‎idris2/src/Ephapax/IR/Decode.idr‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ import Data.String
55
import Ephapax.IR.SExpr
66
import Ephapax.IR.AST
77

8-
%default partial
8+
%default total
99

1010
baseToAtom : BaseTy -> String
1111
baseToAtom Unit = "unit"
@@ -154,6 +154,7 @@ decodeTy (List [Atom "borrow", inner]) = pure (Borrow !(decodeTy inner))
154154
decodeTy (List [Atom "var", Atom v]) = pure (Var v)
155155
decodeTy _ = Left (Invalid "unknown type")
156156

157+
covering
157158
encodeExpr : Expr -> SExpr
158159
encodeExpr (Lit lit) = List [Atom "lit", encodeLit lit]
159160
encodeExpr (VarE name) = List [Atom "var", Atom name]
@@ -181,6 +182,7 @@ encodeExpr (Block es) = List (Atom "block" :: map encodeExpr es)
181182
encodeExpr (BinOpE op a b) = List [Atom "binop", Atom (binopToAtom op), encodeExpr a, encodeExpr b]
182183
encodeExpr (UnOpE op e) = List [Atom "unop", Atom (unaryToAtom op), encodeExpr e]
183184

185+
covering
184186
decodeExpr : SExpr -> Either ParseError Expr
185187
decodeExpr (List (Atom tag :: rest)) =
186188
case tag of
@@ -273,12 +275,14 @@ decodeParam (List [Atom name, ty]) = do
273275
pure (name, t)
274276
decodeParam _ = Left (Invalid "param must be (name ty)")
275277

278+
covering
276279
encodeDecl : Decl -> SExpr
277280
encodeDecl (Fn name params ret body) =
278281
List [Atom "fn", Atom name, List (map encodeParam params), encodeTy ret, encodeExpr body]
279282
encodeDecl (TypeDecl name ty) =
280283
List [Atom "type", Atom name, encodeTy ty]
281284

285+
covering
282286
decodeDecl : SExpr -> Either ParseError Decl
283287
decodeDecl (List (Atom "fn" :: Atom name :: List params :: ret :: body :: [])) = do
284288
ps <- traverse decodeParam params
@@ -291,17 +295,20 @@ decodeDecl (List (Atom "type" :: Atom name :: ty :: [])) = do
291295
decodeDecl _ = Left (Invalid "unknown decl")
292296

293297
public export
298+
covering
294299
fromSExpr : SExpr -> Either ParseError Module
295300
fromSExpr (List (Atom "module" :: Atom name :: List decls :: [])) = do
296301
ds <- traverse decodeDecl decls
297302
pure (MkModule name ds)
298303
fromSExpr _ = Left (Invalid "expected (module name (decls...))")
299304

300305
public export
306+
covering
301307
toSExpr : Module -> SExpr
302308
toSExpr (MkModule name decls) =
303309
List [Atom "module", Atom name, List (map encodeDecl decls)]
304310

305311
public export
312+
covering
306313
encode : Module -> String
307314
encode = show . toSExpr

‎idris2/src/Ephapax/Parse/Lexer.idr‎

Lines changed: 64 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ module Ephapax.Parse.Lexer
22

33
import Data.List
44

5-
%default partial
5+
%default total
66

77
public export
88
record Pos where
@@ -128,7 +128,9 @@ Show LexError where
128128

129129
public export
130130
lex : String -> Either LexError (List Token)
131-
lex input = go (MkPos 1 1) (unpack input) []
131+
lex input =
132+
let cs = unpack input in
133+
go (length cs) (MkPos 1 1) cs []
132134
where
133135
isSpaceChar : Char -> Bool
134136
isSpaceChar ch = ch == ' ' || ch == '\t' || ch == '\r'
@@ -176,176 +178,177 @@ lex input = go (MkPos 1 1) (unpack input) []
176178
goStr pos' (unescape c :: acc) rest
177179
goStr pos acc (c :: rest) = goStr (advance pos c) (c :: acc) rest
178180

179-
go : Pos -> List Char -> List Token -> Either LexError (List Token)
180-
go _ [] acc = Right (reverse acc)
181-
go pos ('-' :: '-' :: rest) acc =
181+
go : Nat -> Pos -> List Char -> List Token -> Either LexError (List Token)
182+
go Z _ _ acc = Right (reverse acc)
183+
go (S k) _ [] acc = Right (reverse acc)
184+
go (S k) pos ('-' :: '-' :: rest) acc =
182185
let (skipped, more) = span (/= '\n') rest in
183186
let (consumed, tail) = case more of
184187
'\n' :: tail' => (skipped ++ ['\n'], tail')
185188
_ => (skipped, more)
186-
in go (advanceN pos ('-' :: '-' :: consumed)) tail acc
187-
go pos (c :: rest) acc =
188-
if isSpaceChar c then go (advance pos c) rest acc
189+
in go k (advanceN pos ('-' :: '-' :: consumed)) tail acc
190+
go (S k) pos (c :: rest) acc =
191+
if isSpaceChar c then go k (advance pos c) rest acc
189192
else if c == '\n' then
190193
let nextPos = advance pos c in
191-
go nextPos rest (MkToken TkSemi pos :: acc)
194+
go k nextPos rest (MkToken TkSemi pos :: acc)
192195
else if isAlphaChar c || c == '_' then
193196
let (identChars, more) = span isIdentChar (c :: rest) in
194197
let ident = pack identChars in
195198
let tokPos = pos in
196199
let nextPos = advanceN pos identChars in
197200
case ident of
198-
"true" => go nextPos more (MkToken (TkBool True) tokPos :: acc)
199-
"false" => go nextPos more (MkToken (TkBool False) tokPos :: acc)
201+
"true" => go k nextPos more (MkToken (TkBool True) tokPos :: acc)
202+
"false" => go k nextPos more (MkToken (TkBool False) tokPos :: acc)
200203
"let" =>
201204
case more of
202205
'!' :: tail =>
203206
let nextPos2 = advance nextPos '!' in
204-
go nextPos2 tail (MkToken (TkKw "let!") tokPos :: acc)
205-
_ => go nextPos more (MkToken (TkKw "let") tokPos :: acc)
206-
"fn" => go nextPos more (MkToken (TkKw "fn") tokPos :: acc)
207-
"if" => go nextPos more (MkToken (TkKw "if") tokPos :: acc)
208-
"then" => go nextPos more (MkToken (TkKw "then") tokPos :: acc)
209-
"else" => go nextPos more (MkToken (TkKw "else") tokPos :: acc)
210-
"in" => go nextPos more (MkToken (TkKw "in") tokPos :: acc)
211-
"region" => go nextPos more (MkToken (TkKw "region") tokPos :: acc)
212-
"drop" => go nextPos more (MkToken (TkKw "drop") tokPos :: acc)
213-
"copy" => go nextPos more (MkToken (TkKw "copy") tokPos :: acc)
214-
"inl" => go nextPos more (MkToken (TkKw "inl") tokPos :: acc)
215-
"inr" => go nextPos more (MkToken (TkKw "inr") tokPos :: acc)
216-
"case" => go nextPos more (MkToken (TkKw "case") tokPos :: acc)
217-
"of" => go nextPos more (MkToken (TkKw "of") tokPos :: acc)
218-
"type" => go nextPos more (MkToken (TkKw "type") tokPos :: acc)
207+
go k nextPos2 tail (MkToken (TkKw "let!") tokPos :: acc)
208+
_ => go k nextPos more (MkToken (TkKw "let") tokPos :: acc)
209+
"fn" => go k nextPos more (MkToken (TkKw "fn") tokPos :: acc)
210+
"if" => go k nextPos more (MkToken (TkKw "if") tokPos :: acc)
211+
"then" => go k nextPos more (MkToken (TkKw "then") tokPos :: acc)
212+
"else" => go k nextPos more (MkToken (TkKw "else") tokPos :: acc)
213+
"in" => go k nextPos more (MkToken (TkKw "in") tokPos :: acc)
214+
"region" => go k nextPos more (MkToken (TkKw "region") tokPos :: acc)
215+
"drop" => go k nextPos more (MkToken (TkKw "drop") tokPos :: acc)
216+
"copy" => go k nextPos more (MkToken (TkKw "copy") tokPos :: acc)
217+
"inl" => go k nextPos more (MkToken (TkKw "inl") tokPos :: acc)
218+
"inr" => go k nextPos more (MkToken (TkKw "inr") tokPos :: acc)
219+
"case" => go k nextPos more (MkToken (TkKw "case") tokPos :: acc)
220+
"of" => go k nextPos more (MkToken (TkKw "of") tokPos :: acc)
221+
"type" => go k nextPos more (MkToken (TkKw "type") tokPos :: acc)
219222
_ =>
220223
case more of
221224
'.' :: rest2 =>
222225
let (tailChars, rest3) = span isIdentChar rest2 in
223226
let full = identChars ++ ['.'] ++ tailChars in
224227
let fullStr = pack full in
225228
let nextPos2 = advanceN pos full in
226-
go nextPos2 rest3 (MkToken (TkIdent fullStr) tokPos :: acc)
227-
_ => go nextPos more (MkToken (TkIdent ident) tokPos :: acc)
229+
go k nextPos2 rest3 (MkToken (TkIdent fullStr) tokPos :: acc)
230+
_ => go k nextPos more (MkToken (TkIdent ident) tokPos :: acc)
228231
else if isDigitChar c then
229232
let (numChars, more) = span isNumChar (c :: rest) in
230233
let tokPos = pos in
231234
let nextPos = advanceN pos numChars in
232235
if elem '.' numChars
233-
then go nextPos more (MkToken (TkFloat (pack numChars)) tokPos :: acc)
234-
else go nextPos more (MkToken (TkInt (pack numChars)) tokPos :: acc)
236+
then go k nextPos more (MkToken (TkFloat (pack numChars)) tokPos :: acc)
237+
else go k nextPos more (MkToken (TkInt (pack numChars)) tokPos :: acc)
235238
else case c of
236239
'(' =>
237240
case rest of
238241
')' :: tail =>
239242
let nextPos = advanceN pos ['(', ')'] in
240-
go nextPos tail (MkToken TkUnit pos :: acc)
243+
go k nextPos tail (MkToken TkUnit pos :: acc)
241244
_ =>
242245
let nextPos = advance pos '(' in
243-
go nextPos rest (MkToken TkLParen pos :: acc)
246+
go k nextPos rest (MkToken TkLParen pos :: acc)
244247
')' =>
245248
let nextPos = advance pos ')' in
246-
go nextPos rest (MkToken TkRParen pos :: acc)
249+
go k nextPos rest (MkToken TkRParen pos :: acc)
247250
'{' =>
248251
let nextPos = advance pos '{' in
249-
go nextPos rest (MkToken TkLBrace pos :: acc)
252+
go k nextPos rest (MkToken TkLBrace pos :: acc)
250253
'}' =>
251254
let nextPos = advance pos '}' in
252-
go nextPos rest (MkToken TkRBrace pos :: acc)
255+
go k nextPos rest (MkToken TkRBrace pos :: acc)
253256
'[' =>
254257
let nextPos = advance pos '[' in
255-
go nextPos rest (MkToken TkLBracket pos :: acc)
258+
go k nextPos rest (MkToken TkLBracket pos :: acc)
256259
']' =>
257260
let nextPos = advance pos ']' in
258-
go nextPos rest (MkToken TkRBracket pos :: acc)
261+
go k nextPos rest (MkToken TkRBracket pos :: acc)
259262
',' =>
260263
let nextPos = advance pos ',' in
261-
go nextPos rest (MkToken TkComma pos :: acc)
264+
go k nextPos rest (MkToken TkComma pos :: acc)
262265
':' =>
263266
let nextPos = advance pos ':' in
264-
go nextPos rest (MkToken TkColon pos :: acc)
267+
go k nextPos rest (MkToken TkColon pos :: acc)
265268
';' =>
266269
let nextPos = advance pos ';' in
267-
go nextPos rest (MkToken TkSemi pos :: acc)
270+
go k nextPos rest (MkToken TkSemi pos :: acc)
268271
'@' =>
269272
let nextPos = advance pos '@' in
270-
go nextPos rest (MkToken TkAt pos :: acc)
273+
go k nextPos rest (MkToken TkAt pos :: acc)
271274
'.' =>
272275
let nextPos = advance pos '.' in
273-
go nextPos rest (MkToken TkDot pos :: acc)
276+
go k nextPos rest (MkToken TkDot pos :: acc)
274277
'=' =>
275278
case rest of
276279
'=' :: tail =>
277280
let nextPos = advanceN pos ['=', '='] in
278-
go nextPos tail (MkToken TkEqEq pos :: acc)
281+
go k nextPos tail (MkToken TkEqEq pos :: acc)
279282
_ =>
280283
let nextPos = advance pos '=' in
281-
go nextPos rest (MkToken TkEq pos :: acc)
284+
go k nextPos rest (MkToken TkEq pos :: acc)
282285
'!' =>
283286
case rest of
284287
'=' :: tail =>
285288
let nextPos = advanceN pos ['!', '='] in
286-
go nextPos tail (MkToken TkNe pos :: acc)
289+
go k nextPos tail (MkToken TkNe pos :: acc)
287290
_ =>
288291
let nextPos = advance pos '!' in
289-
go nextPos rest (MkToken TkBang pos :: acc)
292+
go k nextPos rest (MkToken TkBang pos :: acc)
290293
'<' =>
291294
case rest of
292295
'=' :: tail =>
293296
let nextPos = advanceN pos ['<', '='] in
294-
go nextPos tail (MkToken TkLe pos :: acc)
297+
go k nextPos tail (MkToken TkLe pos :: acc)
295298
_ =>
296299
let nextPos = advance pos '<' in
297-
go nextPos rest (MkToken TkLt pos :: acc)
300+
go k nextPos rest (MkToken TkLt pos :: acc)
298301
'>' =>
299302
case rest of
300303
'=' :: tail =>
301304
let nextPos = advanceN pos ['>', '='] in
302-
go nextPos tail (MkToken TkGe pos :: acc)
305+
go k nextPos tail (MkToken TkGe pos :: acc)
303306
_ =>
304307
let nextPos = advance pos '>' in
305-
go nextPos rest (MkToken TkGt pos :: acc)
308+
go k nextPos rest (MkToken TkGt pos :: acc)
306309
'&' =>
307310
case rest of
308311
'&' :: tail =>
309312
let nextPos = advanceN pos ['&', '&'] in
310-
go nextPos tail (MkToken TkAndAnd pos :: acc)
313+
go k nextPos tail (MkToken TkAndAnd pos :: acc)
311314
_ =>
312315
let nextPos = advance pos '&' in
313-
go nextPos rest (MkToken TkAmp pos :: acc)
316+
go k nextPos rest (MkToken TkAmp pos :: acc)
314317
'|' =>
315318
case rest of
316319
'|' :: tail =>
317320
let nextPos = advanceN pos ['|', '|'] in
318-
go nextPos tail (MkToken TkOrOr pos :: acc)
321+
go k nextPos tail (MkToken TkOrOr pos :: acc)
319322
_ => Left (UnexpectedChar '|' pos)
320323
'+' =>
321324
let nextPos = advance pos '+' in
322-
go nextPos rest (MkToken TkPlus pos :: acc)
325+
go k nextPos rest (MkToken TkPlus pos :: acc)
323326
'-' =>
324327
case rest of
325328
'>' :: tail =>
326329
let nextPos = advanceN pos ['-', '>'] in
327-
go nextPos tail (MkToken TkArrow pos :: acc)
330+
go k nextPos tail (MkToken TkArrow pos :: acc)
328331
_ =>
329332
let nextPos = advance pos '-' in
330-
go nextPos rest (MkToken TkMinus pos :: acc)
333+
go k nextPos rest (MkToken TkMinus pos :: acc)
331334
'*' =>
332335
let nextPos = advance pos '*' in
333-
go nextPos rest (MkToken TkStar pos :: acc)
336+
go k nextPos rest (MkToken TkStar pos :: acc)
334337
'/' =>
335338
case rest of
336339
'/' :: tail =>
337340
let (comment, more) = span (\ch => ch /= '\n') tail in
338341
let skipped = '/' :: '/' :: comment in
339342
let nextPos = advanceN pos skipped in
340-
go nextPos more acc
343+
go k nextPos more acc
341344
_ =>
342345
let nextPos = advance pos '/' in
343-
go nextPos rest (MkToken TkSlash pos :: acc)
346+
go k nextPos rest (MkToken TkSlash pos :: acc)
344347
'%' =>
345348
let nextPos = advance pos '%' in
346-
go nextPos rest (MkToken TkPercent pos :: acc)
349+
go k nextPos rest (MkToken TkPercent pos :: acc)
347350
'"' =>
348351
case readString pos rest of
349352
Left err => Left err
350-
Right (s, more, nextPos) => go nextPos more (MkToken (TkString s) pos :: acc)
353+
Right (s, more, nextPos) => go k nextPos more (MkToken (TkString s) pos :: acc)
351354
_ => Left (UnexpectedChar c pos)

0 commit comments

Comments
 (0)