From 4c205a0c283a4bb8ac323155a45ba007ec04fbc5 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Thu, 29 Aug 2024 21:58:46 -0700 Subject: [PATCH] update readme --- README.md | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index e3b40ce..9b48849 100644 --- a/README.md +++ b/README.md @@ -1,15 +1,6 @@ -"Unifiers as Equivalences" has unification with types. Look into adapting some of that (or at least read/understand it). Indexed types are mentioned here. - -"Elaborating Dependent (Co)pattern Matching" describes building case trees. Section 5.2 has the algorithm. - -"A prettier printer" was the basis of the pretty printer. - -"Elaboration Zoo" was a resource for typechecking and elaboration. In particular pattern unification and handling of implicits is based on that. - - - [x] Support primitives -- Make DCon/TCon separate from Ref? (Or add flavor to VRef/Ref? If processing is often the same. I think I want arity though. I don't think a checked DCon can be overapplied, but it could be underapplied without special form. And special form is possibly difficult if not collecting a stack on the way down... +- [ ] Make DCon/TCon separate from Ref? (Or add flavor to VRef/Ref? If processing is often the same. I think I want arity though. I don't think a checked DCon can be overapplied, but it could be underapplied without special form. And special form is possibly difficult if not collecting a stack on the way down... Need to typecheck case - learning stuff like `n = S k` is not happening and the final bit of the data constructor doesn't unify with the data type, because we're not handling `Bnd n =?= Val`. Cockx collects a list of constraints. We might want flags on unification to enable that? @@ -123,6 +114,7 @@ Code generation is partially done. We're stopping at zoo4 for now. + ### Typecheck / Elaboration - [ ] think about whether there needs to be a desugar step separate from check/infer @@ -134,6 +126,19 @@ We're stopping at zoo4 for now. - [ ] look into Lennart.newt issues - [ ] figure out how to add laziness (might have to be via the monad) + +### References + +"Unifiers as Equivalences" has unification with types. Look into adapting some of that (or at least read/understand it). Indexed types are mentioned here. + +"Elaborating Dependent (Co)pattern Matching" describes building case trees. Section 5.2 has the algorithm. + +"A prettier printer" was the basis of the pretty printer. + +"Elaboration Zoo" was a resource for typechecking and elaboration. In particular pattern unification and handling of implicits is based on that. + +### Misc Notes + So smalltt has TopVar with a Level. typechecking binders end up as top too. Also delayed unfolded values for top or solved metas. This looks like glue - all the bits for the top and a cached value (it's keeping top as values).