git.iko.soy/Idris-dev
on de0bcbd help sign in
history ofsrc/Idris/Parser.hs
all commits
631fc46Further splitting of ParserEdwin Brady 67fb9ccSplit Parser.hs into several filesEdwin Brady 4447a4dChanged structure of parser such that it correctly overloads TokenParsing using some newtype hackery.Ahmad Salim Al-Sibahi fa6f5faRefactored constraint syntax to use less lookaheadAhmad Salim Al-Sibahi d1b5cb9Refactored data declaration to use less lookahead for better errors and some performance improvementAhmad Salim Al-Sibahi 336f5daSome refactoring of bracketed expressions (centralizing most of the expressions). This provides some simplification for future optimization of grammar regrding issue idris-lang/Idris-dev#452.Ahmad Salim Al-Sibahi a88a918Allow eof instead of eol for comments, closes idris-lang/Idris-dev#503Ahmad Salim Al-Sibahi 45e0a55Merge pull request #504 from david-christiansen/with-parserEdwin Brady 4ed09e4Further improve error message on missing parens after withDavid Christiansen 50af5aaMake the parentheses around a with-rule scrutinee mandatoryDavid Christiansen 7ae55f9Merge remote-tracking branch 'upstream/master' into error-reflectionDavid Christiansen 3a69398Add parser and tests for parser for error reflection extensionDavid Christiansen 3db1e91Added flag for error reflection extensionDavid Christiansen fc3f097Removed explanations for comments (as to not say expected comment when something is wrong)Ahmad Salim Al-Sibahi 4afee31Further refactoring of decl' to allow errors to be propagated correctlyAhmad Salim Al-Sibahi 6a8f0dbRefactored new parser to use considerably less try-statements/lookahead for better performance and error reportingAhmad Salim Al-Sibahi 41d7fb8Fixed unspecified error on empty module without any declarationsAhmad Salim Al-Sibahi d3bb097Fixed doc comments in multi-line comments bugAhmad Salim Al-Sibahi 73bdc53Refactoring of parser to Trifecta, documenting and updating some items/fixing some issues.Ahmad Salim Al-Sibahi c55f8c2Unification fix to avoid giving up on recoverable errorsEdwin Brady daab1a3Partially defined names should not reduce at compile-timeEdwin Brady e8f4bb1Some packaging fixesEdwin Brady af4fda7%flag directiveEdwin Brady 8eb2087Separate IO and PrimIO PrimIO is the internal primitive, IO is the user version which requires an explicit World token to be passed in which programmers have no access to directly. Fixes #185 and fixes #325Edwin Brady 0aca9f2New module chaser, for better dependency checking and rebuilding Now treats each source file separately, building a tree of dependencies, and rebuilding if any dependencies have updated. In particular, this fixes a problem with stale definitions hanging around when building packages, and has required some fixes to imports in the library.Edwin Brady 2d8e573Move universe level check to after all modules are loaded ...otherwise it gets repeated needlessly for every moduleEdwin Brady 8f8ab98Remove unused syntax for 'InferRef' definitions Was only meant to be temporary! (InferRef are names in where clauses whose types are to be inferred)Edwin Brady 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 fd9bd68Add '%reflection' option for functions A reflection function can evaluate at compile-time only, and pattern matches on *syntax* rather than on constructor forms. Also add 'prim__syntactic_eq' for a compile-time syntactic equality check.Edwin Brady 0558972Fix parsing of indented blocks If there is no indentation, the block should be considered empty. This means empty parameters or using blocks are no longer allowed, which was always the intention, and empty data/instance/class declarations are allowed without needing an explicit {}. Fixes #437Edwin Brady 7875005Change treatment of underscore in lambda Treat as unnamed variables, rather than as patternsEdwin Brady 6f88ecdAdd syntax for transformation rules %transform lhs ==> rhs Unbound names on the lhs are treated as patterns. Transformation behaviour not yet implemented.Edwin Brady ad66486Add %specialise annotation for functions (Part 1 of partial evaluation) %specialise [n1 t1, n2 t2 ...] as an annotation before a function type means that the r.h.s. of all the clauses will be evaluated, but with the name n1 reduced at most t1 times, etc. The t1 part is optional, and means unlimited (which is the default for all names at the minute anyway)Edwin Brady b543b29Allow names to be attached to provisional definitions lhs ?= {name} rhs -- generates a lemma called 'name' which makes the types of the lhs and rhs match. {name} is optional - a unique name is generated if it is absent.Edwin Brady 8e0f138Merge pull request #383 from JanBessai/ITCharEdwin Brady 7fc4865Allow 'rewrite ... in' to assert the resulting type "rewrite f ==> t in x" means that after applying the rewrite f, the required type of x must be t. This is primarily for readability of proofs built by successive rewritings.Edwin Brady 3448469Add "equiv" tactic "equiv t" asserts that the current goal has a type equivalent (by conversion) to tEdwin Brady 773e454Make ChType a member of IntTy ITChar.Jan Bessai 86b5a5bParse integer SIMD typesBenjamin Saunders 0aa3fd6Beginnings of integer SIMD support (no backend yet)Benjamin Saunders f149970Rename --target to --codegen and add options to specify target triple and CPU, defaulting to that of hostBenjamin Saunders 9c11754Added %unifyLog construct For debugging purposes %unifyLof t will give a trace of unification problems while elaborating t Also, log levels 6 and above will give the traceEdwin Brady ce7e45bEXPERIMENTAL: Syntax for applying functions by expected type "t <== f" applies a function f to arguments in such a way that it returns something of type t. The <== is a placeholder syntax until someone comes up with something better. (Alternative: t by f, but that uses up a new keyword)Edwin Brady c7fded1Added 'mrefine' tactic Like refine, but uses matching instead of unification to resolve implicit arguments. All will become clear, I hope :). This is intended for an additional style of pattern matching (on types) for better explanation of proofs.Edwin Brady 894db6fMerge pull request #340 from JanBessai/BackendTargetSpecificationEdwin Brady eacfe5cAdded backend target specification to %lib, %link and %include directivesJan Bessai f2f0e07Default to Integer instead of Int, and adjust fromInteger accordinglyBenjamin Saunders 5b2f091Allow type class constraints in 'using' clauses e.g. if a using block is given asEdwin Brady 943b653Merge branch 'MixingImplicitArgs' of https://github.com/JanBessai/Idris-dev into JanBessai-MixingImplicitArgsEdwin Brady a0308f1Parser improvement to allow mixing of implicit and non implicit ArgumentsJan Bessai