Custom datatypes in ProofScript

[phlegmaticprogrammer]

It should be possible to define custom datatypes in ProofScript.

[phlegmaticprogrammer]

Here is a draft proposal for how to define two custom datatypes Option and List:

deftype 
  Option
    None !
    Some ! (x : Any)
  List
    Nil !
    Cons ! (head : Any, tail : List)

The deftype construct would only be allowed at the toplevel of the theory. Each type name follows a list of constructor definitions of the form Constructor [pattern]. In the above you could create a value of type Option for example via writing None ! or Some ! 1, and a value of type List by writing Nil ! or Cons ! (1, Cons ! ("Hey", Nil)), but for example not by writing Cons ! 1 because 1 does not match the pattern (head : Any, tail : List). Note that None and Some just written like that have the type Constructor.

There is the new corresponding pattern match construct expr ! pattern which will evaluate expr which must evaluate to some constructor. The value is then checked to have been constructed via this constructor or not. If it has, the argument of the constructor is matched against pattern. Correspondingly, there is a pattern match construct expr !.

[phlegmaticprogrammer]

You would also be able to create values of type Constructor by casting a pair of functions construct and destruct like that:

val C = [construct, destruct] : Constructor

Then the expression C ! t will evaluate to construct t. The pattern C ! p will match a value v if destruct v returns [w] and w matches p, and not match if destruct v returns nil.

Furthermore you can create a constructor like that:

val C = [value] : Constructor

The expression C ! will just evaluate to value, and the pattern C ! will match v if v is comparable to value and v == value is true.

[phlegmaticprogrammer]

Let me take back the bit about being able to create your own constructors, that seems nice, but not really necessary right now. Also what we talked about in terms of encapsulation: we don't really need that, I think. @Chattered , do you agree with that?

[phlegmaticprogrammer]

Ok, after having a discussion with Phil today the design for datatypes is changed to get rid of the bang operator and an explicit constructor type. Instead upper case identifiers always annotate constructors and are thus not available for normal identifiers:

datatype 
  Option
    None 
    Some (x : Any)
  List
    Nil
    Cons (head : Any, tail : List)

Pattern matching is then as simple as expected, for example Nil is a pattern that matches the empty list given the above definition, Cons _ matches any nonempty list, Cons (x if x >= 0, Nil) will match a list consisting of a single nonnegative integer element. Note that the pattern Cons (_, 1) will not match any list at all but is a valid pattern nevertheless.

[phlegmaticprogrammer]

@Chattered : I have published commit 7311ada75b13b99 which introduces the new naming convention that all variables introduced in patterns must be lower-case. That brakes some of your code, especially where you use names like P and Q for variables which match predicate terms. Please fix! I leave it in the datatype branch for now so that you can first push your latest changes to the ProofScript files to master.

[ghost]

How does that help with git? I want to make my changes over yours to make sure they are compatible.

On 16/05/15 16:18, Steven Obua wrote:

@Chattered https://github.com/Chattered : I have published commit 7311ada https://github.com/proofpeer/proofpeer-proofscript/commit/7311ada75b13b99da72494699b46ba407030bcae which introduces the new naming convention that all variables introduced in patterns must be lower-case. That brakes some of your code, especially where you use names like |P| and |Q| for variables which match predicate terms. Please fix! I leave it in the datatype branch for now so that you can first push your latest changes to the ProofScript files to master.

— Reply to this email directly or view it on GitHub https://github.com/proofpeer/proofpeer-proofscript/issues/62#issuecomment-102637194.

[phlegmaticprogrammer]

You have still metis-related fixes that are not in master, right? Push them first so that all scripts run through again. Then I'll sync the data type branch. On 18 May 2015 06:48, "Phil Scott" notifications@github.com wrote:

How does that help with git? I want to make my changes over yours to make sure they are compatible.

On 16/05/15 16:18, Steven Obua wrote:

@Chattered https://github.com/Chattered : I have published commit 7311ada < https://github.com/proofpeer/proofpeer-proofscript/commit/7311ada75b13b99da72494699b46ba407030bcae>

