git.iko.soy/Idris-dev
on d1663cc help sign in
history ofsrc/Core/CoreParser.hs
all commits
3c32b65Whitespace cleanup.George Leontiev d564e1dRemoved keyword from CoreParser tooAhmad Salim Al-Sibahi 48d1105Added 'quoteGoal x by p in e' syntax meaning, let x = p [current goal] in e Additionally, the value of x is normalised, which means p can be a compile-time only %reflection function used to prove something interesting in e. See test030 for an example of automated proof by reflection.Edwin Brady 86b5a5bParse integer SIMD typesBenjamin Saunders 5a968c4Parse empty commentsAndy Morris 8af32d4squash potential space leaks by using strict foldlraichoo db5973bAdded rewrite ... in ... construct rewrite prf in v rewrites the goal type using prf. It is equivalent to applying replace, without the need to provide a predicate. It works by applying the rewrite tactic with prf before elaborating v.Edwin Brady 0bcdd51Complete identifiers following non-whitespaceDavid Christiansen 022d4dfAdded 'implicit' conversions implicit f : a -> b Then, when a function needs a 'b' but has an 'a', f will be called implicitly. This is probably scary and fragile. Use with extreme caution!Edwin Brady 41f3d97Merge branch 'master' of git://github.com/edwinb/Idris-dev into bitstringBenjamin Saunders 25ec644Modify documentation comment parsingEdwin Brady b896224Primitive types for groups of 8, 16, 32, and 64 bits, and basic arithmetic and mutual conversion operations on themBenjamin Saunders dd5001fmake TT aware of Set -> Typeraichoo cc716d7Make 'Type' the type of types instead of Sets ...after mailing list discussionEdwin Brady bbbe563Merge pull request #114 from raichoo/wordEdwin Brady f6451efword 8/16 primitive typesraichoo 06283b6Improve evaluation of projection By caching result of evaluation, so that it's already evaluated when next projection happens.Edwin Brady bd89fdcSmall change to doc comment syntax (allow spaces before | or ^)Edwin Brady 1ccd94aSyntax for documentation comments and :doc REPL commandEdwin Brady 8464bc4Add field for documentation comments in abstract syntaxEdwin Brady 96f3b9eFix nested parameters blocksEdwin Brady 6d7a6aaChange comment rules Comments cannot begin '{-|' or '--|'. This is now reserved for documentation comments, which will be part of the syntax to support documentation at the REPL.Edwin Brady af66f25Added 'mutual' blocks Effect is to elaborate all types in the block before elaborating definitionsEdwin Brady 5692e48Added "codata" Constructors of coinductive types evaluate arguments lazily. Corecursive functions do not reduce at compile time.Edwin Brady 7b2bf5eAdded "partial" keyword and "%default" directiveEdwin Brady 517acc1Namespace parsing improvements (for qualified operator names) thanks to Dirk UllrichEdwin Brady ffc7b69First baby steps towards a new RTS (and towards removing epic dependency)Edwin Brady fee6b51Fix reverse elaboration of dependent pairsEdwin Brady 126eb94Remove 'prefix' keywordEdwin Brady dcb9ca0Change meaning of alternative syntax (| a , b , ... |) Now takes the first alternative to elaborate,rather than requiring exactly one to work. Old behaviour reserved for disambiguating namespaces.Edwin Brady de6bb41Added 'total' keyword and positivity checkEdwin Brady 3b36802Record syntax (but no magic yet...)Edwin Brady 67c5734Added case and pattern matching let bindings Also pattern matching bind in do notation case notation currently has limitations: - only works on simple types (each pattern must have the same type, more specifically) - return type needs to be known at the point of elaborationEdwin Brady 9265e7cAdded 'public', 'abstract' and 'private' modifiers 'public' means export everything (name and definition) 'abstract' means export just the name 'private' means export nothing for data types and classes, 'abstract' means export the type/class name but not the members.Edwin Brady 60c4ef9Added 'impossible' keywordEdwin Brady 9f65713Fix name parsing for nested namespacesEdwin Brady fa5f1cdNamespacesEdwin Brady b26716aCollect cumulativity constraints on universesEdwin Brady dbc607cDecorating names for namespacesEdwin Brady 1807c65No letters in operatorsEdwin Brady bbaa193Better representation of namesEdwin Brady 4931c20Added Integer (but an Epic bug prevents them compiling properly)Edwin Brady 169d8c0Elaborating instance declarationsEdwin Brady be3a53aType class instance resolution, and some Num overloadingEdwin Brady 6cc3c32Fix small elaboration bugEdwin Brady ebcb29bAdded proof script traces for pasting into programEdwin Brady 95a558bAdded = and reflEdwin Brady 39b934cSugar for dependent pairsEdwin Brady bf368abFirst attempt at with ruleEdwin Brady 834a5e0Fix bug in applying syntax rulesEdwin Brady