[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