summaryrefslogtreecommitdiff
path: root/src/pretty_print.ml
AgeCommit message (Collapse)Author
2016-04-25make pretty printer keep up with parser changesKathy Gray
2016-03-02Add new language feature to permit definitions of items of kind Nat, etc as ↵Kathy Gray
well as items of kind Type. Syntax for the feature is: def Nat id = nexp Note: some useful nexps may not parse properly. All typedef forms can also be used as def Type ... if desired, but this is not required.
2016-02-23Several fixesKathy Gray
Improve printing for asl to sail readability; Add -o option for selecting the name of file generation; Add additional initial check module for turning generated ast nodes into ready-to-type-check ast nodes
2016-02-09fix scattered type union source printingKathy Gray
2016-02-08slightly clean up vector type printing and empty effect printing for functionsKathy Gray
2016-01-26move closer to power.sail -> power.ml outputKathy Gray
2016-01-06Add new assert expression to SailKathy Gray
This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error. WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified.
2015-12-21fixes, pp progressChristopher
2015-12-16rewriter and pp changes for generating ARM outputChristopher
2015-12-15better location informationChristopher
2015-12-09adapted for Kathy's lexp effect typing changes: register writes should be ↵Christopher
correct now, fixes, pp
2015-12-07adapted pp for Kathy's effect type changesChristopher
2015-12-03added prompt.lem for connecting to concurrency model and ↵Christopher Pulte
{power,armv8}_extras.lem; fixes
2015-11-25fixes, ppChristopher Pulte
2015-11-24Add BE_escape effect when an E_exit is seenKathy Gray
Close #20
2015-11-20no more unecessary variables from removing vector-concatenation pattern ↵Christopher Pulte
matches, reset variable name counter for each function clause, fixes
2015-11-19fixes for cumulative effect anotationsChristopher Pulte
2015-11-13fixes, more ppChristopher Pulte
2015-11-10rewriting fixes, syntactically correct lem syntax, number type errors remainingChristopher Pulte
2015-11-07fixes, no more uncessary variables, pp progressChristopher Pulte
2015-11-06progress on generating function for read/writing register fieldsChristopher Pulte
2015-11-06fixesChristopher Pulte
2015-11-05some progress on lem backend: rewrite away mutable variable assignments, ↵Christopher Pulte
rewrite for-loops, if/case-expressions to return updated variables
2015-10-29Ocaml generation now just needing big int/little int issues resolved ↵Kathy Gray
(probably) at least for Power.
2015-10-28progress on lem backend: auto-generate read_register and write_register ↵Christopher Pulte
functions, and state definition
2015-10-26fixChristopher Pulte
2015-10-26Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-26add preliminary Sail_values.lem, adapt lem pp to recent Ocaml pp changesChristopher Pulte
2015-10-23More of sail correctly generating ocaml; including using polymorphic ↵Kathy Gray
variants when there are more than 246 constructors
2015-10-20add copies of ocaml-pp functions for lem-ppChristopher Pulte
2015-10-20ocaml output now produces parsing power.sailKathy Gray
2015-10-20more fixesKathy Gray
2015-10-20Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-20compiling prettyprinterKathy Gray
2015-10-20Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-20fix a-normalisation bugChristopher Pulte
2015-10-20Fixing bugs in pretty printer to ocamlKathy Gray
2015-10-19progress on lem backendChristopher Pulte
2015-10-13Merge branch 'master' of https://bitbucket.org/Peter_Sewell/l2Christopher Pulte
2015-10-13some progress on sequentialise_effectsChristopher Pulte
2015-10-13Refine local vs cumulative effects for lexpKathy Gray
More ocaml output, better treatment of registers.
2015-10-07Compiling again after refactoring. Haven't pushed to interpreter and lem yetKathy Gray
2015-10-07adapted pretty_print and rewriter to new tannot typeChristopher Pulte
2015-10-07start changing representation of registers for ocamlKathy Gray
2015-10-06better printing for register writing, whole register (maybe not "right" yet)Kathy Gray
more library
2015-10-05made vector_concat pass remove typ annotation expression inside ↵Christopher Pulte
vector_concat patterns, fixed a pp missing newline
2015-10-04add find_updated_vars to support for-loops for lem or prover backend, add ↵Christopher Pulte
normalise_exp exp that should transform expressions into a form where they can be embedded into monadic lem or prover definitions. Both untested
2015-09-30Alias support for ocaml modeKathy Gray
2015-09-29capitalise and uncapitalise according to ocaml requirementsKathy Gray
2015-09-29ml output passing simple test suite, except for register aliasesKathy Gray
Known todo: Write library functions in ocaml Properly upper-case/lower-case the first letter of names to conform to ocaml requirements Handle register aliases Turn id reads to dereferences for local ref variables
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 04:00:18 +0000