pristine:d94ad4fbf78ce4fd3021173337d1379669c0009f96b7562536a72f374af629b9 [Started formalising "Compiling Exceptions Correctly" by Hutton/Wright. Nils Anders Danielsson **20080205010934] hash: 0000004902-ef98585d2e70a8445f24904bc233b5fff95c58fe0701f521a72439e252eb05a6 [Renamed exec s ops to ⟪ ops ⟫ s. Nils Anders Danielsson **20080205011003] hash: 0000003077-ecdd4956d80de42a619c3ef389629169edab5e0af8e3f7eb890a510a97147b84 [Split up the code into reusable modules. Nils Anders Danielsson **20080205013235] hash: 0000003530-7998805358a2aacaa0ee162264c2bbee16bd8f5e33a52f305a6fd8401753774c [Started on an attempt to calculate an abstract machine. Nils Anders Danielsson **20080206201551 + Unfortunately the proof seems to require extensionality. ] hash: 0000007971-79e36cc5b4c81dd621ce0a103fc6ac4cf71fd7251f4cc1c451f27c38a10e99c8 [The module now assumes extensionality. Nils Anders Danielsson **20080206233441] hash: 0000000870-5eca43d74c823db08e60c77c046c3802cda786ca6eadd1c5a6a5b018a312dc5a [Added a boring file. Nils Anders Danielsson **20080206233536] hash: 0000000189-2d2ad1cff9fd60fe24f969d9172c5f94ffe65d8d78d23a1460854b91b1385531 [Finished the Hutton/Wright derivation. Noted that it has a bug. Nils Anders Danielsson **20080207005559] hash: 0000005681-b086bc694b61ddcdc78d1df40d4152be82264e6025cc7eb12ff2cb6e1ca58048 [Broke out some definitions which simplify calculations. Nils Anders Danielsson **20080207022158] hash: 0000000700-f38ff56813713eb21320dd7f5e5d4e51876ee10564d0c102784b68253c570681 [Tried fixing the bug, but ended up just moving it around. Nils Anders Danielsson **20080207022519] hash: 0000002217-938dbcc9b566bd412bc5d58db3e2b1a9a343d85694bdcb8e9fba5e0dcfea5cef [Started extending the calculation to exceptions. Nils Anders Danielsson **20080207023248 + The calculation is mostly finished, but suffers from the same problem as the one in HuttonsRazor.agda. + Note that my calculation is not quite identical to the Hutton/Wright one. ] hash: 0000009117-38166b31120b4506c3bb02bf9405db5bd5dccb37b48a444e498aa67b5c53cd4f [Hutton/Wright's code is not structurally recursive. Nils Anders Danielsson **20080207024840 + Hence my problems. ] hash: 0000000958-a42986e3c874a1df5c66d47bb100a3b326aff6154d78ff934dee37e3af919293 [Tried showing that the code is terminating. Nils Anders Danielsson **20080209205756 + The termination checker does not accept this code, though. Reason: Inequalities like sizeC c < suc (sizeC c) are not derived. ] hash: 0000002005-6eafb202166847919e434cb92aeab8d1b5530d4a6220e8f759ce57c7bf987c79 [Tried using a slightly different method to prove termination. Nils Anders Danielsson **20080210021346] hash: 0000002882-ee6a9eea3e4d7fd0d68402033c34aac7e22e738a3e6adbcc75b361e7060eac77 [Forced the termination proof to completion. Nils Anders Danielsson **20080210021536] hash: 0000004275-a3c451077e26a5a87d102d8c34ab678f13add095dd235460d72d0876eae61a46 [Simplified the termination proof. Nils Anders Danielsson **20080210021631] hash: 0000003635-702bfaebc28399cd4a2b54226d69e4fa67ac32f840fff122aa840c9b7c4b4c0d [Started formalising one of Wand's derivations. Nils Anders Danielsson **20080224021845] hash: 0000006275-c06102f9c3f188de2b9609eacdb946b0914ef48c3a88ca8427d988dc0611f1f2 [Replaced type vectors with type lists. Nils Anders Danielsson **20080224022258 + Since I don't need to know the length. ] hash: 0000002029-785065d36d35923700eb6b0fe4ceab6fa3ab6e4a6a7418ae057c3f5f7411d968 [Added the first step of the compiler. Nils Anders Danielsson **20080302222628] hash: 0000003815-802cfc10730c66fb6a2bc3647fa60e9a8791c401ab088d5ef8cd8303e1ac9332 [Extracted type lists and _⟪_⟫_ into a separate file. Nils Anders Danielsson **20080302224036] hash: 0000005827-b1e24099bf6576fbc0938ce77fdbc602c00790c77395c20460858e3491f9d06c [Tried using uncurried functions, but this was awkward. Nils Anders Danielsson **20080302230339] hash: 0000002079-f165eff547030ce941424843adc250cb433709dd765afa747d1d3c1a38ef8988 [Tried using uncurried functions, but this was awkward. Nils Anders Danielsson *-20080302230339] hash: 0000002079-79ac0af4f09008d08421a6817fa3607c018b6c24ce28d6fe6d38b41bee792250 [Made it easier (?) to apply the right-assoc lemma. Nils Anders Danielsson **20080303000703 + In the left-to-right direction. ] hash: 0000001772-886f346e390c5919eab63ae67f7b04565ea4713e0aabde34ac0d64fb8f747eae [Parameterised top-level module on Id (instead of every individual module). Nils Anders Danielsson **20080304230431] hash: 0000000578-aacbf6f74ce60a13b63cfa6858372e2778f656a4ca2835abcf5893f43d3d1f14 [Simplified second step by indexing expressions on their semantics. Nils Anders Danielsson **20080304230717] hash: 0000001192-6ee1eb2db27452bfaf889f3e414b05dbc39b47958559d6fae7cb5d7f745e04bf [Replaced type lists with the new Data.List1. Nils Anders Danielsson **20080305000632] hash: 0000005869-8c6315500cd7d75862efccfa0921cfcea66c9c08e76cf7fc3a208715df24e3c8 [Added a universe and a variant of the compiler which uses the universe. Nils Anders Danielsson **20080305011239] hash: 0000003120-d0bb5c31a054e7d3e258a275b688c63a066ab0dcaaff646780d7fd6279bc593d [Added some examples. Nils Anders Danielsson **20080305021144] hash: 0000001019-ba82e6a8393fb9ef707a4a4e75b2cca04e7f5d06de73105a9169d56f442d7c36 [Simplified the universe a little. Nils Anders Danielsson **20080305025215] hash: 0000000346-f40b1973ccaf7edc909dce10c2dde9c4b2c4f214465217827aaf193c4bbc22ce [Started on the rotation code. Nils Anders Danielsson **20080305025625 + In order to continue I need to either generalise the type of the resulting linear expressions, or specialise the types of the input expressions. ] hash: 0000001901-691822c0eac5c1486f76e46ed3cf9fdc6d731f4a8fc4a3825b730121bcaf5c99 [Reduced the universe level of a type. Nils Anders Danielsson **20080305025947] hash: 0000000241-8503a1c18de7fc446fa8dae25d13a2aa30db6fefb9d29195d9a574d04d27b3dc [Finished the code for rotation. Nils Anders Danielsson **20080305040437 + Did this by specialising types. The code is currently a bit ugly. I would prefer more general types. + No correctness proof yet. ] hash: 0000006911-0c79182b9ceb7ef17d52777308b3081a98fa3957c820e4eb7ca82c446755685b [Set the stage to prove correctness of rotation. Nils Anders Danielsson **20080305143644 + Cleaned up the code, proved some lemmas, stated correctness. ] hash: 0000007702-b6d09292281b1c842b98894ed415a0739d4c393a3e04816f026dce4081559628 [Removed the universe, which turned out to be unnecessary. Nils Anders Danielsson **20080305234646 + When I specialised the types the type indices turned into integers, so I did not need to pattern match on any elements of Set. ] hash: 0000005743-4bbfb563b9d8188979fb8ddd231b2d91a32014bbb1918af1ce8e39aeeedc6ebb [Stated the right associativity lemma using casts. Nils Anders Danielsson **20080306014158 + This made both the statement and the proof more complex. ] hash: 0000002661-9357d7b6f5080b4090292f29581e7bf224eea1db3a15274e31904f4b6875cf04 [Simplified the right associativity statement by using difference lists. Nils Anders Danielsson **20080306134221] hash: 0000004997-8fb29db95cd5e30355617833c918d866f3cb59a9f6803f6bd1acba9aae9f35fe [Included the map id ≡ id law as well. Nils Anders Danielsson **20080306134847] hash: 0000001790-c4bd7c18b615586455002c2de2e2b85fac738bf5308f7a777fa862bb51b9125d [Removed B⋆, renamed B⋆* to B*. Nils Anders Danielsson **20080306135503] hash: 0000001821-39475780eb238757a6ad6b71ff708974215437c97843eab81b170ade6cc165fb [Tried switching from casts to conversion functions. Nils Anders Danielsson **20080306135611 + This didn't help much. ] hash: 0000002863-30b841f16b6c2cdd7526ee6f77da4b471db152d2e9f4f52dc2ec62d92f11b5c0 [Added _⟪_⟫-cong_. Nils Anders Danielsson **20080306135929] hash: 0000000409-e0dd7e05c0481259ad2d7b8271cbdda85e506a57b3343d81518c2de10dfc4892 [Renamed Fun to _→_. Nils Anders Danielsson **20080306140736] hash: 0000001221-8880e31f2bd6f2b29d7c9edab7c0094c4371ec6426497f5e69e8608e0bcf9677 [Added _^_. Nils Anders Danielsson **20080306141239] hash: 0000000260-6454b018d3b340f03bc760e11465680ba8c630b719d762c84ba2902a74bd1275 [Converted Wand to the new _⟪_⟫_. Nils Anders Danielsson **20080306162646] hash: 0000007069-beb76758f0014185e8edb535e7190410ad9bad640a8afaee865b59b04307ec01 [Renamed _◅_ to _▻_. Nils Anders Danielsson **20080306162910] hash: 0000003709-98bb0e0709e00c7816697d673b8a8b75db73b80198160972795600b3e3d7ed63 [Proved rot-lemma. Nils Anders Danielsson **20080306231042] hash: 0000009495-8816da7d664cef682f9266d9dfe104fbd155d579bfd5c9ab48ed1f767eb37b9b [Improved comment. Nils Anders Danielsson **20080307012110] hash: 0000000350-3d410e8a10b6e2c1112861c5251ae27bec239c2f4815d2a2aa9e352bd2ddb084 [Reduced code duplication. Nils Anders Danielsson **20080307025832] hash: 0000000846-f7cef8462b5ffe210c3db89a14897d09ee1e35e08e1382da5b99b738e536e71b [Defined an interpreter. Attempted a correctness proof. Nils Anders Danielsson **20080307030133 + However, the correctness statement appears to be incorrect. ] hash: 0000002908-bfc116fdd6751b7a13183ac1b84e4bf7d6f2834edd8a505ad5f3d081e6114dc7 [Changed to a possibly correct correctness statement. Nils Anders Danielsson **20080307033740] hash: 0000003362-0f51aff8b5aa28852954c3eec9664ca42aa759231ae202221716712875bd9b8f [Started formalising Danvy et al's compiler derivation. Nils Anders Danielsson **20080310021949 + Or something inspired by it. ] hash: 0000006361-42a514e1ac5045ea286084a9c51c926bdafcc44f933ea885f236bd7d30bd2505 [Started using Data.Star from the standard library. Nils Anders Danielsson **20080312003502] hash: 0000006551-1ae87a8b5a0a1f87014629c6a424189f865cba3c27323a45cbd4952aefa9001a [Updated code to reflect changes in library API. Nils Anders Danielsson **20080312010019] hash: 0000004192-7096c8dea7c888bec3a93d0e9ea898b426c59f872bc4bbb4945b79c7a7821bb5 [Updated code to reflect changes in library API. Nils Anders Danielsson **20080312210814] hash: 0000000185-688e4a75e3200c20e26ad2aa84844d08eb96d713320b4a0e21489183c815ec75 [Added a comment. Nils Anders Danielsson **20080312211238] hash: 0000000372-75cb78587456e52a386f867354bf92a4770bd523d45b6f99f2256bdc9d4257cc [Renamed the first attempt at following Danvy et al. Nils Anders Danielsson **20080312223027] hash: 0000000362-303a0e86bafbc51af9ab782f27b6dc3b9c6790f0d9862e6b4986a97bc0a6e906 [Started proving the last few lemmas, but they are too awkward. Nils Anders Danielsson **20080312223843 + I don't want to push this any further without first simplifying things. ] hash: 0000005221-f934d288b37717c58af9771a0042a441ef8bbcc2a5b9608d29db4c0ccf94be95 [Started proving the last few lemmas, but they are too awkward. Nils Anders Danielsson *-20080312223843 + I don't want to push this any further without first simplifying things. ] hash: 0000005221-27d6175cb54196970fb8ef84ea4775f784f2b55ed42b78ca3be491e421860ff3 [Postulated some awkward lemmas. Nils Anders Danielsson **20080312224624] hash: 0000001420-dab00c4a921bf26283dc841320c782b069b4591a57a5d46234f24e8682ed6784 [Started formalising another of Wand's papers. Nils Anders Danielsson **20080314011924 + He claims that the method used in that paper is easier than the one I tried formalising in Wand.agda. ] hash: 0000003605-cbde87dd757b98500cec1db4da787a22b758b4b15484e6191c7b5f1ce8c780b5 [Implemented the simply typed lambda calculus with multi-argument functions. Nils Anders Danielsson **20080314052458] hash: 0000005854-3082bf0f0e8ebcc41c8f66a86c5fbce2568db4cc075e914b60c1002813ccc503 [Started on the derivation. Did (parts of) the defunctionalisation. Nils Anders Danielsson **20080315011706] hash: 0000003891-66d75df6848a962f5b33c3bf0cb56a197717583596d3babe26bb778fa11e5c8f [Updated code to reflect changes in library API. Nils Anders Danielsson **20080513173925] hash: 0000006590-3f1f40203d612123ecf4185c296923ea161379e6caa288aff962b25e69a18649 [Another approach to compiling Hutton's razor. Nils Anders Danielsson **20080513181929] hash: 0000003399-5f9f2e4bd88859491397de1444522b46e18cae9e8ecf7ed57aab0de5c64bb688 [Switched to ordinary ℕ and Vec instead of the variants based on star-lists. Nils Anders Danielsson **20080513193052 + Since the code becomes a bit easier to understand. ] hash: 0000002653-f9a27e63e13bef8ca1055a9ad6431df9562c097289340d3aa62f18a653a5f7e0 [Proved compiler correctness. Nils Anders Danielsson **20080514095207] hash: 0000004712-387eeb1d7683658b456a97e1d067ddeea08da718cf1dbf655f2ef1d87ddeed6b [Simplified the correctness proof. Nils Anders Danielsson **20080514095642] hash: 0000000953-6ceeae42250236b664560173aff1094fd8e0d379e929e20f16fb068862e27e85 [Simplified the proof again. Nils Anders Danielsson **20080514102418] hash: 0000005069-8dfd8bac0853e3a2080e6bd33b861cb9480b06475f7711edbb09fcfdfb9962b5 [Replaced reverse composition with ordinary composition. Nils Anders Danielsson **20080515092302] hash: 0000001080-0e47a5be7f0531bd0de42486b65aa878cee197cc0c3fc5eb64cd88130abb558a [Replaced reverse composition with ordinary composition. Nils Anders Danielsson *-20080515092302] hash: 0000001080-6e67e67874e42483b1654ce3436e00a9addad350762f44b5f44a06553cb7b4f0 [Updated code to reflect changes in library API. Nils Anders Danielsson **20080918152933] hash: 0000001192-b6e56debb667f7e1bebda1e7ed28f91229804df46a0082ee349df89aa560f7a9 [Removed incomprehensible remark. Nils Anders Danielsson **20081014202231] hash: 0000000365-174d62d6aa5022f4579f3431929d5a7b229d246e71868a3862508cd19e5c9230 [Updated code to reflect changes in Agda. Nils Anders Danielsson **20081216004414] hash: 0000001036-cdf3480c899b6b79c316ec2a456180f07bfd6dfb65266cb42e01a839574c2147 [Updated code to reflect changes to Agda and the library API. Nils Anders Danielsson **20091015185044 Ignore-this: c08f14565bc6243c0d276d60b456cb79 ] hash: 0000026291-48a30733fc4fe011206b21cc568f4690bb003a6af6c244e7199f7feb0a5faef1 [Replaced ->, forall, \ and a with →, ∀, λ and A, respectively. Nils Anders Danielsson **20091104223323 Ignore-this: 79c0359860b5c4405fc2b055106204ae ] hash: 0000004100-ec6d75f4212a2c17d4339123f9e01a92d5728e0c5cd313e3db5a811ba8dc1ef7 [Improved the documentation. Nils Anders Danielsson **20091104235649 Ignore-this: 45fde22a7b85f3c016b2f255b431ffda ] hash: 0000000928-f20676a2cf99a53a2b34d323a5e213e7f9986402ef48124f3d01e9aee4155dbb [Broke out the stack code to a separate section. Nils Anders Danielsson **20091105001251 Ignore-this: f13672eea1fe4cc2212c6782546bd03 ] hash: 0000003763-bc237e9aeab75523355fdffddb1a6316f02cc155dddfbe43719c3f7b849bfe5d [Simplified a function. Nils Anders Danielsson **20091119134932 Ignore-this: ed2e9f13fbea1371d5a9e7ca08a86113 ] hash: 0000000409-4e96e59587ef9bbef9f46d8db76a94d4afca1ac03bf5ca6fcde8f81267a71e3d [Made EqualTo universe polymorphic. Nils Anders Danielsson **20091119135025 Ignore-this: dbfd13fc9d3db2b7485f887b1b1467c7 ] hash: 0000000917-3ed1e4d5a39ab6934071b0f4f34fd6d6b52289d3c42353834f0d1f1e430ccdd9 [Added ▶_. Nils Anders Danielsson **20091119135037 Ignore-this: f32cd952d3e5c75f85064f606c7ad41e ] hash: 0000000397-9ce8b633ab1c2633f7da029697e25478a110ceaf7cd077a129707afe58989113 [Generalised reverse composition. Nils Anders Danielsson **20091119135051 Ignore-this: 4260670fd7a20df98ba923af4f79cef0 ] hash: 0000001726-67b3c559982f80f42b4d405fe3ed8fd263ebf93e6a40144674db87bdf7ccc9c9 [A compiler derivation based on generalised reverse composition. Nils Anders Danielsson **20091119135116 Ignore-this: 57175ff46b32a698d56e261d43fb90f8 ] hash: 0000014784-cbdf0e7567eafb672c82d76c22837cdbd5426124b5ae83e1476b980934f7306e [Dropped the assumption of extensionality. Nils Anders Danielsson **20091119140846 Ignore-this: 31da99d3fd9cd3e61109c542d581a997 ] hash: 0000004471-00278d58a209f94bdf1f17d4bbdfe540b37cd182246fc29f5e4ad1db25655e6f [Got rid of many explicit indices. Nils Anders Danielsson **20091119145529 Ignore-this: da33cb72de711f636ee4056add8444c1 ] hash: 0000011206-b43ce8b5e69131e62ddba05e62b41e459c7ad8fb3afeeaa39745646e719c3cbe [Removed comment. Nils Anders Danielsson **20091119165538 Ignore-this: 4544972446006fafa44876497af74c01 ] hash: 0000000234-845b122f23dd780da600bfbb55f88a95c90c6a1740a8ecfc9d992a3b09e0656a [Removed arity. Nils Anders Danielsson **20091119165746 Ignore-this: 58d3158f52cccc0664c8cb039a885b23 ] hash: 0000000247-6bf91a4e175873553b126427e1e8f1b1bc5e24ffc90f3d87d269c9c2283a07c1 [Added a step which switches to an explicit stack. Nils Anders Danielsson **20091119170238 Ignore-this: 2313b2be50c1192426d56d3dcda89d71 ] hash: 0000002721-b04a63f0982d2fa6b4e4bfe92857d7a633a40509afe969b46726b119b798579a [Updated boring file preference after conversion to darcs 2 format. Nils Anders Danielsson **20091119173724 Ignore-this: 1feb7bc95c6892378342a0ba7cc53686 ] hash: 0000000221-0247b572c0101fce9272836e6766c8850b010130c39811702ea3753f332fe845 [Switched to a more general definition of "n-ary functions". Nils Anders Danielsson **20091127193044 Ignore-this: b3bd6e76f77d456ce5e965b33722ac6d ] hash: 0000014029-ff223550431f68fdf25442f8c9179750007d72efb12d5a9d0a0de27eac47ba8f [Simplified the definition of equality. Nils Anders Danielsson **20091127194056 Ignore-this: 7a7f0f8816cb548ff2574b46d062d453 ] hash: 0000006584-305f8853878489655e68b2bbc13924b23d34ee794ef408cf11806509df2baf3e [Made the code a bit more tidy. Nils Anders Danielsson **20091127194434 Ignore-this: 6e4a554add27d8b6d2b68a4683a43aa0 ] hash: 0000001583-3f7febf3b794e1f650e40953c876b75cf288cb20c0174ea60667135b567d3d1e [Simplified a proof. Nils Anders Danielsson **20091127195853 Ignore-this: 74093c60b0209f923ac45d35f2fd9c0 ] hash: 0000000470-bb7b619ef06a4c651ef09e148f0444f417e4232dc8f241fb8afb462d7474681c [Turned _⇨_ into a data type with the constructors return and Λ. Nils Anders Danielsson **20091130171248 Ignore-this: 10f167b1e081a4c0cbab04a4f49a1cb4 + This made some proofs more complicated, because less evaluation takes place. However, the definition of _>>=_ is nicer. ] hash: 0000013988-301e62e36eb8c78564c87a701f1760424cf0e554692c1bf3a359af402265a180 [Added Everything. Nils Anders Danielsson **20101115131901 Ignore-this: 56416cba006080642af1baecc88d0677 ] hash: 0000000729-3240197cf0aed2a11ad1e09a7b1b6b36ec38067dbbf4324b2a16b2dfc686eea5 [Updated code to reflect changes to library API. Nils Anders Danielsson **20101115131618 Ignore-this: 3c7a68d5595ace955aa2e9f7cfa8a45e ] hash: 0000008698-acdbbc1a0787ca7f18f1e9e79f1b45a033828e0119280f06b90b3600b411253f [Added some uses of --no-termination-check. Nils Anders Danielsson **20101115132442 Ignore-this: bf392c51d5e2dd31a4b5467e4d2d7a2b ] hash: 0000000618-828ffd725969ba1a65b3bb7fec2735ad2e7d5484ba1b1db466eaa1e4753c5fa1 [Simplified ReverseComposition.≈-Reasoning. Nils Anders Danielsson **20101117133348 Ignore-this: e63cde7dfd71fa986f99418985f40bd7 ] hash: 0000002261-67faa5aa49ad3fe218e7389d88c58eb56dbe87b98cd98ca6a2dae223345042ff [Rearranged the code. Nils Anders Danielsson **20101117135042 Ignore-this: 62881472d7af291f4780937271e99452 ] hash: 0000001657-a9f71768d6a6290aaf5455c077e9749d8dd885a200a8761a63d73e6fc97ac8c8 [Tried to turn _⇨_ into a kind of monad transformer. Nils Anders Danielsson **20101119142025 Ignore-this: e8afc18c2df0edc9eef5bb3ec0bcaa2f ] hash: 0000019065-58feab957d2d7a18e016848c74b31d06e2ade887bf335cd69f8a644c1219d0e3 [Rolled back "Tried to turn _⇨_ into a kind of monad transformer". Nils Anders Danielsson **20101119142048 Ignore-this: 7d55396c35e5499eaecef6ee6286df8b ] hash: 0000019079-c82d2ad87677747776c57d6321b33bf7f97aabd8917c1cf5c057e03ca6b167a6 [Changed the type of the proof constructor return. Nils Anders Danielsson **20101119150324 Ignore-this: 854c7280d3de71312f0fdc98a7a67c15 ] hash: 0000001518-746d57c3a58192169d3e7a12b29e9840f556ddabea6b84aef046b309f68039e6 [Made the code universe-polymorphic. Nils Anders Danielsson **20101119151346 Ignore-this: 6d8e331aedb90136aa4799a21b4f946d ] hash: 0000007214-50f7746f45b5ed5fe8a64dd70a219bc926c84af44a50ca8ce551f64d969febca [Proved that _⇨_ has a second monadic structure. Nils Anders Danielsson **20101119194512 Ignore-this: d8bb31b113d7dcb313ee6f85cd182c09 ] hash: 0000009061-ba1b9f93d515a39376e49dc9e34f9819957edc348acdc471ebd27429715c22d7 [Defined a specialised variant of _⇨_. Nils Anders Danielsson **20101119194543 Ignore-this: 3010746d7162d03e8b041a301746bed0 ] hash: 0000004716-c3fed6f61b84d5e8ed2fc9377a638ca7f5998ca294dd19bd40302388eae5a2a3 [Replaced _↑_ with _↑_⇨_. Nils Anders Danielsson **20101122225458 Ignore-this: a45024d312099b295e2e89046ad706dd ] hash: 0000001824-54e316f6a81997d0fc04f11a560163e62a6b6d0bc4e0f004dd0b6fa9b677b1b6 [Further work on the ReverseComposition theory. Nils Anders Danielsson **20101123005422 Ignore-this: f7e4cc16120e4199614629af6eb9e540 ] hash: 0000010776-f1ed4039e0e296b603e6b744533fc0bbf0f87151028dce8aad36d4059fa17ccb [Derivation of virtual machine and compiler for a language with exceptions. Nils Anders Danielsson **20101123012630 Ignore-this: 143da98d41cb2c5d6e7ceae28e3a30d4 + Based on a (slightly buggy) derivation Graham and I performed on whiteboards. ] hash: 0000015787-e94de12bbf32edd5c9dc99d45df6cdab6d01f043c95320013ea5fe48e1a231eb [Defined something which could be the free annotated monad. Nils Anders Danielsson **20101124183902 Ignore-this: 38e0e555c084f31c7c134075a883fc56 + Over a sequence of functors. ] hash: 0000004424-86f7ff1e43b0fb4568436ae18546e7afcd8caed8304dfcfe630dd058b73b80f9 [Mentioned free monads. Nils Anders Danielsson **20101124183923 Ignore-this: 28b236e2281866aa73201bb09f96a95a ] hash: 0000000277-e3274bde1474145ecc88799a5d1e796365b6882b62e5ec260a7d6138bf8c95fd [A simple language with exceptions and non-determinism. Nils Anders Danielsson **20101210173848 Ignore-this: d246a40ba69ad53a01dc2c34d857ad2f ] hash: 0000002042-cb1def63f77ce5d665ebeca0742a45460a409d0a2b16d8f7d19047c37c9b9da8 [A monad with non-determinism and failure. Nils Anders Danielsson **20101210173852 Ignore-this: ce4ea07d131b36558030d3a45ad6fdf4 ] hash: 0000004844-2bfc0043045c5e65ba81f7fbbf97e6d173fd91418d835132e4812f191a6977a0 [Added curry and uncurry. Nils Anders Danielsson **20101210173923 Ignore-this: 3f9c5dba8c9be16ab950bd3d88acfc56 ] hash: 0000006564-8f7270f1873c4b573a5f431a6dc9ba421f6481fa226c3d6e6ac960a425ceecf9 [Added map-⊙. Nils Anders Danielsson **20101210173939 Ignore-this: aaf3983bc4a0f2fb21dca37ac043fe94 ] hash: 0000001138-7a997787fcb76a597db8990d11b58eb1865da5b17e5b74f0dc78d386f2c9fce6 [Made _⇨_ smaller and enabled η-equality for it. Nils Anders Danielsson **20101210193153 Ignore-this: 4b689c566412af546253a1ded8def24 + Took the opportunity to change the definition of _>>=∥_. ] hash: 0000021517-f54f05d598c5f014699ac5f2473a01204489b327efd4a361c426cf1680fd6188 [Renamed ! to run. Nils Anders Danielsson **20101210193647 Ignore-this: aa20f2edf4c56638bcb5e4ee31c13cac ] hash: 0000003041-106fabcadcd03b8305e7c411d35e8af3af348450a7a9939bac7228596849b144 [An incomplete derivation of a compiler for a simple λ-calculus. Nils Anders Danielsson **20101210201509 Ignore-this: 52f54abd00db2f8eda16d29336f3b0a1 ] hash: 0000009829-28912e385e77013c4b7a89583d622273e69c8a7d4a0777ea096722356ad897d0 [Added map->>=∥ and some applicative functor laws. Nils Anders Danielsson **20101211120642 Ignore-this: 19b315ba7dfe7c4717a14fccfb052140 ] hash: 0000003806-5ba5672ce152ebb21edbced5648e7a5d44e27ad9a10c073d6ad1ab9b254c6fbe [Tried using _⊛∥_ for the accumulator composition. Still stuck. Nils Anders Danielsson **20101211122538 Ignore-this: 41b4ad6a663b464af058e6f9eca6dd59 ] hash: 0000008257-f7b08ca9d281219e36e767cd65fc84f232927250f8d733ba04859a2f43c6f63e [Changed the type of run-cong. Nils Anders Danielsson **20101211170246 Ignore-this: e3ef1247bf09fa0c2bc532c9890f0f8a ] hash: 0000002415-4e7116523ab26ba3d1fb80985e4ed58282cf0381519199c824405cc622b07132 [Found a way to rewrite the evaluator in "accumulator" style. Nils Anders Danielsson **20101211171210 Ignore-this: d3a1baca37d2adf1a348de7ccfa6f75a ] hash: 0000014022-8a831b2678305577f8a163364219f75ff93e57aaf5e9a39df5aae10d459faad3 [Simplified things. Identified a problem. Nils Anders Danielsson **20101211175728 Ignore-this: 3bdb2a1077ac4afc5b53334b77ca4690 ] hash: 0000013168-7d6c0b658b9814144ea0d0f625e4b9e11cdccebbb46d71439c25c81cb95890af [Simplified a proof. Nils Anders Danielsson **20101216133245 Ignore-this: 9c5b488e9e241d211eeccc3f9ed14df4 ] hash: 0000000465-93f0a131c864c398ffba3116ef3d04b29e51a180f0aafe3e8ac0bfccda4e5d62 [Added _⊙∥_ and identity∥. Nils Anders Danielsson **20101216133341 Ignore-this: bbebadf842d83d36c44451f1966d2e56 ] hash: 0000001286-2d5189d0a53756579bb53446cfaea2aa5be77641ae8b3f7802508b2db41a7adc [Some proofs related to map. Nils Anders Danielsson **20101216133418 Ignore-this: f19482a4573252780d01ec1129f5eb75 ] hash: 0000003254-16ba95793150b00492aeaac193727a861ef1359cccde9ff017efba7abe782a52 [Added some combinators which manipulate the "stack" of arguments. Nils Anders Danielsson **20101216163215 Ignore-this: ec329f09f53ecb94459e9c732ca3a46b ] hash: 0000006344-965e79e6904586ac6048747c1ae1742f0f12a7ef08d278e6eeb77255d94cd069 [Tried to use _⊙∥_ as the composition operation. Nils Anders Danielsson **20101216163954 Ignore-this: d4b4a345637e3833d12a1a62c44eb1e ] hash: 0000008121-9b669f56a9ef5df21b54812133e2ebdff566471dcc76e8fac76c6f876a25dca4 [Generalised some lemmas. Nils Anders Danielsson **20101216223808 Ignore-this: 6d3b28e6d87742b1af074d2d7e5d13b0 ] hash: 0000000921-63821965e3c7553bef0b0d3afcfbde176cd5bb634c107ef358525d2139a6f853 [Casts. Nils Anders Danielsson **20101217213505 Ignore-this: f1faccef039e7b6b4bda07ebba2e05b3 ] hash: 0000000556-a305cf09dd8f3062c7e209dad5b6c879abfdab161eced5f80362e83626274cba [Added a comment. Nils Anders Danielsson **20101217213513 Ignore-this: dd906ce28d504588f54c9ae78cc10afe ] hash: 0000000312-b304a501491d883a02f08ba15b47994b5acef0bf57760a8d2ed59155e54217a6 [Proved various laws for const⋆. Nils Anders Danielsson **20101217213659 Ignore-this: ce180baedd47bf7d9e463a93c8bbe311 ] hash: 0000003160-403ab08d1f142e0ec22841c4eb75daeabd93fa55d3534dbf0e25e7298170f48f [Tried using some kind of Kripke-variant of _⊙∥_. Nils Anders Danielsson **20101217215358 Ignore-this: 1049f47b883390f731a6e9518bc28ef6 ] hash: 0000014021-9a187327bed570d6f5a35543f1ece4f403ba3d403f5469c7ac3d4caa015f8ac6 [Tried to separate the environment and the stack. Nils Anders Danielsson **20101220121504 Ignore-this: 55fae5ba7357ad0d3fb0e5899442b544 ] hash: 0000002993-9c8bc874a1ed4ae132322b5eb73971c2350f3f3d355429da9867b2b7bcd26d1d [Added join and split. Nils Anders Danielsson **20101220164503 Ignore-this: f2ebf8f08742b4b74f445ff3de309007 ] hash: 0000001006-05eab565dc232d7387162a07b0d32a5a7a9ecb1732940672e5c81e40ddab579a [Modified the "Kripke"-approach. Nils Anders Danielsson **20101220170727 Ignore-this: c554455fa1dfdcd643fd1b7e3391acca + I realised that this approach is very close to the one which separates the environment and the stack. ] hash: 0000017205-0909c9d5ce2753251da88f07f8fb3dbc03634a52a2a948621117a5d415ca4720 [Replaced calculated lookup functions with simpler ones. Nils Anders Danielsson **20101220170739 Ignore-this: 2249827b2473ee03dd8edd14f36d1c48 ] hash: 0000005493-280ae51cce739011dd6110825e6e724665c57997dc7cf70174cc974be8406637 [Made the separation of the stack and the environment more obvious. Nils Anders Danielsson **20101220191930 Ignore-this: 1542b47af89d33e8c7f0be10e744bd4 ] hash: 0000008240-17f775827893866c0b5ce08c72eef9446a2db77e3a5148f066889f5b68aac959 [Defunctionalised and switched to an explicit environment. Nils Anders Danielsson **20101220202403 Ignore-this: d4cb538204768c8328294691c5359c4b ] hash: 0000008741-4ab79d46d9ca2172b0622946bcebc58d4ed190a3a1485a637b132277c58149c1 [Stopped using ReverseComposition. Simplified the code considerably. Nils Anders Danielsson **20101220233224 Ignore-this: 9213272da68b3eedb3337a1291f13894 ] hash: 0000025249-656816d503d2a57e48d718853703363c3cf27784f72ef90c9b74d10bbd230be6 [Updated some code to match changes in an imported library. Nils Anders Danielsson **20101220234824 Ignore-this: 3fd1d4209fe1573f970f0572e548e298 ] hash: 0000000460-accf60d0e4fe0f982bda0a09e1b63034bba565407ad01d86681a7496b9e27cde [Added/generalised some functions related to context interpretations. Nils Anders Danielsson **20101221193105 Ignore-this: 4e4dcba5f4023968de43835f0e7a5fd9 ] hash: 0000005406-79d5ed569bd7e4a95db6da8b61959687c14caf92ed1b3e04a0c57e8fda3f9886 [Added a .agda-lib file. Nils Anders Danielsson **20161208100615 Ignore-this: b0a7214b659d70dd0f7e1b40d5ebe417 ] hash: 0000000262-740ed0f642cbd5ee52d450cf751b72fe0ef4522a2b655d80105481063e2f6ce4 [Made the code build using recent versions of its dependencies. Nils Anders Danielsson **20161208102317 Ignore-this: 9c1daa1f0d62e146197fb1724ac7c55e ] hash: 0000002464-612fce0b111549b2f8a5c6e034e028460762efe2665316ca6b3cdf2351ebaf6f