Skip to content
Open

pyre #26

Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
464 changes: 464 additions & 0 deletions pyre/.pyre/pyre.stderr

Large diffs are not rendered by default.

41 changes: 41 additions & 0 deletions pyre/_benchmark.rkt
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
#lang racket

(require racket/cmdline)
(require "../lib.rkt")

(define current-typechecker-symbol 'pyre)
(define current-typechecker-name "pyre")

(define typechecker-parameters
`((name ,current-typechecker-name)
(comment-char #\#)
(extension ".py")
(file-base-path ,(current-directory))
(examples-file-base-path ,(current-directory))
(arguments ,(list "check" "--source-directory=main" "none" "--version" "pyre"))
(examples-arguments ,(list "check" "--source-directory=examples" "none" "--version" "pyre"))
(command "npx")))

(command-line
#:program "_benchmark.rkt"
#:once-each
[("-v" "--verbose") "Print the output of the benchmarks to the console"
(benchmark-verbose #t)]
[("-f" "--format") output-format "Print the output of the benchmarks in the specified format. Options: plain, markdown, tex. Default: plain."
(benchmark-output-format (string->symbol output-format))]
[("-t" "--transpose") "Transpose the output of the benchmarks"
(benchmark-output-transposed #t)]
[("-e" "--examples") "Run the advanced examples"
(benchmark-run-examples #t)]
#:args ()
(void))

(define benchmark-data (execute-benchmark-for-one-typechecker typechecker-parameters))
(define benchmark-result-for-printing (list (cons current-typechecker-name benchmark-data)))

(define actual-test-names (map car benchmark-data))
(define header-row (cons "Benchmark" actual-test-names))

(print-benchmark benchmark-result-for-printing
(benchmark-output-format)
header-row)
106 changes: 106 additions & 0 deletions pyre/examples/examples.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,106 @@
from typing import TypeIs, Callable, TypeVar, Union

T = TypeVar("T")
S = TypeVar("S")
type JSON = Union[str, float, bool, None, list[JSON], dict[str, JSON]]

### Code:
## Example filter
## success
def filter_success(l: list[T], predicate: Callable[[T], TypeIs[S]]) -> list[S]:
result: list[S] = []
for element in l:
if predicate(element):
result.append(element)
return result

## failure
def filter_failure(l: list[T], predicate: Callable[[T], TypeIs[S]]) -> list[S]:
result: list[S] = []
for element in l:
if predicate(element):
result.append(element)
else:
result.append(element)
return result

## Example flatten
## success
type MaybeNestedListSuccess = list[MaybeNestedListSuccess] | int
def flatten_success(l: MaybeNestedListSuccess) -> list[int]:
if isinstance(l, list):
if l:
return flatten_success(l[0]) + flatten_success(l[1:])
else:
return []
else:
return [l]

## failure
type MaybeNestedListFailure = list[MaybeNestedListFailure] | int
def flatten_failure(l: MaybeNestedListFailure) -> list[int]:
if isinstance(l, list):
if l:
return flatten_failure(l[0]) + flatten_failure(l[1:])
else:
return []
else:
return l

## Example tree_node
## success
type TreeNodeSuccess = tuple[int, list[TreeNodeSuccess]]

def is_tree_node_success(node: object) -> TypeIs[TreeNodeSuccess]:
if not (isinstance(node, tuple) and len(node) == 2):
return False
else:
if not isinstance(node[0], int):
return False
else:
if not isinstance(node[1], list):
return False
else:
for child in node[1]:
if not is_tree_node_success(child):
return False
return True

## failure
type TreeNodeFailure = tuple[int, list[TreeNodeFailure]]

def is_tree_node_failure(node: object) -> TypeIs[TreeNodeFailure]:
if not (isinstance(node, tuple) and len(node) == 2):
return False
else:
if not isinstance(node[0], int):
return False
else:
if not isinstance(node[1], list):
return False
else:
return True

## Example rainfall
## success
def rainfall_success(weather_reports: list[JSON]) -> float:
total = 0.0
count = 0
for day in weather_reports:
if isinstance(day, dict) and "rainfall" in day:
val = day["rainfall"]
if isinstance(val, float) and 0 <= val <= 999:
total += val
count += 1
return total / count if count > 0 else 0

## failure
def rainfall_failure(weather_reports: list[JSON]) -> float:
total = 0.0
count = 0
for day in weather_reports:
if isinstance(day, dict) and "rainfall" in day:
val = day["rainfall"]
total += val
count += 1
return total / count if count > 0 else 0
Loading