rhiannon morris
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
rhiannon morris
fa7f82ae5a
rename Nat to NAT in AST
2023-11-03 18:05:54 +01:00
rhiannon morris
e0ed37720f
always vsep scheme lets, otherwise they are unreadable
2023-11-03 18:05:54 +01:00
rhiannon morris
050346e344
add postulate, #[compile-scheme], #[main]
2023-11-03 18:05:54 +01:00
rhiannon morris
80b1b3581a
use ST from base
2023-09-19 13:05:01 +02:00
rhiannon morris
e6c06a5c81
pass the subject quantity through equality etc
...
in preparation for non-linear η laws
2023-09-18 21:53:38 +02:00
rhiannon morris
a221380d61
more effect stuff, incl. ST
2023-08-25 18:59:54 +02:00
rhiannon morris
42aa07c9c8
crude but effective stratification
2023-05-21 20:34:05 +02:00
rhiannon morris
d5f4a012c5
add source locations to inner syntax
2023-05-02 03:06:25 +02:00
rhiannon morris
30fa93ab4e
refactor core syntax slightly to derive Eq/Show
...
add a new `WithSubst tm env to` record that packages a `tm from`
with a `Subst env from to`, and write instances for just that. the
rest of the AST can be derived
2023-04-27 21:37:20 +02:00
rhiannon morris
b666bc20cf
do scope checking in FromParser where it belongs
2023-04-18 22:55:23 +02:00
rhiannon morris
4578b30c79
namespaces work now
2023-04-18 00:10:53 +02:00
rhiannon morris
a5ccf0215a
coercions and compositions
2023-04-15 15:13:01 +02:00
rhiannon morris
ba2818a865
remove IsQty interface
2023-04-01 19:16:43 +02:00
rhiannon morris
6dc7177be5
use NContext/SnocVect for scope name lists etc
2023-03-16 18:18:49 +01:00
rhiannon morris
efca9a7138
add enums, which also need whnf to be fallible :(
2023-02-22 07:45:10 +01:00
rhiannon morris
0e481a8098
new representation for scopes
2023-02-22 07:40:19 +01:00
rhiannon morris
7895fa37e5
Q.S.T.Reduce ⇒ Q.Reduce and make it use Definition directly
2023-02-19 18:54:59 +01:00
rhiannon morris
42798f243f
typed equality
2023-02-10 21:52:40 +01:00
rhiannon morris
92617a2e4a
whnf actually reduces to whnf now (probably)
2023-01-23 03:02:55 +01:00
rhiannon morris
c45a963ba0
parameterise over qty semiring
2023-01-08 20:44:25 +01:00
rhiannon morris
da91f7d95e
a few more tests
2022-05-27 18:00:06 +02:00
rhiannon morris
bc9344c6ba
some reduction tests & fixes
2022-05-25 16:10:19 +02:00
rhiannon morris