Skip to content

ucsd-progsys/liquidhaskell-interactive

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

12 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

README

lhi is a persistent LiquidHaskell server (cf. hdevtools) that will enable

  1. Incremental Checking
  2. Interactive Queries
  3. Interactive Proofs & Synthesis

Incremental Checking

Interactive Queries

Interactive Proofs (and Synthesis)

Framework

To create your own server, simply provide implementations of the above, and:

Types

  • Types.Command
  • Types.Response
  • Types.State

Code

  • Handler.init
  • Handler.handler
$ lhi get --key=cat
Daemon started on port 7856
Just (Failed "not found")
$ lhi put --key=cat --val=garfield
Just (Value "Ok!")
$ lhi get --key=cat
Just (Value "garfield")
$ lhi get --key=dog
Just (Failed "not found")
$ lhi put --key=dog --val=fido
Just (Value "Ok!")
$ lhi get --key=cat
Just (Value "garfield")
$ lhi get --key=dog
Just (Value "fido")

About

Persistent LiquidHaskell Server To Enable Fast Interactive/Incremental Checking

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published