Skip to content

Spranjal dependent types support for let rec declarations with refinement types #37

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

Jump to bottom
Open
SharmPranjal wants to merge 72 commits into
base: dependent_types_new_syntax
Choose a base branch
from
Open

Spranjal dependent types support for let rec declarations with refinement types #37

SharmPranjal wants to merge 72 commits into from

Conversation

@SharmPranjal
Copy link

@SharmPranjal SharmPranjal commented Jul 17, 2022

No description provided.

gbdrt and others added 30 commits March 23, 2021 13:05
@gbdrt
Update sundials download link
42fee63
--
030fb13
Add a module for comparing continuous-time floatting-point signals. R…
6854285 
…eturns

a boolean value which is piece-wise constant.
I tried to imagine how to to use "obects with synchronous policies"
f387f54 
to write the example in a more elegant/efficient manner.
Only commented. LS V4 is lost.
Small change.
85ad59a
Small change.
278ee0f
New example used to fix a bug in the scheduling of the
81fa8dc 
init x = ... equations.
Bug fix in the scheduling of [init x = ...] equations
7e0a877 
that appear inside a reset.
@gbdrt
Use Makefile for tests
3165d9a
@gbdrt
Bug fix deps_tools
8dca7e8
@gbdrt
Add all modules to compilerlibs
d855a95
@gbdrt
Release 2.2
ea0acee
@gbdrt
Update subversion
56febdf
@jlvargasme @nskh
adding keyword assume
8526468
@jlvargasme @nskh
adding assert and move_robot keywords
3f728d4
@jlvargasme @nskh
updating files
e2765ee
@jlvargasme @nskh
adding keyword functionality
fee6aa4
@jchen-cs @nskh
Add robot test
18848c5
@jlvargasme @nskh
Adding robot store modifications
cb5a90d
@jchen-cs @nskh
Change keywords to distinguish between languages
b05c154
@jlvargasme @nskh
Adding keyword with string-float arguments
aa6d08d
@jlvargasme @nskh
Adding refinement type parsing
f4b184c
@jlvargasme @nskh
Initial test for refinement type checking in Z3
99105e8
@jlvargasme @nskh
Adding expression parsing for expression validation in Z3
779ab9f
@jlvargasme @nskh
adding hook to compiler pass that interfaces with Z3
ff4255e
@jlvargasme @nskh
Including z3 examples
92e91cc
@jlvargasme @nskh
adding z3 files
0910e88
@jlvargasme @nskh
Adding Z3 interface to deal with constant values and expressions
1d04183
@jlvargasme @nskh
Adding proved property to the environment
ade05e4
@jchen-cs @nskh
Add multiplication, and a counterexample printer
814fbfa
jlvargasme and others added 25 commits February 1, 2022 15:10
@jlvargasme @nskh
Adding proof for refinement functions
965105a
@jlvargasme @nskh
Modifying create_z3_var to check environment for already initialized …
9217b9d 
…values
@jlvargasme
Fixing merge conflicts
18f4dc5
@jlvargasme
Implementing printing for refinement function
2ed3749
@jlvargasme
Adding keyword support of 'box' and 'diamond' to parser
8e63d8b
@jlvargasme
Implementing Z3 translation of 'box' and 'diamond'
ed369ed
@jlvargasme
Adding new custom refinement type support to parser
3974b16
@jlvargasme
Adding unit test for: LTL operator, custom refinement type
4b5c359
@jchen-cs
Merge branch 'dependent_types' of github.com:jeannin/zelus into depen…
455fbda 
…dent_types
@jchen-cs
Revert "Merge branch 'dependent_types' of github.com:jeannin/zelus in…
4294df9 
…to dependent_types"

This reverts commit 455fbda, reversing
changes made to 4b5c359.
@jchen-cs
Add k-induction example
c2fb846
Task23:Making regular function to be trivially true refinement function
3fc9d63
Adding unit tests for task22,23
c8786ed
@EasonZ2022
Merge branch 'dependent_types' into zyicheng-dependent_types_task23
fa0a74c
@EasonZ2022
Merge branch 'dependent_types' into zyicheng-dependent_types_task22
3be78e4
@EasonZ2022
Merge pull request #28 from jeannin/zyicheng-dependent_types_task22
f3dbe16 
Zyicheng dependent types task22
@EasonZ2022
Merge pull request #29 from jeannin/zyicheng-dependent_types_task23
980b280 
Zyicheng dependent types task23
@EasonZ2022
Merge branch 'dependent_types' into zyicheng-dependent_types_fix_cust…
cecce24 
…om_type_error
@EasonZ2022
Merge pull request #32 from jeannin/zyicheng-dependent_types_fix_cust…
1992eb6 
…om_type_error

Zyicheng dependent types fix custom type error
Fixing zparser code lossing
b04f2f5
@EasonZ2022
Merge pull request #33 from jeannin/zyicheng-dependent_types_fix_merg…
4f17308 
…e_conflict

Zyicheng dependent types fix merge conflict
@SharmPranjal
Adding support for pattern COLON type_expression [TASK 16]
321fb44
@SharmPranjal
Adding support for new type expression syntax
82f64cc
@SharmPranjal
Revert "Adding support for new type expression syntax"
00ac504 
This reverts commit 82f64cc.

This revert is for reverting the commit with support for new refinement syntax (needs a pull request of its own)
@SharmPranjal
Unit tests for let rec support
936f208
@jlvargasme jlvargasme changed the base branch from dependent_types to dependent_types_new_syntax August 25, 2022 14:17
@jchen-cs jchen-cs mentioned this pull request Aug 25, 2022
Open
@jlvargasme jlvargasme changed the base branch from dependent_types_new_syntax to dependent_types August 25, 2022 14:17
@jlvargasme jlvargasme changed the base branch from dependent_types to dependent_types_new_syntax August 25, 2022 14:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@SharmPranjal @gbdrt @jlvargasme @jchen-cs @EasonZ2022