GitHub PushEvent at 2014-12-11 17:17:01
Repository: tog
Actor: bitonic
Payload: {"shas":[["49f40ad7a7fd7bd1a2becd283e349f5272d58d5c","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Make contextual definitions work.\n\nSadly we're not using them anywhere, but that shall changes soon.","Francesco Mazzoli",false],["702aabc0f5056ad37b95529a841ef445f0b7ffba","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","WIP Make all definitions under a context\n\nMoreover, represent the context argument of a definition explicitely.\nRight now Term.hs compiles and that's it.","Francesco Mazzoli",false],["83da7760ff2be9a0f20cd22c2ad941f8bbf88158","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Use `Contextual` in data constructors too.\n\nAnd projections.","Francesco Mazzoli",false],["50d1d1db0e077f9dc48de3d6aac460660532653e","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Set up Contextual infrastructure...\n\n...without actually implementing the contextual bit.  Tests pass.","Francesco Mazzoli",false],["ecfeb97153df796411d3b95be0ab282195793a45","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Use Ctxs in declaration checking.","Francesco Mazzoli",false],["976b719068cb96045adf1ab07dc2455723f67ebd","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","IsTerm constraint in MonadTerm","Francesco Mazzoli",false],["19937166ae6824f1efaab3f882e2493b1c19c14f","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Set up more infrastructure for 'Opened' names\n\nThis includes a refactor of the TC monad -- we now parametrise over an\nenvironment type too.\n\nRight now constructor-headed function inversion doesn't work.","Francesco Mazzoli",false],["25033969bfbe4431663bf0f03d310d23128c480f","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Implemented where clauses...\n\n...but I still need to change name to have them qualified.","Francesco Mazzoli",false],["806b6bebbd92ed1090c416b65d106ff303e6bc2b","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","WIP implement modules","Francesco Mazzoli",false],["af092123f5b8d7bb4db341e2a4c4a1d63f3efd23","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","WIP Implement modules\n\n\"Only\" scope checking is missing now.","Francesco Mazzoli",false],["afbaa4ec3b7bd1725ea57d7e0658cd41e8173fbd","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","WIP Attempts at scope-checking","Francesco Mazzoli",false],["ea81387236d1cd1a9afa53c71c1f0a5eb36156a0","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","WIP Keep scope checking, cleaner now.","Francesco Mazzoli",false],["00b2d039374acf86e905695c4bd5592a0615c82b","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Forgot to delete commented out code","Francesco Mazzoli",false],["88200158d4b88994da8e2be77255d155a2543a42","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Add auto-import of modules with no args.","Francesco Mazzoli",false],["81382764b964f586ffda7a912dfa12f7679cdb5c","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Type check modules.  Things seem to work.","Francesco Mazzoli",false],["175730b930d484600f90b2151299fc718ef74ac5","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Make the tests work.\n\nNote that now interaction with Agda is getting more complicated -- `open\nimport Prelude` is interpreted by `tog`.  Moreover, I don't want to make\nan effort in mimicking the record behaviour, since we're probably going\nto change it anyway.\n\nNote that the released `bnfc` is buggy, and the git `bnfc` is buggy, so\nwhile <https://github.com/BNFC/bnfc/pull/116> gets merged you need my\nversion of `bnfc`: <https://github.com/BNFC/bnfc/pull/116>.","Francesco Mazzoli",false],["77c6da9a25131d94aac5d9f3b2e9c041474bc00f","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Cleanup","Francesco Mazzoli",false],["e050d7933aa031582c80d2d4de660fa9a2b87564","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Test equality of module parameters.\n\nStrangely now this works, probably because the terms get expanded when\nchecking.  In any case, I should probably replace the calls to `synEq`\nto `defEq` or similar.","Francesco Mazzoli",false],["05933392b3e614f5b690af019269df48ff737dbd","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Kill the interactive mode.\n\nIt was hacky and I don't have the time to  adapt it to the modules now.\nA better story for carrying the `Scope` forward is needed.","Francesco Mazzoli",false],["7003200ad7f94cb5497ce0e36197df07840ba0c4","4a0a19218e082a343a1b17e5333409af9d98f0f5@mazzo.li","Hackily make function inverting work.\n\nRight now we invert only if the data constructors we need to instantiate\nthe meta-variables with are not parametrised over anything.  This is\nbecause if it is parametrised it's much trickier to instantiate the\nmeta-variable.  In any case, this needs fixing in the long run.","Francesco Mazzoli",false]],"size":21,"ref":"refs/heads/master","head":"54686b1ee995346abba92acce2d4ac582b45846f"}