which introduces the new naming convention that all variables introduced in patterns must be lower-case. That brakes some of your code, especially where you use names like |P| and |Q| for variables which match predicate terms. Please fix! I leave it in the datatype branch for now so that you can first push your latest changes to the ProofScript files to master.

— Reply to this email directly or view it on GitHub < https://github.com/proofpeer/proofpeer-proofscript/issues/62#issuecomment-102637194 .

— Reply to this email directly or view it on GitHub https://github.com/proofpeer/proofpeer-proofscript/issues/62#issuecomment-102928256 .

[ghost]

No. I pushed all those fixes on the 13th. I've also committed downcasings of the variables that offend the datatype branch and pushed them to master. You should be able to go ahead with merging datatype onto master.

On 18/05/15 09:53, Steven Obua wrote:

You have still metis-related fixes that are not in master, right? Push them first so that all scripts run through again. Then I'll sync the data type branch. On 18 May 2015 06:48, "Phil Scott" notifications@github.com wrote:

How does that help with git? I want to make my changes over yours to make sure they are compatible.

On 16/05/15 16:18, Steven Obua wrote:

@Chattered https://github.com/Chattered : I have published commit 7311ada <

https://github.com/proofpeer/proofpeer-proofscript/commit/7311ada75b13b99da72494699b46ba407030bcae>

which introduces the new naming convention that all variables introduced in patterns must be lower-case. That brakes some of your code, especially where you use names like |P| and |Q| for variables which match predicate terms. Please fix! I leave it in the datatype branch for now so that you can first push your latest changes to the ProofScript files to master.

— Reply to this email directly or view it on GitHub <

https://github.com/proofpeer/proofpeer-proofscript/issues/62#issuecomment-102637194

.

— Reply to this email directly or view it on GitHub

https://github.com/proofpeer/proofpeer-proofscript/issues/62#issuecomment-102928256 .

— Reply to this email directly or view it on GitHub https://github.com/proofpeer/proofpeer-proofscript/issues/62#issuecomment-102980166.

[phlegmaticprogrammer]

I tested the current master branch with run scripts, but three theories don't go through yet:

failed compiling theory '\bootstrap\Redundancies':
  * term expected
    in scripts/bootstrap/syntax.thy at row 20, column 9
    in scripts/bootstrap/syntax.thy at row 20, column 3
    in scripts/bootstrap/syntax.thy at row 19, column 11 (rator applied to: nil)

skipping theory '\bootstrap\lift' because one of its ancestor theories failed
skipping theory '\bootstrap\redundancies2' because one of its ancestor theories failed

What's up with those?

[ghost]

Your proofpeer-metis might be out-of-date. Is it saying that the conjecture is unprovable?

On 18/05/15 10:09, Steven Obua wrote:

I tested the current master branch with |run scripts|, but three theories don't go through yet:

|failed compiling theory '\bootstrap\Redundancies':

• term expected in scripts/bootstrap/syntax.thy at row 20, column 9 in scripts/bootstrap/syntax.thy at row 20, column 3 in scripts/bootstrap/syntax.thy at row 19, column 11 (rator applied to: nil)

skipping theory '\bootstrap\lift' because one of its ancestor theories failed skipping theory '\bootstrap\redundancies2' because one of its ancestor theories failed |

What's up with those?

— Reply to this email directly or view it on GitHub https://github.com/proofpeer/proofpeer-proofscript/issues/62#issuecomment-102983296.

[phlegmaticprogrammer]

Updated proofpeer-metis, now it runs through until this error comes:

failed compiling theory '\bootstrap\redundancies2':
  * unknown identifier: bigUnion
    in scripts/bootstrap/redundancies2.thy at row 32, column 64
    in scripts/bootstrap/redundancies2.thy at row 30, column 3
    in scripts/bootstrap/redundancies2.thy at row 27, column 1

I guess that's because you already propagated the datatype changes to redundancies2.

Cool, will sync the datatype branch once I get it to run through again (right now there are parse conflicts).

[phlegmaticprogrammer]

Merged datatype on top of master and everything runs through now with the new uppercase/lowercase conventions. Great!

[phlegmaticprogrammer]

datatype feature is implemented now, see https://github.com/proofpeer/proofpeer-proofscript/blob/master/scripts/examples/CustomDatatypes.thy for examples.