Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[pre-commit.ci] pre-commit autoupdate #21

Open
wants to merge 2 commits into
base: tutorial
Choose a base branch
from
Open

[pre-commit.ci] pre-commit autoupdate #21

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3f38806
[pre-commit.ci] pre-commit autoupdate
pre-commit-ci[bot] Jan 27, 2025
28ce689
[pre-commit.ci] auto fixes from pre-commit.com hooks
pre-commit-ci[bot] Jan 27, 2025
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
4 changes: 2 additions & 2 deletions .pre-commit-config.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,13 @@
# See https://pre-commit.com/hooks.html for more hooks
repos:
- repo: https://github.com/pre-commit/pre-commit-hooks
rev: v4.4.0
rev: v5.0.0
hooks:
- id: trailing-whitespace
- id: end-of-file-fixer
- id: check-yaml
- id: check-added-large-files
- repo: https://github.com/igorshubovych/markdownlint-cli
rev: v0.36.0
rev: v0.44.0
hooks:
- id: markdownlint-fix
5 changes: 0 additions & 5 deletions examples/hyperrec/spec.vcl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,8 +49,3 @@ hyperRectangle x = forall i . vectorMin ! i <= x ! i <= vectorMax ! i
@property
property : Bool
property = forall x . hyperRectangle x => advises x pos





28 changes: 11 additions & 17 deletions examples/hyperrec/spec2.vcl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,22 +55,22 @@ inputTranspose = foreach i . foreach j . inputs ! j ! i
-- identity : Tensor Rat [2, 3]
-- identity = [ [1, 0, 1], [0, 1, 0] ]

-- vectorMin : Tensor Rat [inputSize, 5] -> Index 5 -> Bool
-- vectorMin x i = forall j k. x ! j ! i <= x ! j ! k
-- vectorMin : Tensor Rat [inputSize, 5] -> Index 5 -> Bool
-- vectorMin x i = forall j k. x ! j ! i <= x ! j ! k

vectorMin : Index 30 -> Index 5 -> Bool
vectorMin i j = forall k . inputs ! j ! i <= inputs ! j ! k
vectorMin i j = forall k . inputs ! j ! i <= inputs ! j ! k

vectorMax : Index 30 -> Index 5 -> Bool
vectorMax i j = forall k . inputs ! j ! k <= inputs ! j ! i
vectorMax i j = forall k . inputs ! j ! k <= inputs ! j ! i

@property
property : Bool
property = forall x. forall j i l k. validInput x and vectorMin i j and vectorMax l k and x ! i >= inputs ! j ! i and inputs ! k ! l >= x ! l => advises x pos
property = forall x. forall j i l k. validInput x and vectorMin i j and vectorMax l k and x ! i >= inputs ! j ! i and inputs ! k ! l >= x ! l => advises x pos

{-
vectorMax : Vector Rat 5 -> Index 5 -> Vector Bool 5
vectorMax x i = foreach j . x ! j <= x ! i
vectorMax : Vector Rat 5 -> Index 5 -> Vector Bool 5
vectorMax x i = foreach j . x ! j <= x ! i

vectorOut : Tensor Rat [inputSize, n] -> Vector Rat inputSize
vectorOut x = foreach i . x ! i -}
Expand All @@ -80,25 +80,19 @@ vectorOut x = foreach i . x ! i -}
-- property = True

{-
vectorMax : InputVector
vectorMax : InputVector
vectorMax = foreach i . 1 -- maxList (inputTranspose ! i)

vectorMin : InputVector
vectorMin : InputVector
vectorMin = foreach i . 0 --minList (inputTranspose ! i)

vectorMax : InputVector
vectorMax : InputVector
vectorMax = foreach i . 1 -- maxList (inputTranspose ! i)

hyperRectangle : InputVector -> Bool
hyperRectangle x = forall i . vectorMin ! i <= x ! i <= vectorMax ! i

@property
property : Bool
property = forall x . hyperRectangle x => advises x pos
property = forall x . hyperRectangle x => advises x pos
-}