1. Peter_Sewell
  2. lem

Commits

Show all
Author Commit Message Date Builds
Gabriel Kerneis
Improve lexing of string literals - Allow lower-case hexadecimal digits - Fix line number in the "\newline spaces" special case
Branches
string-literals
Gabriel Kerneis
Document UTF8 string literals and escape sequences Escape sequences follow the OCaml syntax. This should maybe be explained in the documentation as well.
Branches
string-literals
Gabriel Kerneis
UTF8 string literals and escape sequences - Represent string literals as UTF-8 internally. - Check that literals are UTF-8 encoded during lexing. - Allow escape sequences, with OCaml syntax: http://caml.inria.fr/pub/docs/manual-ocaml/lex.html#escape-sequence - Add a string_escape hook to allow backend-specific escaping. HOL and Isabelle backends are currently not escaped properly (this was already the case before this patch, of course)…
Branches
string-literals
Gabriel Kerneis
Upgrade Ulib to the latest batteries version Keep the structure of files in batteries to ease future upgrades. BatText has been cut to remove pretty-printing, since we do not need it in Lem and it pulls a lot of dependencies (BatIO, etc.).
Branches
string-literals
Dominic Mulligan
Tidied the standard Coq extlib by removing all ad hoc list functions and defining set functions in terms of standard Coq list constants.
Dominic Mulligan
Merge branch 'master' of https://bitbucket.org/Peter_Sewell/lem
Dominic Mulligan
Moved from ad hoc implementation of lists in the Coq extlib to standard Coq list library. Happy consequence: Mark's cmm.lem now is completely processed by Coq including the previously troublesome apply_trees. Program Fixpoint must use some previously defined lemmas on Coq list functions silently to close termination proofs.
kathyg
More support for solving matrix of equations, most of solver implemented. Also resolving issue #10
Thomas Tuerk
adding sum-type
Dominic Mulligan
Some more work on vectors and their implementation in the Coq backend from this morning.
Thomas Tuerk
fix issue #8 fix problem with precedence inside record expressions
Gabriel Kerneis
Syntax error on not terminated strings (closes #9)
Dominic Mulligan
Some minor work on alternative Coq lib for Jade.
Dominic Mulligan
Some more work on vectors.
Dominic Mulligan
Coq extlib renamed as Coq cannot understand hyphens in library names apparently.
Dominic Mulligan
q# (use "git checkout -- <file>..." to discard changes in working directory)
kathyg
More support for setting up matrix for solving constraints; simplifying matrix prior to solving resolves most unification variables that previously were solvable under strict structural equality.
kathyg
WARNING: Non-backwards-compatible change. Vector type parameter order is now : forall 'type ''length . vector 'type ''length
kathyg
Turning constraints into matrices for solving.
Dominic Mulligan
Missed some files in last commit: changes to Coq backend to get vectors working.
Dominic Mulligan
Work on including vectors in the Coq backend. Also started an alternative implementation of the Coq extlib using Jade's preferred definition of set, implemented as a predicate into Prop.
kathyg
Add comments for the vector functions in vector library.
kathyg
Constraint solving for simple, one unification variable constraints. (old system still active as many constraints use at least two unification variables).
kathyg
Merge branch 'master' of https://bitbucket.org/Peter_Sewell/lem
Peter_Sewell
tidy old README
Peter_Sewell
add lem.pdf to repo
Peter_Sewell
build fixes
kathyg
Merge branch 'master' of https://bitbucket.org/Peter_Sewell/lem
kathyg
starting to gather constraints
Peter_Sewell
point to lem.pdf in README.md
  1. Prev
  2. Next