summaryrefslogtreecommitdiff
path: root/src/pretty_print.ml
AgeCommit message (Collapse)Author
2018-07-25Remove unused internal AST nodesAlasdair Armstrong
E_internal_cast, E_sizeof_internal, E_internal_exp, E_internal_exp_user, E_comment, and E_comment_struc were all unused. For a lem based interpreter, we want to be able to compile it to iUsabelle, and due to slowness inherent in Isabelle's datatype package we want to remove unused constructors in our AST type. Also remove the lem_ast backend - it's heavily bitrotted, and for loading the ARM ast into the interpreter it's just not viable to use this approach as it just doesn't scale. We really need a way to be able to serialise and deserialise the AST efficiently in Lem.
2018-01-05Removed legacy parser/lexer and pretty printerAlasdair Armstrong
2017-12-05Update license headers for Sail sourceAlasdair Armstrong
2017-11-24Use unbound precision big_ints throughout sail.Alasdair Armstrong
Alastair's test cases revealed that using regular ints causes issues throughout sail, where all kinds of things can internally overflow in edge cases. This either causes crashes (e.g. int_of_string fails for big ints) or bizarre inexplicable behaviour. This patch switches the sail AST to use big_int rather than int, and updates everything accordingly. This touches everything and there may be bugs where I mistranslated things, and also n = m will still typecheck with big_ints but fail at runtime (ocaml seems to have decided that static typing is unnecessary for equality...), as it needs to be changed to eq_big_int. I also got rid of the old unused ocaml backend while I was updating things, so as to not have to fix it.
2017-07-21Everything moved to new typecheckerAlasdair Armstrong
Modified initial_check.ml so it no longer requires type_internal. It's still needs cleaned up in a few ways. Most of the things it's trying to do could be done nicer if we took some time to re-factor it, and some of the things should just be handled by the main typechecker, leaving it as a think layer between the parse_ast and the ast. Now that's done everything can be switched to the new typechecker and the _new suffixes were deleted from everything except the monomorphisation pass because I don't know the status of that.
2017-07-21Switch to new typechecker (almost)Thomas Bauereiss
Initial typecheck still uses previous typechecker
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 23:39:14 +0000