git.iko.soy/Idris-dev
on 783d45f help sign in
history ofsrc/Core/CoreParser.hs
all commits
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 2402885Generic syntax declarations (see prelude.idr for example)Edwin Brady a805f47Added constants and some primitive operationsEdwin Brady 82585e7Some ghc 6.12 compatibilityEdwin Brady 64b7cfdParsing high level data declarationsEdwin Brady 3b297bcParsing declarations, keeping track of fixitiesEdwin Brady ff5f762Rename Core to TTEdwin Brady 0ae24f1Shift core TT into a separate directory (for ease of reuse)Edwin Brady