summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-11-27Added test for short-circuiting of boolean operationsAlasdair Armstrong
2017-11-27Split rewriter into separate rewriting library and rewrite passesAlasdair Armstrong
2017-11-27Use guards from when patterns when typing casesBrian Campbell
2017-11-27Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2017-11-27Compile assertions into OCamlAlasdair Armstrong
2017-11-27Fix bitvector pattern removal typoBrian Campbell
2017-11-27Replace bad generic comparisons in monoBrian Campbell
2017-11-27Case splitting on boolsBrian Campbell
2017-11-24Use unbound precision big_ints throughout sail.Alasdair Armstrong
2017-11-24Attempt to document intermediate language used by Sail in ott.Alasdair Armstrong
2017-11-21Expose entry point in elf_loader for Sail modelAlasdair Armstrong
2017-11-21Check non-constraint liftable assertions in blocks correctlyAlasdair Armstrong
2017-11-21Merge Thomas' suggested changesBrian Campbell
2017-11-20Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2017-11-20Fix a bug with constraint generation in flow typing.Alasdair Armstrong
2017-11-20Tidy last upBrian Campbell
2017-11-20Constant propagation in guardsBrian Campbell
2017-11-20Basic handling of recursive calls in monomorphisation analysisBrian Campbell
2017-11-20Look up the right type variables in monomorphisation analysisBrian Campbell
2017-11-20Support new nexp in monoBrian Campbell
2017-11-17Fix Makefile for interpreter and update instruction_extractorAlasdair Armstrong
2017-11-17Fix interpreter to work with new typecheckerAlasdair Armstrong
2017-11-16Make the generation of the lem_ast numeric constants automatic for all number...Alasdair Armstrong
2017-11-16Made l2.ott generate an ast.lem which is is valid w.r.t. -lem_ast output.Alasdair Armstrong
2017-11-16Remove unused Typ_wild constructorAlasdair Armstrong
2017-11-16Fixed some longstanding issues regarding constraints on type constructors.Alasdair Armstrong
2017-11-15Additional test case for OCaml backendAlasdair Armstrong
2017-11-15Simplify flow typing code in typecheckerAlasdair Armstrong
2017-11-15Merge branch 'smt' into experimentsAlasdair Armstrong
2017-11-15Fix atom - range unification againAlasdair Armstrong
2017-11-15Fix rule for allowing atom to unify with rangeAlasdair Armstrong
2017-11-15Allow user defined operations in nexps (experimental)Alasdair Armstrong
2017-11-15Report all monomorphisation problemsBrian Campbell
2017-11-15For loops bind a type variableBrian Campbell
2017-11-15Remove untested infix monomorphisation (removed by type checker)Brian Campbell
2017-11-15Tidy up in monomorphisationBrian Campbell
2017-11-14During monomorphisation always refine constructors,Brian Campbell
2017-11-14Fix existential union typing problem in monomorphisationBrian Campbell
2017-11-14Remove some obsolete codeBrian Campbell
2017-11-14Automatic analysis for monomorphisationBrian Campbell
2017-11-13Record where existentials were created in their names.Alasdair Armstrong
2017-11-10Fixed ocaml backend so it correctly compiles registers passed by name.Alasdair Armstrong
2017-11-10Fixed some tricky typechecking bugsAlasdair Armstrong
2017-11-08Allow functions to be selectively declared external only for some backendsThomas Bauereiss
2017-11-08Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong
2017-11-08Allow for different extern names for different backendsAlasdair Armstrong
2017-11-07Fix typo in constraint rewriterThomas Bauereiss
2017-11-07Add builtin for reversing endiannessThomas Bauereiss
2017-11-07Declare prelude functions as externThomas Bauereiss
2017-11-07Fix vector_subrange typoBrian Campbell