From 1694b97d0a0865064e866cffa77f986e4dea96fe Mon Sep 17 00:00:00 2001 From: Regis Blanc <regwblanc@gmail.com> Date: Tue, 21 Jul 2015 15:10:51 +0200 Subject: [PATCH] basic purescala scaladoc --- src/main/scala/leon/package.scala | 2 ++ .../scala/leon/purescala/Constructors.scala | 5 ++++ .../scala/leon/purescala/Expressions.scala | 17 ++++++++++++- src/main/scala/leon/purescala/package.scala | 24 +++++++++++++++++++ 4 files changed, 47 insertions(+), 1 deletion(-) create mode 100644 src/main/scala/leon/purescala/package.scala diff --git a/src/main/scala/leon/package.scala b/src/main/scala/leon/package.scala index 92e4b7a03..147109724 100644 --- a/src/main/scala/leon/package.scala +++ b/src/main/scala/leon/package.scala @@ -1,3 +1,5 @@ +/* Copyright 2009-2015 EPFL, Lausanne */ + /** Core package of the Leon system * * Provides the basic types and definitions for the Leon system. diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala index e520e049e..5a931642e 100644 --- a/src/main/scala/leon/purescala/Constructors.scala +++ b/src/main/scala/leon/purescala/Constructors.scala @@ -11,6 +11,11 @@ import TypeOps._ import Common._ import Types._ +/** Provides constructors for [[purescala.Expressions]. + * + * The constructors implement some logic to simplify the tree and + * potentially use a different expression node if one is more suited. + */ object Constructors { // If isTuple, the whole expression is returned. This is to avoid a situation diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala index 5c02df406..c23aa1f6e 100644 --- a/src/main/scala/leon/purescala/Expressions.scala +++ b/src/main/scala/leon/purescala/Expressions.scala @@ -11,7 +11,22 @@ import Extractors._ import Constructors._ import ExprOps.replaceFromIDs -/** Expression definitions for Pure Scala. */ +/** Expression definitions for Pure Scala. + * + * If you are looking for things * such as function or class definitions, + * please have a look to [[purescala.Definitions]]. + * + * Every expression in Leon inherits from [[Expr]]. The AST definitions are simple + * case classes, with no behaviour. In particular, they do not perform smart + * rewriting. What you build is what you get. For example, + * {{{ + * And(BooleanLiteral(true), Variable(id)) != Variable(id) + * }}} + * because the ``And`` constructor will simply build a tree without checking for + * optimization opportunities. Unless you need exact control on the structure + * of the trees, you should use constructors in [[purescala.Constructors]], that + * simplify the trees they produce. + */ object Expressions { private def checkParamTypes(real: Seq[Typed], formal: Seq[Typed], result: TypeTree): TypeTree = { diff --git a/src/main/scala/leon/purescala/package.scala b/src/main/scala/leon/purescala/package.scala new file mode 100644 index 000000000..03ab3061f --- /dev/null +++ b/src/main/scala/leon/purescala/package.scala @@ -0,0 +1,24 @@ +/* Copyright 2009-2015 EPFL, Lausanne */ + +package leon + +/** Provides AST definitions for Leon programs. + * + * The core language supported by Leon is called Pure Scala and its + * [[leon.purescala.Definitions]] and [[leon.purescala.Expressions]] are defined here. + * This package also contains the [[leon.purescala.Types]] definitions. Each of those + * trees come with a corresponding set of operations in the ???Ops objects. + * + * The package also provides general utilities operations on Pure Scala programs, such as + * a method lifting phase [[leon.purescala.MethodLifting]] (transforming methods into + * top level functions) and a function closure phase [[leon.purescala.FunctionClosure]] + * (lifting an inner function to the top level). + * + * Two printers for Pure Scala programs are also provided, a [[leon.purescala.PrettyPrinter]] + * that outputs a nice and readable program (typically using unicode for some operations) and + * a [[leon.purescala.ScalaPrinter]] that outputs a valid Scala program from a Leon + * representation. + */ +package object purescala { + +} -- GitLab