noschinl / cyp Goto Github PK
View Code? Open in Web Editor NEWChecker for "morally correct" induction proofs about haskell programs
License: MIT License
Checker for "morally correct" induction proofs about haskell programs
License: MIT License
for consistency with other named equations (axiom, lemma), goal syntax should:
So, not goal non . not .=. id
but goal g1: not . not .=. id
As I'm planning to use this in an online system: could this be DoS-ed?
Are there short proofs where checking would be expensive?
But the proof language is rather explicit - so cyp never has to guess/search? Well, it guesses the subterm where a rule is applied, and the direction of the rule application. But the work is still linear in the size of the term, and the term is written in the proof.
What else could go wrong? Like, too much backtracking in the parser, or even: inefficient pretty-printing ( haskell/pretty#32 )
If we do type-inference, then that's another surface for attack (naive unification algorithms, or naive printing of inferred types in error messages)
(I do have other safety measures in place already.)
README.md says
<term a1>
.=. <term a2>
but this should be
<term a1>
(by <reason>) .=. <term a2>
(request for discussion of feature)
It seems an identifier can only be used in axioms and goals if it has a definition (that is, equations).
I would love to be able to have exercises "prove this about f, using only that axioms" - where f's implementation is not given.
Of course, f's type should be declared (see issue #10) but I could also imagine f = undefined
(again, Wadler's law)
some identifiers consist of more that one token. Sometimes they are separated by exactly one space, sometimes by whitespace (e.g., more spaces). (I will mark space by "_" in the following)
I think that in all cases, whitespace should be accepted.
perhaps not that important, but when I tried to write a simple proof (without looking at examples),
I fully expected that it's by axiom <name>
, by similarity to by def <name>
.
( https://wiki.haskell.org/Wadler%27s_Law )
Since cyp is about proving things about Haskell programs, I expect line "--" and block "{- .. -}" comments to work. These may be useful while working on a proof (students will ask for this) and for giving hints for proofs (when I give students a template for the proof).
The current situation seems to be that comments only work inside inside expressions, or directly before or after them - and in a few other cases, like in proof texts, where I can comment out a line of (inside a chain of equations).
For the tests in test-data/neg
there are always cout
to test that cyp gives the correct message. When the file contains a newline before the end of the file (which many editors add automatically), then the tests break. Moreover, this is quite difficult to spot when viewing the tasty test results as tasty prints a newline automatically. For future reference: if you want to remove the newline at EOL you can use the command truncate -s -1
This uses an identifier xs
Proof by induction on List xs
but its type is not what's written there (the type argument is missing).
This will super-confuse students - or (worse), keep them in the Java-before-Generics mindset where List
actually was a type ...
(EDIT: I see, this uses the identifier. The declaration comes from Proof by extensionality with <name>
, which does not mention a type at all. - That's even worse :-)
If I want to give exercise questions of the kind "complete this (partial) proof", then I need to mark positions in a proof tree where students can fill in stuff.
(and I need to check that they did not change the tree in other places, but this issue is not about implementation, it is about design)
I think there are two kinds of "proof holes"
(by def foo) .=. <hole>
- the studentParseProof
, etc.) (cyp has "by cheating" already?)What would be good (uniform) notation for that? Preferrable, notation that is understood by cyp,
so it does not crash, but gives a message "partial proof, need to fill hole(s) at ..." and continues processing in some meaningful way (if possible).
(Implemenation for Haskell Lückentexte: https://gitlab.imn.htwk-leipzig.de/autotool/all0/blob/master/collection/src/Haskell/Blueprint/Match.hs . I don't use "list holes" there, in fact, it was in the matching code, but I switched it off)
I made this example https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/tree/master/test-data/pos/bintree
and I was surprised that I could write two IHs:
Case Branch l k r
To show: (inorder . mirror) (Branch l k r) .=. (reverse . inorder) (Branch l k r)
IH: (inorder . mirror) l .=. (reverse . inorder) l
IH: (inorder . mirror) r .=. (reverse . inorder) r
and that I could refer to them just by IH
(and cyp picks the right one)
Because of #12 , I tried
append = append
but this was rejected by the parser.
Parsing background theory
Parsing function definition 'append = append'
Invalid function definition
I think it should be accepted, since it is syntactically valid Haskell.
This special case foo = foo
perhaps is only needed for this work-around, but foo = bar
might actually occur.
Not a bug. But I'd appreciate hints on how this feature could be implemented (relative to the current code base) most easily.
I want to write
inorder :: Tree a -> List a
right next to the actual definitions (current parser simply rejects this). For my own sanity, for documentation, and because I recommend this coding style to my students.
I find upper case very inconvenient for typing (needs one more key). Does it improve readability? Not sure. "QED" definitely feels overdone. (Or is this because Latin didn't have lower case letters at all?)
How does Isabelle do it - all keywords start with lowercase letter?
(design question)
I think it would be nice if theory files were valid Haskell modules, so they can be used with ghc(i),
so that the student can interactively develop the program, type-check it, and evaluate expressions.
This applies to data declarations and value (function) declarations. Of course I don't want full Haskell - just that GHC understands CYP syntax and agrees on the semantics.
(This would also make testing any CYP extensions (type system) much easier.)
Then we have CYP axioms and goals, which currently are not-Haskell. We could
E.g., goal filter p . filter p .=. filter p
could be written as
goal_1 p xs = (filter p . filter p) xs == (filter p) xs
so we can evaluate Test.LeanCheck.check goal_1
.
This has two technical problems:
==
on functions (in Leancheck)Currently cyp has no pretty printer for its expression type. Sometimes, we can work around this by using the input string instead (see AProp, ATerm types), but this does not work if the terms are automatically generated (induction subgoals, for example).
Goal: Implement a pretty printer. This should omit unneeded parentheses and input operators.
Hi,
I am forking your project at https://gitlab.imn.htwk-leipzig.de/waldmann/cyp because I want to use this with the Leipzig autotool system (cf. https://gitlab.imn.htwk-leipzig.de/autotool/all0/issues/39 )
As a first step, I patched cyp to work with recent haskell-src-exts.
I am getting 4 failed tests (see https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/builds/3770 , https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/builds/3770/artifacts/file/test.text ) is this expected?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.