Mon Sep 6 12:22:19 BST 2010 jeanphilippe.bernardy@gmail.com * Documentation updates in the parser. Mostly: * Ids are now separated by spaces in the binders. * Also remove some nonsense. New patches: [Documentation updates in the parser. jeanphilippe.bernardy@gmail.com**20100906112219 Mostly: * Ids are now separated by spaces in the binders. * Also remove some nonsense. ] hunk ./src/full/Agda/Syntax/Concrete.hs 124 -- | A telescope is a sequence of typed bindings. Bound variables are in scope --- in later types. Or it's the mysterious Thierry-function-telescope. Only it's not. +-- in later types. type Telescope = [TypedBindings] hunk ./src/full/Agda/Syntax/Concrete.hs 126 --- data Telescope = TeleBind [TypedBindings] --- | TeleFun Telescope Telescope --- deriving (Typeable, Data) - {-| Left hand sides can be written in infix style. For example: hunk ./src/full/Agda/Syntax/Parser/Parser.y 301 | '{' SpaceIds '}' HiddenIds { map ((,) Hidden) $2 ++ $4 } | '{' SpaceIds '}' { map ((,) Hidden) $2 } --- Qualified operators are treated as identifiers, i.e. they have to be back --- quoted to appear infix. QId :: { QName } QId : q_id {% mkQName $1 } | Id { QName $1 } hunk ./src/full/Agda/Syntax/Parser/Parser.y 324 : BId SpaceBIds { $1 : $2 } | BId { [$1] } --- Comma separated list of binding identifiers. Used in dependent --- function spaces: (x,y,z : Nat) -> ... +-- Space-separated list of binding identifiers. Used in dependent +-- function spaces: (x y z : Nat) -> ... +-- (Used to be comma-separated; hence the name) +-- QUESTION: Should this be replaced by SpaceBIds above? CommaBIds :: { [Name] } CommaBIds : Application {% let getName (Ident (QName x)) = Just x hunk ./src/full/Agda/Syntax/Parser/Parser.y 462 | TypedBindings { [$1] } --- A typed binding is either (x1,..,xn:A;..;y1,..,ym:B) or {x1,..,xn:A;..;y1,..,ym:B}. +-- A typed binding is either (x1 .. xn:A;..;y1 .. ym:B) or {x1 .. xn:A;..;y1 .. ym:B}. TypedBindings :: { TypedBindings } TypedBindings : '(' TBinds ')' { TypedBindings (fuseRange $1 $3) NotHidden $2 } hunk ./src/full/Agda/Syntax/Parser/Parser.y 480 | Expr { [TNoBind $1] } --- x1,..,xn:A +-- x1 .. xn:A TBind :: { TypedBinding } TBind : CommaBIds ':' Expr { TBind (fuseRange $1 $3) (map mkBoundName_ $1) $3 } hunk ./src/full/Agda/Syntax/Parser/Parser.y 584 ImportName : Id { ImportedName $1 } | 'module' Id { ImportedModule $2 } +-- Actually semi-colon separated CommaImportNames :: { [ImportedName] } CommaImportNames : {- empty -} { [] } hunk ./src/full/Agda/Syntax/Parser/Parser.y 954 ParseOk _ (TokId _) -> return () _ -> fail $ "in the name " ++ s ++ ", the part " ++ x ++ " is not valid" - -- we know that there aren't two Ids in a row + -- we know that there are no two Ids in a row alternating (Hole : Hole : _) = False alternating (_ : xs) = alternating xs alternating [] = True Context: [Disallowed all user-defined pattern matching on codata (part 2). Nils Anders Danielsson **20100905214602 Ignore-this: f95b754feddafdc73245cac485e2413b ] [Disallowed all user-defined pattern matching on codata. Nils Anders Danielsson **20100905211039 Ignore-this: 5625296f613b5d7c7dc21c58172caeb3 ] [Removed recursive reference. Nils Anders Danielsson **20100905204207 Ignore-this: 601ee5630b6ab072dd2699ef432a575b ] [Removed the codata keyword. Nils Anders Danielsson **20100905203533 Ignore-this: 9714f41408855fd997b30e375e3a3de5 ] [Removed trailing whitespace. Nils Anders Danielsson **20100905203248 Ignore-this: a4d08f5e7219d5f813c1ebc3e9f01c24 ] [Removed Alonzo. Nils Anders Danielsson **20100905171625 Ignore-this: e8e363a872a2c2118a21d733520b00de ] [Replaced error call with __IMPOSSIBLE__. Nils Anders Danielsson **20100905202430 Ignore-this: 5e884fc207d93d2235cda7c1889f9043 ] [Tried to document the naming scheme used by MAlonzo. Nils Anders Danielsson **20100905202413 Ignore-this: 45e871656ccef0aefa46f200fc79f45f ] [Reduced the amount of duplication in the output of hTags. Nils Anders Danielsson **20100905171050 Ignore-this: d7b0d3077ebb72c5690f996dc903a36e ] [Made "make TAGS" work. Nils Anders Danielsson **20100905165147 Ignore-this: 9d8d26490b1f494974c6fd9b5da0d392 ] [updated error messages in test/fail ulfn@chalmers.se**20100903164527 Ignore-this: 91d8e43dba3ad2b13496abcf455ffea2 ] [updated monad benchmark to work with the latest version of the standard library ulfn@chalmers.se**20100903164415 Ignore-this: 95ea75f3c16325209860a1b473cb3d4d ] [Forgot to update a test case. Nils Anders Danielsson **20100903161722 Ignore-this: 4bf4de87b62881d94d588def4b6326b6 ] [don't normalise types before forcing analysis ulfn@chalmers.se**20100903160658 Ignore-this: 5cbfc68b1b8b9273de07078b8ad2ddd3 ] [fixed a bug with forcing ulfn@chalmers.se**20100903151151 Ignore-this: b2ba5eb8241add171f35b07d945b22ec ] [forcing optimisation also for functions ulfn@chalmers.se**20100903144151 Ignore-this: 83dbe53ff2b05361136af1890053be97 ] [implemented forcing optimisation for constructors ulfn@chalmers.se**20100903133017 Ignore-this: 534f7000c3f3c6fcbc34b3e9587256e6 ] [started on forcing optimization ulfn@chalmers.se**20100903105918 Ignore-this: 90f87c6d3ddd12cac8b77c027476a34a ] [Updated the tested-with field. Nils Anders Danielsson **20100903105116 Ignore-this: 4adb93254e42777d3e14c235c19a77a8 ] ["Have: ..." is now also displayed before the context. Nils Anders Danielsson **20100902152728 Ignore-this: bd83a9519266b6afcfc81924f000f135 ] [Added a comment to the Relevance data type. andreas.abel@ifi.lmu.de**20100903104352] [File in test/bugs/ which documents the scope violation with the size inference (Warshall). andreas.abel@ifi.lmu.de**20100903100521] [Made some things boring. Nils Anders Danielsson **20100903095912 Ignore-this: ecab5a0fc9ed2863c36a375ad2d0d045 ] [Fixed Makefile problem: compiled modules were ignored on subsequent runs. Nils Anders Danielsson **20100903095801 Ignore-this: 90dd39fee964a40507452ae0d1b6fbba ] [Fixed a bug exposed by the fix for issue 274. Nils Anders Danielsson **20100903095626 Ignore-this: 922d4d58eee394d458de20c8ecc0d453 + Done together with Ulf. ] [preparations for improved universe polymorphism ulfn@chalmers.se**20100903094851 Ignore-this: b0b20f93ae3ebb6bd20e4d23abbb2946 ] [In preparation for irrelevance depessimization, added an extra argument to the Arg data type in Syntax/Common.hs. This affects next to ALL modules. andreas.abel@ifi.lmu.de**20100903093732] [Fixed issue 274 (hopefully). Nils Anders Danielsson **20100902161134 Ignore-this: 26fbf227f3c1f05dbd87486bfbe46814 ] [removed sudo command from make install ulfn@chalmers.se**20100902162123 Ignore-this: f62f2444d185ec92b12d07dd18378c3a ] [Some error messages were changed by Makoto's recent patch. Nils Anders Danielsson **20100902162134 Ignore-this: 9ab0ae937776041dc45e74fa13359388 ] [abstractToConcrete-improvement-2 makoto.takeyama@aist.go.jp**20100902104446 Ignore-this: 491e0dcd88966c367d9ae5504790262d ] [Fixed issue 296. Nils Anders Danielsson **20100902105026 Ignore-this: d8ee71a05c7ada9c079680d4f73a4da1 ] [.flags files can now be used under test/succeed. Nils Anders Danielsson **20100902104554 Ignore-this: 66a2aab7f572b306995f78ac059aa68f ] [fixed testcase Issue298 again andreas.abel@ifi.lmu.de**20100902094511] [corrected module name in Issue298.agda andreas.abel@ifi.lmu.de**20100902094311] [test case for issue 298 (sized types bug) andreas.abel@ifi.lmu.de**20100902093953] [The goal is now displayed before the context. Nils Anders Danielsson **20100901125714 Ignore-this: c9ad26ee743d0b26682aa37e7876e0c7 ] [Cabal is the preferred way to install Agda jeanphilippe.bernardy@gmail.com**20100903152119] [Sized Types sizeSuc is now injective. andreas.abel@ifi.lmu.de**20100901122721] [Merged conflicting changes (both Ulf and I fixed issue 246). Nils Anders Danielsson **20100720105953 Ignore-this: e114dd55695978b74dd08574528258d8 ] [Fixed issue 246. Nils Anders Danielsson **20100720100732 Ignore-this: 1514a7e54ef5c99b1a4b092408b67580 ] [The pretty-printer seems to have changed. Nils Anders Danielsson **20100720084030 Ignore-this: 37c442b2e86f4721502a6ac7a18091df ] [fixed issue 246: recursive functions mistakingly thought to be invertible ulfn@chalmers.se**20100720101738 Ignore-this: f5744fa21c21ed973ab368de537dad37 ] [updated changed output from interactive test ulfn@chalmers.se**20100720090613 Ignore-this: bf6cc9c1ce7fd9822ea3c712c49f9001 ] [Fix: Vim highlighting: repeated constructor names no longer overlooked. Daniel Brown **20100717064314 Ignore-this: 6da99d7ec766d69c3332ec51770c0c2f ] [improved some pretty printing ulfn@chalmers.se**20100719103804 Ignore-this: 5ffb8ad933bd100ed6e8fd36a12f0797 ] [made the definition of a record type available in the record module ulfn@chalmers.se**20100719103418 Ignore-this: 2653144f58575bf2114f92eebf928d52 - you can now define things like record R : Set where field x : Bool op : R op = record { x = not x } ] [added -v0 when checking examples ulfn@chalmers.se**20100712120234 Ignore-this: 22ff78ed80ca280e06e8b425548298c ] [compile clauses for more efficient evaluation ulfn@chalmers.se**20100712115851 Ignore-this: efb78126b5cb14b5e015bf8b02c33a3c ] [fixed issue with superfluous parentheses in goal types ulfn@chalmers.se**20100711103737 Ignore-this: ed387641d6dee67fd0e529370a4a4a7d ] [fixed bug with printing of metavariable types ulfn@chalmers.se**20100711102310 Ignore-this: ef9c9f7394e5f2ded5f1b9900a9652f1 ] [nat literals are now reflected in constructor form (instead of as 'unknown') ulfn@chalmers.se**20100709195610 Ignore-this: c9f768ced7d4858ae31639b6211c4593 ] [occurs check will now remove conflicting flexible variables (when possible) ulfn@chalmers.se**20100629192521 Ignore-this: 8db67c7c679e3f9e31d4ef2143b1b616 - for instance, if we're trying to instantiate _1 := suc (_2 x) rather than postponing (since _1 can't depend on x) we'll instantiate _2 := \_ -> _3 for a fresh meta _3, which lets us do the originial instantiation _1 := suc _3 ] [replaced (!!) with an __IMPOSSIBLE__'d version ulfn@chalmers.se**20100629192437 Ignore-this: de8fe805828b4147e3cfc3d449da707e ] [added missing error message for failing test and minor fixes ulfn@chalmers.se**20100629192239 Ignore-this: 245905acd37d838148dc9526cd0ebbfd ] [removed broken tags target from make default ulfn@chalmers.se**20100629192153 Ignore-this: f71ad67a967669f8568cae32c2853552 ] [fixed a bug in sort constraint solving ulfn@chalmers.se**20100629192111 Ignore-this: a72c628761950f6eed293594ca2f70e8 ] [some debug printing ulfn@chalmers.se**20100624100812 Ignore-this: b3c21ba095d43ec2eb60b128f25957d9 ] [started looking at 243, requires rethinking display forms (need to remember dots) ulfn@chalmers.se**20100604160323 Ignore-this: dacd738a077b014717bf0d28a363b1f4 ] [Fixed an Emacs mode bug. Nils Anders Danielsson **20100709222654 Ignore-this: 2cdfcb1c7b621faed7fbfc755ae04fcf + If code was "give"n from the minibuffer, then the goal was replaced with whitespace. ] [Improved a comment. Nils Anders Danielsson **20100612174604 Ignore-this: 26e1a65cc651e2e57a836952824e957a ] [abstractToConcrete_improvement makoto.takeyama@aist.go.jp**20100621012400 Ignore-this: 583875e5000834b6acf05ffb003d9217 ] [Set no longer preserves guardedness. Nils Anders Danielsson **20100608131911 Ignore-this: e8d101172d3ead3ee9fe4226e87bd9ea ] [release notes 2.2.8 for --termination-depth andreas.abel@ifi.lmu.de**20100519141629 Ignore-this: 1ff564a8e0172650e0dc49651c1e7cf9 ] [test case for issue 166 andreas.abel@ifi.lmu.de**20100519130944 Ignore-this: 124d9b2ca45c2e4fbb0c84fbf5a325c9 ] [test case for issue 166 andreas.abel@ifi.lmu.de**20100519130743 Ignore-this: 529766e38c0d2ef6044bc259fcdbaf2d ] [Termination checking sort expressions. andreas.abel@ifi.lmu.de**20100518155619 Ignore-this: d536940844041acb776956a04399b06e ] [{-# IMPORT -#}s are qualified by the compiler again. Nils Anders Danielsson **20100607150510 Ignore-this: 20d04319f334bbf3b65858aee6ccffbb + Reason: Imported constructors which are named in COMPILED_DATA directives may be used in other files, and with qualified imports we ensure that the constructors can be disambiguated, even if other (homonymous) constructors are also in scope. ] [Fixed issue 264 (missing parentheses for quote). Nils Anders Danielsson **20100604162031 Ignore-this: 32b5a75411f88ce0b36318161085294d ] [Removed outdated statement. Nils Anders Danielsson **20100604154034 Ignore-this: 9b46801fa707485feda61c3407e62ac7 ] [CABAL_OPTIONS can now be used to override our default options. Nils Anders Danielsson **20100604153949 Ignore-this: 180d5ba36a476ec3cd70b70deab76307 ] [bumped interface version ulfn@chalmers.se**20100604133009 Ignore-this: 4dd9111fe6a9e2060324dac536558d48 ] [fixed issue 277: abstract ignored at top-level evaluation ulfn@chalmers.se**20100604132916 Ignore-this: b2280594b6e0375eb430bcbd5f6d2ae8 ] [-v is a pragma option again ulfn@chalmers.se**20100604130231 Ignore-this: 8f5597086ad17b9ca53d43bb0030ccc9 + It might be misleading to allow it, but it's still really useful when debugging interactive commands. ] [issue 237: with applications generated by 'rewrite' ulfn@chalmers.se**20100604110210 Ignore-this: baddc489c16e3871740f2ee8411e65d0 ] [line number change for impossible test case ulfn@chalmers.se**20100604105110 Ignore-this: 2903520979ab085b0699023a2fc6d5a9 ] [the default for 'make install-lib' should be to build without profiling ulfn@chalmers.se**20100604104508 Ignore-this: 98ba160be310dc21acbb203c107ce443 (ignoring ~/.cabal/config) use 'cabal install' if you want the .cabal default ] [dist directories are boring ulfn@chalmers.se**20100604104449 Ignore-this: 61cd4c310a0b84973f046b67b8ffb09b ] [fixed second part of issue 263: datatype modules not added as sections ulfn@chalmers.se**20100604104415 Ignore-this: 865734a7fcf1b20a64c8658156d51818 ] [test case for issue 263 ulfn@chalmers.se**20100604104127 Ignore-this: e77dc417b891524a3e9cc0ef3de4ee9c ] [fixed issue 263 (first problem): module instantiation generating too fresh names ulfn@chalmers.se**20100604103843 Ignore-this: dda54f9dde2b1f63e3337b848d3f2475 ] [{-# IMPORT -#}s should not be qualified by the compiler ulfn@chalmers.se**20100421103148 Ignore-this: bd4d248e510d720830b4d5af73f2a13c ] [Fixed issue 275 plus some small things frelindb@chalmers.se**20100601083220 Ignore-this: d47d2a20b0c78febdea6a8a11b917255 ] [Reduced code duplication. Nils Anders Danielsson **20100520151718 Ignore-this: 87199a42f7369c32e8e741b710d0291a ] [Added some interaction tests for Auto Fredrik Lindblad **20100518144917 Ignore-this: 6fe0531622d9ee950c25be8ee847236a ] [Made some import statements referring to Data.Generics more precise. Nils Anders Danielsson **20100511181121 Ignore-this: df2bc57ef08b064f6bd7c49de32eacb ] [Removed some unused Eq instances. Nils Anders Danielsson **20100511162428 Ignore-this: f17a7684dc7b800cff1571a841750605 + These instances were "incorrect" anyway, because they involved comparison of ranges. ] [Fixed bug: Paths pointing to non-existing files were sometimes truncated. Nils Anders Danielsson **20100506225548 Ignore-this: 17101cae07188bc99f6ef2a873e25d79 ] [Update of auto/agsy containing a bunch of bug-fixes and new features frelindb@chalmers.se**20100508123709 Ignore-this: dcca435ae69558e2a18db96fbee86fe7 + Bug-fixes include issues 257 and 266 + Basic equality reasoning + Auto refine (suggest) + Recursive calls in normal mode (not only case-split) ] [Fixed bug: Premature attempt to open non-existing file. Nils Anders Danielsson **20100506204949 Ignore-this: 6775f308284baf00b3336d71b40f4bac + The Emacs mode complained when a buffer with a non-existing associated file was created. ] [Fixed typo. Nils Anders Danielsson **20100505172450 Ignore-this: 6b59ce56759876eea047bc862e48d9c9 ] [Added a flag which enables compilation of agda-pkg. Nils Anders Danielsson **20100505104347 Ignore-this: f762fd1b930883df52af7a6faabeadee ] [The interaction test suite now tests all the main commands. Nils Anders Danielsson **20100505100429 Ignore-this: 8d2920e8033f7a7e768135bf035058b9 + The tests could be made more exhaustive, though. ] [All independent interactions now set the include path. Nils Anders Danielsson **20100504140856 Ignore-this: 61cef76979d73e4c0019344464cd0b43 + Removed cmd_reset. ] [Simplified the communication between the Emacs UI and the backend. Nils Anders Danielsson **20100504140700 Ignore-this: 3436aa32327b5422ad0731ad146c0e65 + Removed cmd_goals. + Updated the interaction test framework. ] [We now keep better track of include dir status (relative/absolute). Nils Anders Danielsson **20100503144932 Ignore-this: 614e97ad77ad0922bcea186b82268149 ] [Replaced use of the extensions field with LANGUAGE pragmas. Nils Anders Danielsson **20100504183841 Ignore-this: ce70aea28679f946d5be1c520de7c71a ] [Merged the agda-pkg package with the Agda package. Nils Anders Danielsson **20100504183400 Ignore-this: bd9d9c91e9ddb9dc6ed106cecbc36725 + Currently agda-pkg is disabled (buildable: False). ] [-v is no longer a pragma option. Nils Anders Danielsson **20100430001924 Ignore-this: bcc33458da5f660b366e6b365e346693 + Allowing it in pragmas was misleading, because when a module was loaded it did not take effect until after some messages had already been handled. ] [Fixed a bug: OPTIONS pragmas were ignored for skipped files. Nils Anders Danielsson **20100430000310 Ignore-this: d42513c49469503d0d304c2b50c218d6 ] [Made the interaction test framework a bit more robust. Nils Anders Danielsson **20100430000244 Ignore-this: e02c1fb7169b06ed26fe089aa38b4e21 + Previously it mattered if "Checking" or "Skipping" was printed. Now all debug messages are suppressed. ] [Added a separate type for options which can be set using pragmas. Nils Anders Danielsson **20100429211051 Ignore-this: b8aaf410873a00a1be5282245644c934 ] [Submitted version of HCAR report. Nils Anders Danielsson **20100501232144 Ignore-this: f90aae961e0bfb2496f03c514bfdd181 ] [Ulf's description of test/interaction. Nils Anders Danielsson **20100429211615 Ignore-this: 3fb6c96082488c117903cace6c05ae9e ] [The cabal-version field is now identical in the three main packages. Nils Anders Danielsson **20100429154221 Ignore-this: b80ce600118dd288c7c1a50e0ea895c ] [Updated comment. Nils Anders Danielsson **20100429150355 Ignore-this: 70a8ffa0743a8496fa6c9520cbb3d603 ] [Initial draft of HCAR report for May 2010. Nils Anders Danielsson **20100430002022 Ignore-this: 4c523df374379050fcc6a10c0e67b169 ] [Added missing dependency. Nils Anders Danielsson **20100429151220 Ignore-this: ef5c45cf6c006684724975d369dd175c ] [We now require Cabal 1.8 or higher. Nils Anders Danielsson **20100428143529 Ignore-this: 71a1a64de97b9d59b1669d027f4364b6 + I failed to install Agda using Cabal 1.6.0.3. + I took the opportunity to simplify some code/instructions. I don't know whether these simplifications would have been correct if 1.6.0.3 were still supported. ] [Tried to clarify the installation instructions. Nils Anders Danielsson **20100428141501 Ignore-this: 4bf8ee98b362cad9c8294d82931e55f ] [Reverted some accidental (?) changes. Nils Anders Danielsson **20100423181603 Ignore-this: a8d1a59e7963b051ddf30ddbaf2b4f78 ] [Noted dependency on ncurses. Nils Anders Danielsson **20100423173225 Ignore-this: 4714884ba86915122060fecd70dbb795 ] [Removed the (partially broken) Ubuntu installation scripts. Nils Anders Danielsson **20100423172551 Ignore-this: 46f8cff207fd569ad1a4289e1361847 ] [There were two "prof" targets. Removed one. Nils Anders Danielsson **20100422150250 Ignore-this: 51ecb9f5cdc2a7338dc7806104e78aeb ] [Agda seems to work just as well with GHC 6.12.2 as with 6.12.1. Nils Anders Danielsson **20100422143937 Ignore-this: e9bf716b0b50691cc3db1bafb4206fab ] [Added "cabal update" to README and Makefile. Nils Anders Danielsson **20100419153629 Ignore-this: 30cb7dfc6aa2ff75f78afcbb7751780b ] [fixed issue 262 (qualified imported constructors) and some improvements on issue 260 ulfn@chalmers.se**20100419131356 Ignore-this: bf1bc292e7c688f4451c3012cae9cca1 - it's no longer allowed to define a datatype or record with the same name as an existing module, since datatypes and records also introduce modules and we don't allow module shadowing ] [Fixed a highlighting bug. Nils Anders Danielsson **20100414232724 Ignore-this: 8bd97fffa4a00cdfa4aa30dcd4060b0e + The module name "Bug" was highlighted as if it were a constructor: module Bug where record R : Set₁ where field A : Set ] [Updated the tested-with field. Nils Anders Danielsson **20100414232026 Ignore-this: 33fcbef8102f85450755c91ece83406e ] [minor tweaks to interaction testing ulfn@chalmers.se**20100413131050 Ignore-this: 80c2f377faef0637d8cd3422627ec515 ] [test framework for interactions ulfn@chalmers.se**20100413124313 Ignore-this: 9bf693ddf326286e82612241ef1e84c5 - 'make interaction' runs the interaction tests (also part of 'make test') - Each test consists of an agda file SomeTest.agda and a interaction script SomeTest.in. The interaction script contains interactions (as commands to ghci) that should be performed on the Agda file. - A simple example: top_command (cmd_goals currentFile) goal_command 0 (cmd_goal_type_context Normalised) "" goal_command 0 cmd_give "s z" goal_command 0 cmd_give "Nothing" The Agda file is loaded automatically before running the test script and the variable currentFile is bound to the current file name (needed by cmd_goals, for instance). - Two new functions have been added to Agda.Interaction.GhciTop for convenience: top_command :: Interaction -> IO () goal_command :: InteractionId -> GoalCommand -> String -> IO () - The default scope for the script is Agda.Interaction.GhciTop and Agda.Interaction.BasicOps, but more modules can be added with ':mod +Agda.Some.Other.Module'. - The ghci output from each test is recorded in SomeTest.out and compared against for each run of the test. ] [Made interface files more portable by replacing Int with Int32. Nils Anders Danielsson **20100412140140 Ignore-this: 9f286f0c7c5ed5c9ae948686005fa798 + We still store Doubles in interface files, and the Double type is not platform-independent. ] [issue 259 again ulfn@chalmers.se**20100409113542 Ignore-this: c5cd1cfdda644def46c2fafc09bb5b58 - It's not always safe to eta contract implicit lambdas when doing with abstraction, since f expands to \{x} -> f {_} when type checking and it's not always possible to infer that implicit argument. This is a problem for with abstraction since we re-type check the type of the generated with function. On the other hand, eta contraction is very useful in with abstractions since it allows more abstractions This seems to outweigh the potential problems caused by too aggressive eta contraction (in most cases the implicit argument to f can be inferred), so we choose to eta contract implicit lambdas rather than not. See test/fail/Issue259.agda for an example where this doesn't work. ] [another go at fixing issue 259 (should work now) ulfn@chalmers.se**20100408185506 Ignore-this: 55b6b916babf82b0dcea05fef1878ea0 ] [fixed issue 259 (for good this time?) ulfn@chalmers.se**20100408114530 Ignore-this: 7eadf3d17e6a96f3c16d8b7be9ff62cd - we want to eta contract implicit lambdas unless we're about to turn them back to abstract syntax for type checking (when there's a with) ] [fixed issue 259 (again), it's not safe to eta contract hidden lambdas ulfn@chalmers.se**20100408073343 Ignore-this: c339095e3f753703f69f7b56adf23de ] [fixed issue 258 (bug in with abstraction) ulfn@chalmers.se**20100407121809 Ignore-this: ffb17c8b83b1e3b6c42590aa8414026 ] [fixed issue 259 (eta contraction ignoring hiding) ulfn@chalmers.se**20100407093133 Ignore-this: 2bd8bf84a8e413b496c6509c0d388f51 ] [Minor changes. Nils Anders Danielsson **20100404091756 Ignore-this: 98339bccb609335165cbf4c1b8eda2d4 ] [Updated the description of --guardedness-preserving-type-constructors. Nils Anders Danielsson **20100404091712 Ignore-this: 76017399914f4576f7852f9af962985c ] [Fixed directive name in an error message. Andrés Sicard-Ramírez **20100402061517 Ignore-this: 48467bab938424abdae3a9f952277df3 ] [changed error message for a failing test ulfn@chalmers.se**20100401170437 Ignore-this: 3fdf4083a96b9fe70059419d416acc66 ] [updated a test case to new version of quote ulfn@chalmers.se**20100401111934 Ignore-this: d4295c65c019661d7e21b2208678b3bd ] [quote for variables only txa@cs.nott.ac.uk**20100331014641 quote will now only accept variables. test case is also updated. ] [fixed minor issue with qualified constructors ulfn@chalmers.se**20100401062230 Ignore-this: 1b717cc395540158d641535a0cc94e88 ] [wrote something about reflection in the release notes ulfn@chalmers.se**20100331012130 Ignore-this: 9f824a9c7b47dcb36886876bdcfb329c ] [fixed TestQuote example to work with the new agda term representation ulfn@chalmers.se**20100331010252 Ignore-this: 9b6ca75dc868a891b69ba2af4bc7ecc0 ] [some reformatting in release notes ulfn@chalmers.se**20100331010228 Ignore-this: 69bbbb9cd902e4d0a9867b8446eeeb38 ] [allow constructors to be qualified by their datatypes to resolved ambiguities ulfn@chalmers.se**20100331010154 Ignore-this: 3933df01303771c0dc3a2cb6ca16d242 - for instance, given natural numbers Nat with constructors zero and suc, you can now refer to the constructors as Nat.zero and Nat.suc if necessary to distinguish them from other constructors with the same names ] [more reflection test cases ulfn@chalmers.se**20100330133702 Ignore-this: dfee4b872519ab18770d7bb4266c88 ] [bumped interface version ulfn@chalmers.se**20100330114727 Ignore-this: 4c4fae503f05870efdab5e320c4cb273 ] [reflection with AgdaTerm txa@cs.nott.ac.uk**20100330092835 implemented AgdaTerm as a more convenient interface for reflection. Currently no type checking on the constructor is done. ] [darcs boring files ulfn@chalmers.se**20100330070842 Ignore-this: e16dc2cab6c5b2652eda81556e9e0124 ] [error messages for failing tests ulfn@chalmers.se**20100330070818 Ignore-this: 956a10095312ee110816294493bceb57 ] [smart constructor for matrix shaped orders (to avoid a potential bug) andreas.abel@ifi.lmu.de**20100330061653] [example for counting termination checker andreas.abel@ifi.lmu.de**20100330044821] [conflict resolution with Nisse's patch on guardedness preserving type constructors andreas.abel@ifi.lmu.de**20100330043120] [termination checker which can handle limited temporarily increase for linear datatypes like Nat and Size andreas.abel@ifi.lmu.de**20100330031138 Especially useful with sized types. Activated by flag --termination-depth=N. Internally, the order seminring (<,=,?) is replace by (Decr k, Unknown) for k bounded by N. Thus, foetus can count up to N. ] [testsuite-counting-terminator andreas.abel@ifi.lmu.de**20100128171327 Ignore-this: 76d8e06b0ddf04fe3334fce6bc6fd779 ] [termination checker counts, new option --termination-depth andreas.abel@ifi.lmu.de**20100128153929 Ignore-this: a675717017adb33cc17f8d9f3bdb7b4e ] [make positivity checker look inside patterns ulfn@chalmers.se**20100330043146 Ignore-this: 53ac5736ea21b17b4835001d6019774f ] [Testing relocatable now Mac OS compatible (use of shell commands in Makefile). andreas.abel@ifi.lmu.de**20100330030858] [Removed a source of inconsistency. Nils Anders Danielsson **20100329144512 Ignore-this: b3f38625286360c3b7de84b566b260d5 + The experimental feature --guardedness-preserving-type-constructors could be used to break the termination checker: D : Set D = Rec (♯ (D → D)) _·_ : D → D → D fold f · x = f x ω : D ω = fold (λ x → x · x) Ω : D Ω = ω · ω This was discovered by Thorsten, Ulf and me. We hope to have fixed this problem by only treating type constructors as preserving guardedness in those arguments which are used strictly positively (or not at all). ] [Fixed one part of issue 175. Nils Anders Danielsson **20100330025433 Ignore-this: a95977215af60c83a0004a661e237368 ] [added check for unsolved metas to quoteGoal (but not quote) ulfn@chalmers.se**20100329163018 Ignore-this: 5de17892c8a9e9f2d4f91dc67548419d ] [fixed issue 253 (impossible when using with and lots of level metas) ulfn@chalmers.se**20100329151957 Ignore-this: 6d40ac50400e6c5650b742d7105ace6c ] [fixed issue 242 (out of scope variable when using parameterised modules) ulfn@chalmers.se**20100329142359 Ignore-this: cadbfaf63ad7fb17d5a2058ee7b3073a ] [conflict resolution ulfn@chalmers.se**20100329131347 Ignore-this: c9f1b95ef482a0a57e89d4aa69b24094 ] [basic quotation txa@cs.nott.ac.uk**20100329130144 first version of reflection (quoteGoal, quote) with String as the internal representation of terms as a stop gap. ] [changed internal representation of record constructors ulfn@chalmers.se**20100329094206 Ignore-this: e15fbfdf03a931106432ca57d5189091 ] [records have eta equality again ulfn@chalmers.se**20100329083654 Ignore-this: a37e5166f2a69657f75692db3292ce34 ] [switched off eta for records by default (switched on by the pragma {-# ETA NameOfRecord #-}) ulfn@chalmers.se**20100329054119 Ignore-this: f1c4ecd1328c14e3e5b35f7a59c6eabc + just for experimental purposes ] [added support for records without eta internally ulfn@chalmers.se**20100329025225 Ignore-this: 275c52b6a42a30092c281d330e6f6717 ] [changed error to __IMPOSSIBLE__ ulfn@chalmers.se**20100329020506 Ignore-this: e925dff82ec67779ff11fda58270c1cb ] [Removed the binding \par → '
'. Nils Anders Danielsson **20100329144640 Ignore-this: 9f053d94ef52975ba6d227da635e5791 ] [Made → respect the --guardedness-preserving-type-constructors flag. Nils Anders Danielsson **20100329143356 Ignore-this: a7c7a7726ccff0d08d9758d1bb14929c ] [Another example which ought to type check faster. Nils Anders Danielsson **20100329064735 Ignore-this: 656e4d72714940c5f4b3369c1b57fe82 ] [Intermediate update of agsy Fredrik Lindblad **20100328211624 Ignore-this: 586cecbb74617583d32fc1836679a2f4 ] [fixed compiler problem for trustMe ulfn@chalmers.se**20100328125423 Ignore-this: 33f6df1aabb488872e57fddfaf311a98 ] [fixed issue 249 (allowed repeated names in renaming clauses) ulfn@chalmers.se**20100328125304 Ignore-this: 6b3513c7da9e74dc2333f1d742e167ea ] [fixed issue 248 (with abstraction doing the wrong thing for universe levels) ulfn@chalmers.se**20100328121911 Ignore-this: d8e960249e389c696c36a734f996c5b4 ] [fixed issue 251 (not so impossible partially applied record) ulfn@chalmers.se**20100328092419 Ignore-this: f9ef9b7de64f1cea8bc96a8638cf937 ] [fixed a bug with trustMe ulfn@chalmers.se**20100328084340 Ignore-this: 9cc4701e9dfbc38956c20a7889417add ] [made positivity checker aware of unused arguments ulfn@chalmers.se**20100328082329 Ignore-this: bc26acf4e3b96fdbb7991e174ac16d69 ] [fixed issue 252 (normalisation not happening properly before with abstraction) ulfn@chalmers.se**20100328073732 Ignore-this: c4a7ce3a3f06a5c7ee733e7246aee70c ] [fixed some bugs for eta expansion of metavariables ulfn@chalmers.se**20100326133712 Ignore-this: 56d6ce787c7d1fdbf1eb208a84fe3dbc ] [fixed issue245 (singleton record metavariable) ulfn@chalmers.se**20100326070057 Ignore-this: 18b4b492dcc8de4e1f0480ee1f4b069d ] [term representation prototyping ulfn@chalmers.se**20100326064355 Ignore-this: e11a18437ee61fe2e2244dc46d91f935 ] [do eta contraction when in instantiateFull ulfn@chalmers.se**20100326064228 Ignore-this: fb12c656d6ce0f7a1ebc46f8863b3f57 ] [don't print where clauses in error messages ulfn@chalmers.se**20100326064141 Ignore-this: 73f1ac2c7c0a29c6a6adca145c40f0de ] [Added --guardedness-preserving-type-constructors. Nils Anders Danielsson **20100326063830 Ignore-this: 2dcd0ae2d054fa14977648d318d2f9e ] [Fixed a bug: The intro command could not introduce the empty record. Nils Anders Danielsson **20100326054204 Ignore-this: 5b8c1d4ca6bf6edbed67b78fc3e98975 ] [UNDO: "Does it help to reload newly checked interfaces from disk?". Nils Anders Danielsson **20100325115255 Ignore-this: 36076013fd05f0f0371f1d2b5193c4d2 ] [Experiment: Does it help to reload newly checked interfaces from disk? Nils Anders Danielsson **20100325115141 Ignore-this: b5a5d48f89062c541fefb8acff5dead1 + Answer: No, at least not when checking the current version of the standard library. ] [Minor change. Nils Anders Danielsson **20100325114937 Ignore-this: 1c1ff47b72e74b6e604a9f8908b8c72d ] [Added Fredrik Lindblad to .authorspellings. Nils Anders Danielsson **20100324044146 Ignore-this: 24edf1e545872012959fb7bd7798a261 ] [ignore context precedence when printing errors ulfn@chalmers.se**20100325030518 Ignore-this: e1dee60077a94916e3fd712a214eb0e7 ] [dropped traces (Agda.Utils.Trace) since they were consuming a lot of memory ulfn@chalmers.se**20100325030409 Ignore-this: 8a100642732872630bb1014c8b601e ] [changed bad catchError_ back to catchError ulfn@chalmers.se**20100325000344 Ignore-this: 1237aff55cb14b709c9676c0b184b54e ] [make fresh strict (caused big memory leak) ulfn@chalmers.se**20100324160035 Ignore-this: 547e7fcbd4d68c29223d331cdc4d05f7 ] [rollback IORef state ulfn@chalmers.se**20100324160026 Ignore-this: 889aadec00db7955e4f348aed46c5ae ] [use IORef for the state ulfn@chalmers.se**20100324155841 Ignore-this: 3c91dcda18d8a3937afaab8ff9dfaa5d ] [don't use monad transformers in TCMT (and specialized catchError_) ulfn@chalmers.se**20100324151709 Ignore-this: 8a2be4084afe9d529843679530f639e8 ] [A new version of agsy with eg absurd lambda, case split and disproving Fredrik Lindblad **20100322163019 Ignore-this: e1ccdc948d12679c52fec646302c3465 ] [tried to make hTags run with ghc-6.12 (unsuccessfully) ulfn@chalmers.se**20100323134152 Ignore-this: 709473b0bbfaf002c3f4fe758aee2539 ] [boring files in agda-pkg ulfn@chalmers.se**20100323134030 Ignore-this: 399ddb0e7d3887141aa5e6bcef057671 ] [benchmark run ulfn@chalmers.se**20100323134006 Ignore-this: 47bddf5e608f38903251d0c3de65acae ] [left constructor type checking experiment for now ulfn@chalmers.se**20100323133802 Ignore-this: 7710fc9181b1000ce3e5bb42ac69efe7 ] [push types into constructor applications more aggressively ulfn@chalmers.se**20100115000224 Ignore-this: ae4b48464eed99d83d4414b770d3c5de ] [Made the .authorspellings file compatible with darcs 2.4. Nils Anders Danielsson **20100227193436 Ignore-this: 4a502d3f49c10b48e6eeb0ef4919b3fe ] [Removed unnecessary dependency on Data.Generics. Nils Anders Danielsson **20100216163722 Ignore-this: 1ca5e35ca3b96a66f2d51a7626cd0458 ] [Fixed a bug: symbolic links were not handled properly. Nils Anders Danielsson **20100213165457 Ignore-this: 8759f944dd309a056862498696642b41 + The bug could be triggered by defining A.M in A/M.agda, where A was symlinked to B. The problem was that some paths were canonicalised (this includes "normalising" symlinks), whereas others were not. ] [Modified a comment. Nils Anders Danielsson **20100213160913 Ignore-this: 4fbb19398d8ae26068b5489f3269951f ] [The "module contents" command no longer shows private names. Nils Anders Danielsson **20100209174552 Ignore-this: f775cd127c7afa37a55d767d4085a048 ] [Ported some parts other parts of the package handling code to the new format. Incomplete and untested. dwm@cs.nott.ac.uk**20100208174331 Ignore-this: d39e52135fa112382d45160af701a706 ] [Basic error handling dwm@cs.nott.ac.uk**20100208141041 Ignore-this: 9ae26deaf3ce0b28740c37b8e7e1a31e ] [Fix package DB reading to work with new DB format (Cabal >= 1.8.0.2 && GHC >= 6.12) dwm@cs.nott.ac.uk**20100208135726 Ignore-this: fb59e7041e1ef902eff5ace837c98891 ] [cleanup dwm@cs.nott.ac.uk**20100205132723 Ignore-this: 297bdff11b2067b2f519a4a7688167d0 ] [The intro command for records now returns a constructor, if possible. Nils Anders Danielsson **20100204192319 Ignore-this: 75f9229c3d165dc62098367f13dc4956 ] [Updated copyright year ranges. Nils Anders Danielsson **20100203173537 Ignore-this: beb5d18982e0a58bb936cd5535023280 ] [Various changes and fixes. Nils Anders Danielsson **20100203173402 Ignore-this: a8bc76f4c8680470693fc641d15b9588 ] [Switched to warning flags which are accepted by cabal check. Nils Anders Danielsson **20100203172834 Ignore-this: b0521331787a10dc6510a6dab70a6926 ] [Made the build dependency constraints stricter. Nils Anders Danielsson **20100203172738 Ignore-this: 8e8757f4cd424497cab806f22eaa16df ] [Updated Makefile and release procedure to reflect existence of agda-pkg. Nils Anders Danielsson **20100203172352 Ignore-this: adc26c9385d2aa5afdc2ec0fb5fcc517 ] [Removed a hard-coded version number. Nils Anders Danielsson **20100203172050 Ignore-this: df1bc0cf321af142ad047808066ba753 ] [initial commit for cabal stuff dwm@cs.nott.ac.uk**20100203163005 Ignore-this: f1b5c73f68d3f93648d784c69d760d5b ] [Optimisation: Goal types were normalised, but the results thrown away. Nils Anders Danielsson **20100201234248 Ignore-this: f8df88a0fc8c220273d14677d1dfefd4 ] [Modified a test. Nils Anders Danielsson **20100201181009 Ignore-this: 621a7481cfd66ccbc5c69c0989225d16 ] [Added the possibility to print out call matrices. Nils Anders Danielsson **20100128170523 Ignore-this: a4c08b5043d7307c16e60c47eef72cb4 ] [Increased code reuse. Nils Anders Danielsson **20100128164859 Ignore-this: f074897f21477afc2a188ac45ecc1c9d ] [Fixed a comment. Nils Anders Danielsson **20100128164833 Ignore-this: 68756f8265310a0c4aebddff8c685851 ] [Cleanup. Nils Anders Danielsson **20100128162531 Ignore-this: ea497e2247092fcec9e20634fbdab060 ] [Removed duplicated debug output. Nils Anders Danielsson **20100128162113 Ignore-this: 41917d9d74b438400982547c95ad9deb ] [Removed potentially misleading comments. Nils Anders Danielsson **20100126160018 Ignore-this: e2c54e6ce5c0e02b45a48b68cb6cdc9e ] [file-SparseMatrix.hs andreas.abel@ifi.lmu.de**20100126111132 Ignore-this: c9af617e7e6cc6d11de1997760251c6 ] [sparse-call-matrices andreas.abel@ifi.lmu.de**20100125235326 Changed the representation of call matrices from the naive to a sparse one. Drastically improves performance for functions with many arguments (like with-generated ones, which could have 30+ arguments). ] [small internal change in the temination module without outside effects andreas.abel@ifi.lmu.de**20090918143412 To turn off the Guardedness check, now you just have to install the alternate definition of addGuardedness ] [Note about pattern matching for records. Nils Anders Danielsson **20100118134956 Ignore-this: e634456c76f539dc10270839f9bc4b99 ] [Added a command which displays all names defined in a given module. Nils Anders Danielsson **20100117101328 Ignore-this: e9e348e2a9d57f128306d4672660588f ] [Avoided duplication of warnings in the file Agda.cabal. Andrés Sicard-Ramírez **20100113073428 Ignore-this: af796047dacd64913d6481b25cce61c1 + Due to a bug in Cabal, I applied the workaround indicated in http://www.haskell.org/pipermail/cabal-devel/2010-January/006018.html. ] [Made "top-level" commands better behaved. Added atTopLevel. Nils Anders Danielsson **20100114193334 Ignore-this: f47dc91031e1a69ec03649376494006 + Previously cmd_infer_toplevel returned answers with unnecessarily long telescopes. ] [Avoided potentially deprecated behaviour of read-string. Nils Anders Danielsson **20100114185313 Ignore-this: bf0d80553d01567c2aa588cba21bfaf3 ] [Added align. Nils Anders Danielsson **20100114184536 Ignore-this: e1165f89409a06d99629f4c63a2a70f3 ] [Added parseExpr. Nils Anders Danielsson **20100114184404 Ignore-this: b99590394cfda1edebb2914e92a161b7 ] [Fixed a comment. Nils Anders Danielsson **20100114184321 Ignore-this: 5ff8a0ec93715a8e79789f0bf0d99462 ] [An example that should arguably typecheck faster. Nils Anders Danielsson **20100118001716 Ignore-this: 3d23879a42fd8c6405bc7428c7d5e080 ] [fixed more problems with record pattern matching ulfn@chalmers.se**20100113203344 Ignore-this: 278fb493bc2f1e49bf4077b49df4354d ] [fixed bug with previous patch ulfn@chalmers.se**20100113193101 Ignore-this: 5546f1fe2aa3a426a0966e9dfe6b79e5 ] [allow pattern matching on records (doesn't obey eta equality yet) ulfn@chalmers.se**20100113192232 Ignore-this: 46f13dbdac196856282002f130ddf1e4 ] [fixed a bug with eta expansion of record metas ulfn@chalmers.se**20100113174408 Ignore-this: e544c417c9f649a851822af7ed55d7cb ] [Less aggressive eta expansion of record metas. Nils Anders Danielsson **20100112190341 Ignore-this: ba96265522d7d0d5d408e72c4a8d4abb + Should make code involving lots of records faster. We have a test case which runs ∼5 times faster. + Implemented together with Ulf. ] [Some PrettyTCM instances. Nils Anders Danielsson **20100112181230 Ignore-this: 9261d17eb11aaf8cd5fc050551b7e5e2 ] [Fixed bug: Some metavariables were stored in interfaces. Nils Anders Danielsson **20100112151312 Ignore-this: 5b98744ad7085d11a5fe452061ada45 + Implemented together with Ulf. ] [added a constraint for argument spines ulfn@chalmers.se**20100113170604 Ignore-this: 7628606aa58005dd42a083b8d9cc5c7b ] [Code which demonstrates poor performance for records. Nils Anders Danielsson **20100112103927 Ignore-this: 1e69474936c5abfbffa453c3d8b57ab8 ] [Instantiate meta-variables before storing function definitions. Nils Anders Danielsson **20100112103648 Ignore-this: 5c889dd14d3ce96ff8528a0885478360 + Consider the function slow: slow : (A : Set) → ℕ → A slow A zero = yippie A slow A (suc n) = slow _ n Before this patch normalisation of slow n seemed to take time proportional to n². The reason was that, even though the meta-variable corresponding to the underscore was solved, the stored code still contained a meta-variable: slow A (suc n) = slow (_173 A n) n (For some value of 173.) The evaluation proceeded as follows: slow A 1000 = slow (_173 A 999) 999 = slow (_173 (_173 A 999) 998) 998 = ... Furthermore, in every iteration the Set argument was traversed, to see if there was any de Bruijn index to raise. + Note that this fix does not apply if the meta-variable cannot be solved locally. It may be worthwhile to go back and update function definitions when meta-variables are solved. + Implemented together with Ulf. ] [Added a performance-related note. Nils Anders Danielsson **20100112103228 Ignore-this: 2f672442f04271020b4de2f98467868 ] [No eta expansion of terms which are already expanded. Nils Anders Danielsson **20100112102332 Ignore-this: eb8061dc45753901ebb9295b6f325f59 + Implemented together with Ulf. ] [Made Agda normalise less often. Nils Anders Danielsson **20100112102050 Ignore-this: d32a2b6f7ac1f55fbdc670c6efebf2fb + This optimisation occasionally gives large benefits. + Implemented together with Ulf. ] [Updated the release notes. Nils Anders Danielsson **20100108184717 Ignore-this: 994f826aa7c9d9dcb9a98bf7a26ce82f ] [Added release note for the option --injective-type-constructors. Andrés Sicard-Ramírez **20100108170224 Ignore-this: 6d21aa02a97dcd7e4bf19c931a6264c5 ] [added --injective-type-constructors option ulfn@chalmers.se**20100108125938 Ignore-this: 2ebc39f7b155ae828c45cc6068c9d656 unless this is switched on you can't prove D A == D B -> A == B for a datatype D ] [Added the Cabal field ghc-prof-options. Andrés Sicard-Ramírez **20091223212332 Ignore-this: a4159a42be9baee198a5b65cc7c95365 ] [Bumped version to 2.2.7. Nils Anders Danielsson **20091223002932 Ignore-this: e0a7b5bddcd4eabde87d9ce4765a12f3 ] [TAG 2.2.6 Nils Anders Danielsson **20091223153937 Ignore-this: 336e8a7d9c462f2fa63d09882b26ed23 ] Patch bundle hash: 8db8cf950fe25f8b3166e3c8f31434f7823d346d