msph/micro sappho

Micro sappho is a minimalistic language for demonstration of the SPHO type system. It is implemented using a simple parser and lexer that implements the grammar below. The indended use is to allow experimentation and familiarization with the SPHO types and subtyping.

Grammar

Grammar in pseudo-bnf

And yes, it is ambiguous at places. More specification coming when there is time.


MSph ::= Body

Body ::= Dirs

Dir ::= Typedef             (directives, with lack of a better name)
      | Memberdef
      | Nominaldecl
      | Checkdir

Typedef ::= 'type' Name '=' TExpr                   (type definition/binding)
          | 'type' Name '[' Names ']' '=' TExpr
          | 'type' Name                             (declaration, donno if useful)

Memberdef ::= 'member' Name ':' TExpr

Nominaldecl ::= 'nominal' Name

Checkdir ::= 'check' TExpr '<:' TExpr

TExpr ::= 'True'
        | 'False'
        | Var
        | Nominal
        | Trait
        | TExpr '&' TExpr
        | TExpr '|' TExpr
        | TExpr '=>' TExpr
        | TExpr '->' TExpr
        | 'box' TExpr
        | 'forall' Name '.' TExpr
        | '(' TExpr ')'

Trait ::= '{' Body '}'                  (trait, this introduces scoping)

Var ::= Name                            (type variables)
Nominal ::= Name                        (nominal type)

Name ::= '[a-zA-Z0-9_]+' & !Reserved     (name/identifier)

Reserved ::= 'type'                     (reserved/keywords)
           | 'member'
           | 'nominal'
           | 'check'
           | 'forall'
           | 'box'
           | 'True'
           | 'False'

Precedence of binary operators: '&' < '|' < '->' < '=>'

< means "binds closer"

Example

A simple example msph program


nominal ExampleN

type ExampleDecl
type ExampleDecl2

type Example = {
    member example_m : C -> C
    type FA = forall X. X -> X

    type b = forall X. (box X => ExampleDecl) => ExampleDecl2
}

member example_global : Example & ExampleN

type TripleConj[X, Y, Z] = X & Y & Z

2 KiB Raw Blame History

msph/micro sappho

Grammar

Example

2 KiB

Raw Blame History