Code Monkey home page Code Monkey logo

literate-unitb's People

Stargazers

avatar avatar

Watchers

avatar avatar avatar

literate-unitb's Issues

Command line option to override constant "tool" in Build

Originally reported by: Simon Hudon (Bitbucket: cipher2048, GitHub: Unknown)

Add the command line option:

-build Stack
-build Cabal

to override the default value of "tool". Look into packages "lambda-options" (which I do not know) or "System.Console.GetOpt" in base (which I know and use in Continuous.hs).

Think of using unsafePerformIO (from System.IO.Unsafe) in the definition of "tool" to gain access to command line arguments.

With this design, any executable linked with Build will be able to make use of that command line option.

Self documenting parser

Originally reported by: Simon Hudon (Bitbucket: cipher2048, GitHub: Unknown)

The file ./syntax.txt documents the top-most syntax of machines - not including expressions or proofs. Here are the first 7 lines:

#!text
\assumption{fresh-name}{expression}
\comment{text / comment}{text / comment}
\constant{text / comment}
\constraint{fresh-name}{expression}
\cschedule{concrete event-name}{fresh-name}{expression}
\dummy{text / comment}
\evassignment{concrete event-name}{fresh-name}{expression}

And the last two lines:

#!text

\begin{liveness}{proof-obligation-name} .. \end{liveness}
\begin{proof}{proof-obligation-name} .. \end{proof}

Note that they don't come with descriptive paragraphs and the inside of \begin / \end are not described.

Improvements:
o Include a paragraph for every command / environment
o Include a section for the syntax of expressions
o Include a section for predicate calculus proofs
o Include a section for liveness proofs

Swap out MissingH

Originally reported by: Amin Bandali (Bitbucket: aminb, GitHub: aminb)

MissingH is not being developed anymore and the author(s) doesn't seem to be responding or taking any action on the reported issues.

It has been a probable cause of build problems with stack in the past (for me personally) and lately with the introduction of isSymbolicLink in directory-1.2.6.0 there's an ambiguity between the version from 'directory' and the one from 'unix'.

Right now, we use a couple of string utility functions from Data.String.Utils, and map, replace, and split functions from Data.List.Utils, from MissingH.

The following list of alternatives is incomplete, so we'd either bring code over directly from MissingH find other existing packages that have the utilities we use.

Alternatives:

  • split: We can use Data.List.Split.splitOn from the split package instead of Data.List.Utils.split and/or Data.String.Utils.split from MissingH. As of now, the mentioned methods of MissingH and split have the same behaviour for non-empty lists, and the split package seems to handle the empty list case more sanely than MissingH.

Use Data.Fix to make the recursion of Expr explicit

Originally reported by: Simon Hudon (Bitbucket: cipher2048, GitHub: Unknown)

I'm thinking of one task that might lie ahead for you. It's to generalize the expression syntax tree. So far, it has four type parameters: the encoding of names, the type system (so far I handle multi-sorted first order, because of Z3, and polymorphic ML type, for the reasoning in the specification and also no type system), the type annotation (similar to the type system) and quantifier type (first order (without lambdas, sums, etc) and higher order (with lambdas, etc))

I would like to add one degree of flexibility. I would like to use Data.Fix to handle the recursion of expression trees explicitly. If I simplify the expression tree,

data Expr = Var VarName | FunApp FunName Expr

would become

data Expr' expr = Var VarName | FunApp FunName expr
type Expr = Fix Expr'

The new version of Expr would be isomorphic to the old one (i.e. it contains the same information) but now Expr' is more flexible. We can use it to create expression trees with holes waiting to be filled:

type ExprWithHole = Fix (Compose Maybe Expr')
-- (Compose Maybe Expr' a) is isomorphic to Maybe (Expr' a)
-- the difference is that in Compose Maybe Expr' a the last
-- type parameter is 'a' while in Maybe (Expr' a) the last type
-- parameter is Expr a.

In the above, every subexpression is basically optional: you can fill them up with 'Nothing' if you have a procedure that will fill them up later. For example, we could
imagine a monadic action on an ExprWithHole as "fillHoles":

fillHoles :: Monad m => (Maybe Expr -> m Expr) -> (ExprWithHoles -> m Expr)
What really interests me about this type definition is adding LineInfo to the nodes of an expression tree. This way, when we do type checking, we can generate exact messages about which expression and subexpressions are badly typed and output the line info of the beginning and end of the problematic subexpressions.

It would be defined as:

type ExprLI = Fix (Compose ((,,) LineInfo LineInfo) Expr')
-- ((,,) LineInfo LineInfo) is the type of triples applied to two arguments,
-- which leaves one argument open to be filled by a subexpression.

It is not urgent as my current approach can still serve for the moment. What I currently do is render problematic expressions as S-expressions (as if I would feed them to Z3). It's not the best but it's ok.
The task is not easy so you can start thinking about how you would do it and get started only when you feel ready.

Delay redundant proofs

Originally reported by: Simon Hudon (Bitbucket: cipher2048, GitHub: Unknown)

When re-parsing a model some proof obligations remain the same and they do not have to be proved again. Other proof obligations remain mostly the same with the exception of added assumptions. If they were proved successfully already, the truth of the new proof obligation follows. However, more assumptions make the task of the theorem prover harder and retrying the proof obligation might result in a failure. Most of the time, it shouldn't but we want only want to call "proved" the proof obligations on which the theorem prover succeeded.

On the other hand, every time an invariant is added to a model, most of its proof obligations get a new assumption and retrying all of them for every new invariant becomes expensive and delays the proof of more important, newer proof obligations.

The idea is to delay (maybe by 1 minute, maybe by 5) the starting of provers on augmented proof obligations (the ones that were proved and for which the only change is adding assumptions) and only starting them when no others need to be proved.

Retirement of Latex.Scanner

Originally reported by: Simon Hudon (Bitbucket: cipher2048, GitHub: Unknown)

I would like to retire the model Latex.Scanner on which Logic.Expr.Parser relies (I think Latex.Parser no longer does) because parsec is a better way of writing that code. After you've separated expression parsing from type checking, when you're ready, rewriting the expression parser using parsec would be very useful.

Type-based arity invariant in Expr

Originally reported by: Simon Hudon (Bitbucket: cipher2048, GitHub: Unknown)

The thing is to use type checking to increase the safety of expression syntax trees.

If I remove the type parameters and simplify, function application is declared as:

| FunApp Fun [Expr] -- Line 66 in Logic.Expr.Expr

where Fun contains [Type] as one of its components. One invariant that I need to rely on is that the list of expressions and the list of types have the same length. We can use existential types to enforce that invariant. All we need to do is give Fun a type parameter that stands for its arity and use a different data structure than list - let's call them vectors - which has a type parameter that stands for its length. Function application becomes:

| forall arity. FunApp (Fun arity) (Vector arity Expr)

Now the parser is responsible of checking the arity of functions applied to arguments and the rest of the code can safely assume that it is consistent (the type checker won't let it be inconsistent).

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.