lix/src/libexpr/nix.sdf

definition

module Main
imports Fix


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Top level syntax.

module Fix
imports Fix-Exprs Fix-Layout


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Expressions.

module Fix-Exprs
imports Fix-Lexicals URI
exports
  sorts Expr Formal Bind Binds BindSemi ExprList
  context-free syntax

    Id -> Expr {cons("Var")}

    Int -> Expr {cons("Int")}

    Str -> Expr {cons("Str")}

    Uri -> Expr {cons("Uri")}

    Path -> Expr {cons("Path")}

    "(" Expr ")" -> Expr {bracket}

    Expr Expr -> Expr {cons("Call"), left}

    "{" {Formal ","}* "}" ":" Expr -> Expr {cons("Function")}
    Id -> Formal {cons("NoDefFormal")}
    Id "?" Expr -> Formal {cons("DefFormal")}

    "assert" Expr ";" Expr -> Expr {cons("Assert")}

    "rec" "{" Binds "}" -> Expr {cons("Rec")}
    "let" "{" Binds "}" -> Expr {cons("LetRec")}
    "{" Binds "}" -> Expr {cons("Attrs")}

    Id "=" Expr -> Bind {cons("Bind")}
    {Bind ";"}* -> Binds
    Bind ";" -> BindSemi 
    BindSemi* -> Binds

    "[" ExprList "]" -> Expr {cons("List")}
    "" -> ExprList {cons("ExprNil")}
    Expr ExprList -> ExprList {cons("ExprCons")}

    Expr "." Id -> Expr {cons("Select")}

    "if" Expr "then" Expr "else" Expr -> Expr {cons("If")}

    Expr "==" Expr -> Expr {cons("OpEq"), non-assoc}
    Expr "!=" Expr -> Expr {cons("OpNEq"), non-assoc}

    "!" Expr -> Expr {cons("OpNot")}
    Expr "&&" Expr -> Expr {cons("OpAnd"), right}
    Expr "||" Expr -> Expr {cons("OpOr"), right}
    Expr "->" Expr -> Expr {cons("OpImpl"), right}

    Bool -> Expr {cons("Bool")}

  context-free priorities

    Expr "." Id -> Expr
  > Expr ExprList -> ExprList
  > Expr Expr -> Expr
  > "!" Expr -> Expr
  > Expr "==" Expr -> Expr
  > Expr "!=" Expr -> Expr
  > Expr "&&" Expr -> Expr
  > Expr "||" Expr -> Expr
  > Expr "->" Expr -> Expr
  > "assert" Expr ";" Expr -> Expr
  > "{" {Formal ","}* "}" ":" Expr -> Expr


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Lexical syntax.

module Fix-Lexicals
exports
  sorts Id Int Str Path PathComp Bool
  lexical syntax
    [a-zA-Z\_][a-zA-Z0-9\_\']* -> Id
    "rec" -> Id {reject}
    "let" -> Id {reject}
    "if" -> Id {reject}
    "then" -> Id {reject}
    "else" -> Id {reject}
    "true" -> Id {reject}
    "false" -> Id {reject}
    "assert" -> Id {reject}

    [0-9]+ -> Int

    "\"" ~[\n\"]* "\"" -> Str

    PathComp ("/" PathComp)+ -> Path
    [a-zA-Z0-9\.\_\-\+]+ -> PathComp

    "true" -> Bool
    "false" -> Bool

  lexical restrictions
    Id -/- [a-zA-Z0-9\_\']
    Int -/- [0-9]
    Path -/- [a-zA-Z0-9\.\_\-\+\/]


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% URIs (RFC 2396, appendix A).

module URI
exports
  sorts Uri Uhierpart Uopaquepart Uuricnoslash Unetpath Uabspath
        Urelpath Urelsegment Uscheme Uauthority Uregname Userver
        Uuserinfo Uhostport Uhost Uhostname Udomainlabel Utoplabel
        UIPv4address Uport Upath Upathsegments Usegment Uparam
        Upchar Uquery Ufragment Uuric Ureserved Uunreserved Umark
        Uescaped Uhex Ualphanum Ualpha Ulowalpha Uupalpha Udigit
  lexical syntax
    Uscheme ":" (Uhierpart | Uopaquepart) -> Uri

    (Unetpath | Uabspath) ("?" Uquery)? -> Uhierpart
    Uuricnoslash Uuric* -> Uopaquepart

    Uunreserved | Uescaped | [\;\?\:\@\&\=\+\$\,] -> Uuricnoslash

    "//" Uauthority Uabspath? -> Unetpath
    "/" Upathsegments -> Uabspath
    "//" Uuric* -> Uabspath {reject}
    Urelsegment Uabspath? -> Urelpath

    (Uunreserved | Uescaped | [\;\@\&\=\+\$\,])+ -> Urelsegment

    Ualpha (Ualpha | Udigit | [\+\-\.])* -> Uscheme

    Userver | Uregname -> Uauthority

    (Uunreserved | Uescaped | [\$\,\;\:\@\&\=\+])+ -> Uregname

    ((Uuserinfo "@") Uhostport) -> Userver
    (Uunreserved | Uescaped | [\;\:\&\=\+\$\,])* -> Uuserinfo

    Uhost (":" Uport)? -> Uhostport
    Uhostname | UIPv4address -> Uhost
    (Udomainlabel ".")+ Utoplabel "."? -> Uhostname
    Ualphanum | Ualphanum (Ualphanum | "-")* Ualphanum -> Udomainlabel
    Ualpha | Ualpha (Ualphanum | "-")* Ualphanum -> Utoplabel
    Udigit+ "." Udigit+ "." Udigit+ "." Udigit+ -> UIPv4address
    Udigit* -> Uport

    Uabspath | Uopaquepart -> Upath
    Usegment ("/" Usegment)* -> Upathsegments
    Upchar* (";" Uparam)* -> Usegment
    Upchar* -> Uparam
    Uunreserved | Uescaped | [\:\@\&\=\+\$\,] -> Upchar

    Uuric* -> Uquery

    Uuric* -> Ufragment

    Ureserved | Uunreserved | Uescaped -> Uuric
    [\;\/\?\:\@\&\=\+\$\,] -> Ureserved
    Ualphanum | Umark -> Uunreserved
    [\-\_\.\!\~\*\'\(\)] -> Umark

    "%" Uhex Uhex -> Uescaped
    Udigit | [A-Fa-f] -> Uhex

    Ualpha | Udigit -> Ualphanum
    Ulowalpha | Uupalpha -> Ualpha

    [a-z] -> Ulowalpha
    [A-Z] -> Uupalpha
    [0-9] -> Udigit

  lexical restrictions
    Uri -/- [a-zA-Z0-9\-\_\.\!\~\*\'\(\)]


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Layout.

module Fix-Layout
exports
  sorts HashComment Asterisk Comment EOF
  lexical syntax
    [\ \t\n] -> LAYOUT
    HashComment -> LAYOUT
    Comment -> LAYOUT
    "#" ~[\n]* ([\n] | EOF) -> HashComment
    "//" ~[\n]* ([\n] | EOF) -> HashComment
    "/*" ( ~[\*] | Asterisk )* "*/" -> Comment
    [\*] -> Asterisk
    "" -> EOF
  lexical restrictions
    Asterisk -/- [\/]
    EOF -/- ~[]
  context-free restrictions
    LAYOUT? -/- [\ \t\n] | [\#]