summaryrefslogtreecommitdiff
path: root/src/pretty_print.ml
AgeCommit message (Collapse)Author
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
2016-05-27small change to comment printingKathy Gray
2016-05-27Add sizeof to sail. Documentation to followKathy Gray
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 09:03:14 +0000