summaryrefslogtreecommitdiff
path: root/src/pretty_print.ml
AgeCommit message (Collapse)Author
2017-03-29Factor out pretty printers into separate files. Hopefully this will make ↵Robert Norton
searching easier.
2017-03-24Checkpoint work-in-progress mips sequential interpreter using ocaml shallow ↵Robert Norton
embedding.
2017-03-24changes to ocaml pp to allow mips->ocaml to compileRobert Norton
2017-02-09group initial type environment into meaningful sections; pretty-print in ↵Peter Sewell
user-readable way
2017-02-09tweak pp of initial type environment and l2.ott commentsPeter Sewell
2017-02-05command-line option to dump initial type environmentPeter Sewell
2017-02-03fix headersPeter Sewell
2017-01-31Kathy, Peter: pp of initial type environmentPeter Sewell
2017-01-14update pretty printing to actually reflect lem ast changesKathy Gray
2016-12-12pp fixChristopher Pulte
2016-12-12cheri sail export progressChristopher Pulte
2016-12-09sail changes for making lem embedding Isabelle-friendlierChristopher Pulte
2016-12-01move interpreter-specific types from Sail_impl_base to Interp_interfaceChristopher Pulte
2016-11-30shallow embedding fix, rename 'copy' to 'reset_vector_start', don't print ↵Christopher Pulte
shallow/deep ast conversion type class instances anymore, add herdtools ast / shallow ast conversion functions, add mips ImplementationDefinedStopFetching instruction
2016-11-28make sail produce prompt and state version of shallow embedding files at the ↵Christopher Pulte
same time with the types both have in common factored out into separate file, rename one mips shallow embedding _extras file as required by this
2016-11-23Make type checker not run to fix point on resolving case-split type ↵Kathy Gray
variables; modern implementation of nexp unification seems not to need it
2016-11-23Add new type checking file. Small changes to type inference, temporary ↵Kathy Gray
change to printing
2016-11-14add option -lem_sequential for producing shallow embedding that refers to ↵Christopher Pulte
state monad, library fixes
2016-11-08fixesChristopher Pulte
2016-11-07factor out regfp analysis types into etc/regfp.sailChristopher Pulte
2016-11-05fixesChristopher Pulte
2016-10-28shallow embedding progressChristopher Pulte
2016-10-27more shallow embedding fixesChristopher Pulte
2016-10-26shallow embedding fixesChristopher Pulte
2016-10-24fixes, check in Shaked's sail_impl_base changesChristopher Pulte
2016-10-21shallow embedding progressChristopher Pulte
2016-10-20fix previous FromToInterpValue typeclass issue, factor out intpreter's ↵Christopher Pulte
interp_value_to_instr_external
2016-10-19typeclass instances for converting between shallow and deep embeddingChristopher Pulte
2016-10-13make sail-to-lem rewriting passes use dependency analysis, make dependency ↵Christopher Pulte
analysis include type information, small pp fix
2016-10-11move armv8_extras and power_extras to idl/power and idlarm, fixesChristopher Pulte
2016-10-10changed the way registers/register fields work, fixes, nicer names for new ↵Christopher Pulte
letbound variables
2016-10-06move type definitions that both interpreter and shallow embedding use to ↵Christopher Pulte
sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome
2016-09-26minor changesChristopher Pulte
2016-09-26nicer lem output: fewer unnecessary letbinds, monad binds and returnsChristopher Pulte
2016-09-25nicer lem output: no more unecessary 'unit' returns if if-expressions, ↵Christopher Pulte
for-loops or case-expressions also return updated variables
2016-09-24nicer lem output: fewer unecessary 'return'sChristopher Pulte
2016-09-23sail-to-lem progressChristopher Pulte
2016-09-21fixesChristopher Pulte
2016-09-19sail-to-lem progressChristopher Pulte
2016-09-16make vector concatenation pattern removal deal with vector patterns of ↵Christopher Pulte
unknown length (in the last item)
2016-09-09update instruction_analysis to support nias and instruction kindChristopher Pulte
2016-09-07push some lem pp changesChristopher Pulte
2016-08-17Fix pattern match bug in interp where vector accesses were using the wrong ↵Kathy Gray
start index
2016-08-14Start adding form for (a,b,c) := foo()Kathy Gray
Not working yet
2016-07-25auto coerce to bit vector from bitKathy Gray
pretty print lret effects into lem
2016-07-23Add a return exp form to Sail, supported in type checker and in interpreter.Kathy Gray
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
2016-07-20Make rewriter understand type abbreviations for removing internal_exp instancesKathy Gray
2016-07-13fixesChristopher
2016-07-12sail-to-lem and lem library fixesChristopher
2016-05-27Fix parsing of sizeof and some printing issues with letKathy Gray
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 20:56:02 +0000