Commit graph

571 commits

Author SHA1 Message Date
8823154973 add golden test stuff 2024-04-14 20:49:10 +02:00
b7dc5ffdc4 add check for #[main] type 2024-04-14 16:20:40 +02:00
dd697ba56e add CheckBuiltin 2024-04-14 16:20:25 +02:00
32b9fe124f minor tweaks in Q.Typing.Context 2024-04-14 15:48:10 +02:00
95a0b38d74 update pretty-printing tests 2024-04-12 22:00:08 +02:00
7883a3cae7 pretty printing fixes 2024-04-12 21:54:25 +02:00
a1d8fd4ab5 %inline 2024-04-12 21:53:54 +02:00
9d60f366cf add #![log] pragma 2024-04-12 21:53:54 +02:00
f56f594839 push multiple loglevel changes at once 2024-04-12 21:53:54 +02:00
fca75377a0 MakeName ⇒ MkName for consistency 2024-04-12 21:53:50 +02:00
11b0ab6a25 remove default from FromParser.fromParserPure and Main.step 2024-04-07 03:20:42 +02:00
7a0bc73d25 approximate log stack in handleLogDiscard 2024-04-06 20:14:24 +02:00
567176e076 log refactors 2024-04-05 18:43:00 +02:00
3b6ae36e4e add logging to core 2024-04-04 19:26:41 +02:00
861bd55f94 add log effects to FromParser 2024-04-04 19:26:41 +02:00
e6ad16813e add log effects to executable 2024-04-04 19:26:41 +02:00
78555711ce add Q.Log 2024-04-04 19:26:41 +02:00
ec839a1d48 big Main refactor 2024-04-04 19:26:41 +02:00
727f968afb add delimited continuations to bib 2024-04-04 19:26:30 +02:00
41c8a92c97 bib fixes 2024-04-04 19:26:13 +02:00
efddb1aea1 skip broken pretty-printing tests till i fix them 2024-03-27 18:21:45 +01:00
8cba73f741 bump pack collection 2024-03-27 18:21:26 +01:00
582666a254 comments in infer for coercions 2024-03-21 21:29:13 +01:00
a9e8f14ad5 fix a small bug in Q.Whnf.Coercion 2024-03-21 21:29:01 +01:00
a8ac6f11f7 fix a quantity in CaseBox 2024-02-28 16:49:15 +01:00
b67162bda1 fix the other similar loops
closes #38, again
2024-02-24 16:04:38 +01:00
24ae5b85a2 fix a broken test???? 2024-02-24 15:45:04 +01:00
325e128063 add η for False and True 2024-02-10 11:39:07 +01:00
642ac25a71 happy new year [pack update. also idris 0.7.0] 2024-02-10 10:14:22 +01:00
05a688d49e reject "" in NatExtra.fromHex 2024-02-10 10:14:22 +01:00
1c8c50f3e2 remove some unneeded Ord impls 2024-02-10 10:14:22 +01:00
f337625801 remove most noLocs 2024-02-10 10:14:22 +01:00
1f01cec322 refactor Main a whole lot 2024-02-10 10:14:22 +01:00
103f019dbd move NDefinition to Quox.Definition and add an untyped one 2024-02-10 10:14:22 +01:00
2cafb35bc1 fix some comments 2024-02-10 10:14:22 +01:00
47069a9316 fill a stray hole 2024-02-10 10:14:22 +01:00
fb14b756c7 add algebraic ornaments to bib 2024-02-10 10:14:22 +01:00
81783dbae0 fix typechecker loop when coercing boxes
closes #38
2024-02-10 10:07:06 +01:00
a14c4ca1cb never inline let bindings from the original source 2023-12-21 18:04:12 +01:00
b7074720ad pretty printing fixes 2023-12-21 18:03:57 +01:00
48a050491c fix several quantity issues
- contents of box intro
- definition of let
- non-recursive ℕ case
- also make a few var names more consistent
2023-12-21 18:01:17 +01:00
aa4ead592a allow "let x : A = e in s" with type annotation 2023-12-21 17:54:31 +01:00
54db7e27ef make #[fail] run in the current namespace 2023-12-21 17:53:46 +01:00
7afcbfe258 recognise nats other than 0 in eq checker 2023-12-21 17:48:12 +01:00
0fdd4741be print quantity on let 2023-12-07 01:43:39 +01:00
03c197bd04 add local bindings to context
- without this, inside the body of `let x = e in …`, the typechecker
  would forget that `x = e`
- now bound variables can reduce, if they have a definition, so RedexTest
  needs to take the context too
2023-12-07 01:43:39 +01:00
cdf1ec6deb fix a comment 2023-12-04 23:38:17 +01:00
08a8c694b1 a usage in hello.quox. why not 2023-12-04 23:36:30 +01:00
8b8129027d update syntax.ebnf 2023-12-04 23:35:54 +01:00
e48f03a61c multiple semi-sep binds in a let 2023-12-04 23:27:59 +01:00