mantognini

<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">

<!--
SFML - Simple and Fast Multimedia Library
Copyright (C) 2007-2018 Marco Antognini (antognini.marco@gmail.com),
                        Laurent Gomila (laurent@sfml-dev.org)

This software is provided 'as-is', without any express or implied warranty.
In no event will the authors be held liable for any damages arising from the use of this software.

mantognini

import stainless.lang._

object Eval {
  def foo: Int = {
    // assert(false)
    43
  } ensuring { _ + 58 == 100 }

  def goo = 1

mantognini

class Lazy[T](computeValue: => T) {
  @volatile private var computed = false
  @volatile private var computing = false // ignore me
  private var value: T = _

  def get: T = {
    if (!computed)
      //synchronized
      {
        if (!computed) {

mantognini

import stainless.annotation._
import stainless.collection._
import stainless.lang._
import stainless.lang.StaticChecks._
import stainless.proof._

object MiniForall {

  @induct
  def lemmaV1[T](xs: List[T], p1: T => Boolean, p2: T => Boolean): Boolean = {

mantognini

(declare-datatypes (A1!36 R!59) ((fun1!8 (fun1!10 (f!148 (=> A1!36 R!59)) (pre!89 (=> A1!36 Bool))))))

(declare-datatypes () ((Positive!1 (Positive!2 (i!53 Int)))))

(declare-const f!28 (fun1!8 Positive!1 Positive!1))

(datatype-invariant thiss!1 Positive!1 (> (i!53 thiss!1) 0))

(assert (not (=> (@ (f!148 (fun1!10 (pre!89 f!28) (lambda ((x!187 Positive!1)) true))) (Positive!2 1)) (let ((res!102 (@ (f!148 f!28) (Positive!2 1)))) (> (i!53 res!102) 0)))))

mantognini

diff -r doc/interpolations.md src/main/doc/interpolations.md
40c40
< ```scala
---
> ```tut:silent
50,55c50,52
< ```scala
< scala> val tpe = t"Boolean"
< tpe: mySymbols.interpolator.trees.Type = Boolean
< 

mantognini

place the two other files in stainless/bin after running `sbt package`.

mantognini

edit build.sbt as follow:

  lazy val `stainless-scalac` = (project in file("frontends/scalac"))
+   .disablePlugins(AssemblyPlugin)

...


  lazy val `stainless-dotty` = (project in file("frontends/stainless-dotty"))
-   .disablePlugins(AssemblyPlugin)

mantognini

[info] Executing forall (codegen): 
[info] ∀x$53354: D$293. ((x$53538: F$3) => {
[info]   require(((x$53529: D$293) => {
[info]     val x$53672: (D$293, D$293, D$293, D$293, D$293, D$293, D$293) = (x$53529, x$53529, x$53529, x$53529, x$53529, x$53529, x$53529)
[info]     true
[info]   })(x$53538) && ((x$53529: E$10) => {
[info]     val x$53859: (E$10, E$10, E$10, E$10, E$10, E$10, E$10, E$10, E$10, E$10, E$10) = (x$53529, x$53529, x$53529, x$53529, x$53529, x$53529, x$53529, x$53529, x$53529, x$53529, x$53529)
[info]     true
[info]   })(((x$53680: D$293) => {
[info]     require({

mantognini

        IOHIDElementRef element = ...

        switch (IOHIDElementGetUsagePage(element)) {
            case kHIDPage_Undefined: sf::err() << "Page of element: kHIDPage_Undefined" << std::endl; break;

            case kHIDPage_GenericDesktop:
                sf::err() << "Page of element: kHIDPage_GenericDesktop" << std::endl;

                switch (IOHIDElementGetUsage(element)) {
                    case kHIDUsage_GD_Pointer: sf::err() << "	Usage of element: kHIDUsage_GD_Pointer" << std::endl; break;