From 248f76e33c99466119e25526b6c40b6faec9880d Mon Sep 17 00:00:00 2001 From: Yves Date: Mon, 21 Aug 2023 13:50:20 +0200 Subject: [PATCH] PLT-7142: Script to generate language specification, moved Marlowe LBNF --- flake.nix | 4 +- haskell/marlowe-reference.cabal | 9 +- .../src/Language/Marlowe/Syntax/AbsMarlowe.hs | 77 ----- .../src/Language/Marlowe/Syntax/LexMarlowe.x | 270 ------------------ .../src/Language/Marlowe/Syntax/ParMarlowe.y | 227 --------------- .../src/Language/Marlowe/Syntax/Translate.hs | 91 ------ nix/scripts.nix | 8 +- .../language_specification}/Marlowe.cf | 0 8 files changed, 11 insertions(+), 675 deletions(-) delete mode 100644 haskell/src/Language/Marlowe/Syntax/AbsMarlowe.hs delete mode 100644 haskell/src/Language/Marlowe/Syntax/LexMarlowe.x delete mode 100644 haskell/src/Language/Marlowe/Syntax/ParMarlowe.y delete mode 100644 haskell/src/Language/Marlowe/Syntax/Translate.hs rename {haskell/src/Language/Marlowe/Syntax => papers/language_specification}/Marlowe.cf (100%) diff --git a/flake.nix b/flake.nix index 9daa9f0a..8e07103f 100644 --- a/flake.nix +++ b/flake.nix @@ -46,7 +46,7 @@ }; latex = (pkgs.texlive.combine { - inherit (pkgs.texlive) scheme-basic ulem collection-fontsrecommended mathpartir stmaryrd polytable lazylist; + inherit (pkgs.texlive) scheme-basic ulem collection-fontsrecommended mathpartir stmaryrd polytable lazylist ucs; }); project = pkgs.haskell-nix.cabalProject' { @@ -67,11 +67,13 @@ build-marlowe-proofs edit-marlowe-proofs build-marlowe-docs + generate-marlowe-language-specification ] ) ++ (with pkgs; [ nil haskellPackages.lhs2tex + haskellPackages.BNFC ]) ++ [ latex formatting.fix-nix-fmt ]; }; diff --git a/haskell/marlowe-reference.cabal b/haskell/marlowe-reference.cabal index 3dd84385..77d4703b 100644 --- a/haskell/marlowe-reference.cabal +++ b/haskell/marlowe-reference.cabal @@ -9,10 +9,7 @@ cabal-version: >= 1.10 executable marlowe default-language: Haskell2010 - build-tools: alex, - happy - build-depends: array, - base >= 4.9 && < 5, + build-depends: base >= 4.9 && < 5, base16-bytestring >= 1 && < 2, bytestring >= 0.10.12 && < 0.12, containers >= 0.6.5 && < 0.7, @@ -36,10 +33,6 @@ executable marlowe Language.Marlowe.Semantics.Types Language.Marlowe.Semantics.Deserialisation Language.Marlowe.Semantics.Serialisation - Language.Marlowe.Syntax.AbsMarlowe - Language.Marlowe.Syntax.LexMarlowe - Language.Marlowe.Syntax.ParMarlowe - Language.Marlowe.Syntax.Translate Language.Marlowe.ExtendedBuilder Language.Marlowe.Serialisation Language.Marlowe.Deserialisation diff --git a/haskell/src/Language/Marlowe/Syntax/AbsMarlowe.hs b/haskell/src/Language/Marlowe/Syntax/AbsMarlowe.hs deleted file mode 100644 index c78c9263..00000000 --- a/haskell/src/Language/Marlowe/Syntax/AbsMarlowe.hs +++ /dev/null @@ -1,77 +0,0 @@ --- File generated by the BNF Converter (bnfc 2.9.4). - --- | The abstract syntax of language Marlowe. - -module Language.Marlowe.Syntax.AbsMarlowe where - -import Prelude (Integer, String) -import qualified Prelude as C (Eq, Ord, Show, Read) - -data Contract - = Close - | Pay Party Payee Token Value Contract - | If Observation Contract Contract - | When [Case] Timeout Contract - | Let ValueId Value Contract - | Assert Observation Contract - deriving (C.Eq, C.Ord, C.Show, C.Read) - -data Case = Case Action Contract | MerkleizedCase Action String - deriving (C.Eq, C.Ord, C.Show, C.Read) - -data Action - = Deposit Party Party Token Value - | Choice ChoiceId [Bound] - | Notify Observation - deriving (C.Eq, C.Ord, C.Show, C.Read) - -data Value - = AvailableMoney Party Token - | Constant Integer - | NegValue Value - | AddValue Value Value - | SubValue Value Value - | MulValue Value Value - | DivValue Value Value - | ChoiceValue ChoiceId - | TimeIntervalStart - | TimeIntervalEnd - | UseValue ValueId - | Cond Observation Value Value - deriving (C.Eq, C.Ord, C.Show, C.Read) - -data Observation - = AndObs Observation Observation - | OrObs Observation Observation - | NotObs Observation - | ChoseSomething ChoiceId - | ValueGE Value Value - | ValueGT Value Value - | ValueLT Value Value - | ValueLE Value Value - | ValueEQ Value Value - | TrueObs - | FalseObs - deriving (C.Eq, C.Ord, C.Show, C.Read) - -data Party = Address String | Role String - deriving (C.Eq, C.Ord, C.Show, C.Read) - -data Payee = Account Party | Party Party - deriving (C.Eq, C.Ord, C.Show, C.Read) - -data Timeout = Timeout Integer - deriving (C.Eq, C.Ord, C.Show, C.Read) - -data Bound = Bound Integer Integer - deriving (C.Eq, C.Ord, C.Show, C.Read) - -data Token = Token String String - deriving (C.Eq, C.Ord, C.Show, C.Read) - -data ChoiceId = ChoiceId String Party - deriving (C.Eq, C.Ord, C.Show, C.Read) - -data ValueId = ValueId String - deriving (C.Eq, C.Ord, C.Show, C.Read) - diff --git a/haskell/src/Language/Marlowe/Syntax/LexMarlowe.x b/haskell/src/Language/Marlowe/Syntax/LexMarlowe.x deleted file mode 100644 index 392053d3..00000000 --- a/haskell/src/Language/Marlowe/Syntax/LexMarlowe.x +++ /dev/null @@ -1,270 +0,0 @@ --- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.4). - --- Lexer definition for use with Alex 3 -{ -{-# OPTIONS -fno-warn-incomplete-patterns #-} -{-# OPTIONS_GHC -w #-} - -{-# LANGUAGE PatternSynonyms #-} - -module Language.Marlowe.Syntax.LexMarlowe where - -import Prelude - -import qualified Data.ByteString.Char8 as BS -import qualified Data.Bits -import Data.Char (ord) -import Data.Function (on) -import Data.Word (Word8) -} - --- Predefined character classes - -$c = [A-Z\192-\221] # [\215] -- capital isolatin1 letter (215 = \times) FIXME -$s = [a-z\222-\255] # [\247] -- small isolatin1 letter (247 = \div ) FIXME -$l = [$c $s] -- letter -$d = [0-9] -- digit -$i = [$l $d _ '] -- identifier character -$u = [. \n] -- universal: any character - --- Symbols and non-identifier-like reserved words - -@rsyms = \[ | \] | \( | \) | \, - -:- - --- Whitespace (skipped) -$white+ ; - --- Symbols -@rsyms - { tok (eitherResIdent TV) } - --- Keywords and Ident -$l $i* - { tok (eitherResIdent TV) } - --- String -\" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t | r | f)))* \" - { tok (TL . unescapeInitTail) } - --- Integer -$d+ - { tok TI } - -{ --- | Create a token with position. -tok :: (BS.ByteString -> Tok) -> (Posn -> BS.ByteString -> Token) -tok f p = PT p . f - --- | Token without position. -data Tok - = TK {-# UNPACK #-} !TokSymbol -- ^ Reserved word or symbol. - | TL !BS.ByteString -- ^ String literal. - | TI !BS.ByteString -- ^ Integer literal. - | TV !BS.ByteString -- ^ Identifier. - | TD !BS.ByteString -- ^ Float literal. - | TC !BS.ByteString -- ^ Character literal. - deriving (Eq, Show, Ord) - --- | Smart constructor for 'Tok' for the sake of backwards compatibility. -pattern TS :: BS.ByteString -> Int -> Tok -pattern TS t i = TK (TokSymbol t i) - --- | Keyword or symbol tokens have a unique ID. -data TokSymbol = TokSymbol - { tsText :: BS.ByteString - -- ^ Keyword or symbol text. - , tsID :: !Int - -- ^ Unique ID. - } deriving (Show) - --- | Keyword/symbol equality is determined by the unique ID. -instance Eq TokSymbol where (==) = (==) `on` tsID - --- | Keyword/symbol ordering is determined by the unique ID. -instance Ord TokSymbol where compare = compare `on` tsID - --- | Token with position. -data Token - = PT Posn Tok - | Err Posn - deriving (Eq, Show, Ord) - --- | Pretty print a position. -printPosn :: Posn -> String -printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c - --- | Pretty print the position of the first token in the list. -tokenPos :: [Token] -> String -tokenPos (t:_) = printPosn (tokenPosn t) -tokenPos [] = "end of file" - --- | Get the position of a token. -tokenPosn :: Token -> Posn -tokenPosn (PT p _) = p -tokenPosn (Err p) = p - --- | Get line and column of a token. -tokenLineCol :: Token -> (Int, Int) -tokenLineCol = posLineCol . tokenPosn - --- | Get line and column of a position. -posLineCol :: Posn -> (Int, Int) -posLineCol (Pn _ l c) = (l,c) - --- | Convert a token into "position token" form. -mkPosToken :: Token -> ((Int, Int), BS.ByteString) -mkPosToken t = (tokenLineCol t, tokenText t) - --- | Convert a token to its text. -tokenText :: Token -> BS.ByteString -tokenText t = case t of - PT _ (TS s _) -> s - PT _ (TL s) -> BS.pack (show s) - PT _ (TI s) -> s - PT _ (TV s) -> s - PT _ (TD s) -> s - PT _ (TC s) -> s - Err _ -> BS.pack "#error" - --- | Convert a token to a string. -prToken :: Token -> String -prToken t = BS.unpack (tokenText t) - --- | Finite map from text to token organized as binary search tree. -data BTree - = N -- ^ Nil (leaf). - | B BS.ByteString Tok BTree BTree - -- ^ Binary node. - deriving (Show) - --- | Convert potential keyword into token or use fallback conversion. -eitherResIdent :: (BS.ByteString -> Tok) -> BS.ByteString -> Tok -eitherResIdent tv s = treeFind resWords - where - treeFind N = tv s - treeFind (B a t left right) = - case compare s a of - LT -> treeFind left - GT -> treeFind right - EQ -> t - --- | The keywords and symbols of the language organized as binary search tree. -resWords :: BTree -resWords = - b "MerkleizedCase" 24 - (b "Choice" 12 - (b "Address" 6 - (b "," 3 - (b ")" 2 (b "(" 1 N N) N) (b "AddValue" 5 (b "Account" 4 N N) N)) - (b "AvailableMoney" 9 - (b "Assert" 8 (b "AndObs" 7 N N) N) - (b "Case" 11 (b "Bound" 10 N N) N))) - (b "Constant" 18 - (b "ChoseSomething" 15 - (b "ChoiceValue" 14 (b "ChoiceId" 13 N N) N) - (b "Cond" 17 (b "Close" 16 N N) N)) - (b "FalseObs" 21 - (b "DivValue" 20 (b "Deposit" 19 N N) N) - (b "Let" 23 (b "If" 22 N N) N)))) - (b "Token" 36 - (b "Party" 30 - (b "NotObs" 27 - (b "NegValue" 26 (b "MulValue" 25 N N) N) - (b "OrObs" 29 (b "Notify" 28 N N) N)) - (b "SubValue" 33 - (b "Role" 32 (b "Pay" 31 N N) N) - (b "TimeIntervalStart" 35 (b "TimeIntervalEnd" 34 N N) N))) - (b "ValueLE" 42 - (b "ValueEQ" 39 - (b "UseValue" 38 (b "TrueObs" 37 N N) N) - (b "ValueGT" 41 (b "ValueGE" 40 N N) N)) - (b "[" 45 (b "When" 44 (b "ValueLT" 43 N N) N) (b "]" 46 N N)))) - where - b s n = B bs (TS bs n) - where - bs = BS.pack s - --- | Unquote string literal. -unescapeInitTail :: BS.ByteString -> BS.ByteString -unescapeInitTail = BS.pack . unesc . tail . BS.unpack - where - unesc s = case s of - '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs - '\\':'n':cs -> '\n' : unesc cs - '\\':'t':cs -> '\t' : unesc cs - '\\':'r':cs -> '\r' : unesc cs - '\\':'f':cs -> '\f' : unesc cs - '"':[] -> [] - c:cs -> c : unesc cs - _ -> [] - -------------------------------------------------------------------- --- Alex wrapper code. --- A modified "posn" wrapper. -------------------------------------------------------------------- - -data Posn = Pn !Int !Int !Int - deriving (Eq, Show, Ord) - -alexStartPos :: Posn -alexStartPos = Pn 0 1 1 - -alexMove :: Posn -> Char -> Posn -alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1) -alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1 -alexMove (Pn a l c) _ = Pn (a+1) l (c+1) - -type Byte = Word8 - -type AlexInput = (Posn, -- current position, - Char, -- previous char - [Byte], -- pending bytes on the current char - BS.ByteString) -- current input string - -tokens :: BS.ByteString -> [Token] -tokens str = go (alexStartPos, '\n', [], str) - where - go :: AlexInput -> [Token] - go inp@(pos, _, _, str) = - case alexScan inp 0 of - AlexEOF -> [] - AlexError (pos, _, _, _) -> [Err pos] - AlexSkip inp' len -> go inp' - AlexToken inp' len act -> act pos (BS.take len str) : (go inp') - -alexGetByte :: AlexInput -> Maybe (Byte,AlexInput) -alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s)) -alexGetByte (p, _, [], s) = - case BS.uncons s of - Nothing -> Nothing - Just (c,s) -> - let p' = alexMove p c - (b:bs) = utf8Encode c - in p' `seq` Just (b, (p', c, bs, s)) - -alexInputPrevChar :: AlexInput -> Char -alexInputPrevChar (p, c, bs, s) = c - --- | Encode a Haskell String to a list of Word8 values, in UTF8 format. -utf8Encode :: Char -> [Word8] -utf8Encode = map fromIntegral . go . ord - where - go oc - | oc <= 0x7f = [oc] - - | oc <= 0x7ff = [ 0xc0 + (oc `Data.Bits.shiftR` 6) - , 0x80 + oc Data.Bits..&. 0x3f - ] - - | oc <= 0xffff = [ 0xe0 + (oc `Data.Bits.shiftR` 12) - , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f) - , 0x80 + oc Data.Bits..&. 0x3f - ] - | otherwise = [ 0xf0 + (oc `Data.Bits.shiftR` 18) - , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f) - , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f) - , 0x80 + oc Data.Bits..&. 0x3f - ] -} diff --git a/haskell/src/Language/Marlowe/Syntax/ParMarlowe.y b/haskell/src/Language/Marlowe/Syntax/ParMarlowe.y deleted file mode 100644 index ac1d8df3..00000000 --- a/haskell/src/Language/Marlowe/Syntax/ParMarlowe.y +++ /dev/null @@ -1,227 +0,0 @@ --- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.4). - --- Parser definition for use with Happy -{ -{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-} -{-# LANGUAGE PatternSynonyms #-} - -module Language.Marlowe.Syntax.ParMarlowe - ( happyError - , myLexer - , pContract - , pCase - , pListCase - , pAction - , pValue - , pObservation - , pParty - , pPayee - , pTimeout - , pBound - , pListBound - , pToken - , pChoiceId - , pValueId - ) where - -import Prelude - -import qualified Language.Marlowe.Syntax.AbsMarlowe -import Language.Marlowe.Syntax.LexMarlowe -import qualified Data.ByteString.Char8 as BS - -} - -%name pContract Contract -%name pCase Case -%name pListCase ListCase -%name pAction Action -%name pValue Value -%name pObservation Observation -%name pParty Party -%name pPayee Payee -%name pTimeout Timeout -%name pBound Bound -%name pListBound ListBound -%name pToken Token -%name pChoiceId ChoiceId -%name pValueId ValueId --- no lexer declaration -%monad { Err } { (>>=) } { return } -%tokentype {Token} -%token - '(' { PT _ (TS _ 1) } - ')' { PT _ (TS _ 2) } - ',' { PT _ (TS _ 3) } - 'Account' { PT _ (TS _ 4) } - 'AddValue' { PT _ (TS _ 5) } - 'Address' { PT _ (TS _ 6) } - 'AndObs' { PT _ (TS _ 7) } - 'Assert' { PT _ (TS _ 8) } - 'AvailableMoney' { PT _ (TS _ 9) } - 'Bound' { PT _ (TS _ 10) } - 'Case' { PT _ (TS _ 11) } - 'Choice' { PT _ (TS _ 12) } - 'ChoiceId' { PT _ (TS _ 13) } - 'ChoiceValue' { PT _ (TS _ 14) } - 'ChoseSomething' { PT _ (TS _ 15) } - 'Close' { PT _ (TS _ 16) } - 'Cond' { PT _ (TS _ 17) } - 'Constant' { PT _ (TS _ 18) } - 'Deposit' { PT _ (TS _ 19) } - 'DivValue' { PT _ (TS _ 20) } - 'FalseObs' { PT _ (TS _ 21) } - 'If' { PT _ (TS _ 22) } - 'Let' { PT _ (TS _ 23) } - 'MerkleizedCase' { PT _ (TS _ 24) } - 'MulValue' { PT _ (TS _ 25) } - 'NegValue' { PT _ (TS _ 26) } - 'NotObs' { PT _ (TS _ 27) } - 'Notify' { PT _ (TS _ 28) } - 'OrObs' { PT _ (TS _ 29) } - 'Party' { PT _ (TS _ 30) } - 'Pay' { PT _ (TS _ 31) } - 'Role' { PT _ (TS _ 32) } - 'SubValue' { PT _ (TS _ 33) } - 'TimeIntervalEnd' { PT _ (TS _ 34) } - 'TimeIntervalStart' { PT _ (TS _ 35) } - 'Token' { PT _ (TS _ 36) } - 'TrueObs' { PT _ (TS _ 37) } - 'UseValue' { PT _ (TS _ 38) } - 'ValueEQ' { PT _ (TS _ 39) } - 'ValueGE' { PT _ (TS _ 40) } - 'ValueGT' { PT _ (TS _ 41) } - 'ValueLE' { PT _ (TS _ 42) } - 'ValueLT' { PT _ (TS _ 43) } - 'When' { PT _ (TS _ 44) } - '[' { PT _ (TS _ 45) } - ']' { PT _ (TS _ 46) } - L_integ { PT _ (TI $$) } - L_quoted { PT _ (TL $$) } - -%% - -Integer :: { Integer } -Integer : L_integ { (read (BS.unpack $1)) :: Integer } - -String :: { String } -String : L_quoted { (BS.unpack $1) } - -Contract :: { Language.Marlowe.Syntax.AbsMarlowe.Contract } -Contract - : 'Close' { Language.Marlowe.Syntax.AbsMarlowe.Close } - | 'Pay' Party Payee Token Value Contract { Language.Marlowe.Syntax.AbsMarlowe.Pay $2 $3 $4 $5 $6 } - | 'If' Observation Contract Contract { Language.Marlowe.Syntax.AbsMarlowe.If $2 $3 $4 } - | 'When' '[' ListCase ']' Timeout Contract { Language.Marlowe.Syntax.AbsMarlowe.When $3 $5 $6 } - | 'Let' ValueId Value Contract { Language.Marlowe.Syntax.AbsMarlowe.Let $2 $3 $4 } - | 'Assert' Observation Contract { Language.Marlowe.Syntax.AbsMarlowe.Assert $2 $3 } - | '(' Contract ')' { $2 } - -Case :: { Language.Marlowe.Syntax.AbsMarlowe.Case } -Case - : 'Case' Action Contract { Language.Marlowe.Syntax.AbsMarlowe.Case $2 $3 } - | 'MerkleizedCase' Action String { Language.Marlowe.Syntax.AbsMarlowe.MerkleizedCase $2 $3 } - -ListCase :: { [Language.Marlowe.Syntax.AbsMarlowe.Case] } -ListCase - : {- empty -} { [] } - | Case { (:[]) $1 } - | Case ',' ListCase { (:) $1 $3 } - | {- empty -} { [] } - | Case ListCase { (:) $1 $2 } - -Action :: { Language.Marlowe.Syntax.AbsMarlowe.Action } -Action - : 'Deposit' Party Party Token Value { Language.Marlowe.Syntax.AbsMarlowe.Deposit $2 $3 $4 $5 } - | 'Choice' ChoiceId '[' ListBound ']' { Language.Marlowe.Syntax.AbsMarlowe.Choice $2 $4 } - | 'Notify' Observation { Language.Marlowe.Syntax.AbsMarlowe.Notify $2 } - | '(' Action ')' { $2 } - -Value :: { Language.Marlowe.Syntax.AbsMarlowe.Value } -Value - : 'AvailableMoney' Party Token { Language.Marlowe.Syntax.AbsMarlowe.AvailableMoney $2 $3 } - | 'Constant' Integer { Language.Marlowe.Syntax.AbsMarlowe.Constant $2 } - | 'NegValue' Value { Language.Marlowe.Syntax.AbsMarlowe.NegValue $2 } - | 'AddValue' Value Value { Language.Marlowe.Syntax.AbsMarlowe.AddValue $2 $3 } - | 'SubValue' Value Value { Language.Marlowe.Syntax.AbsMarlowe.SubValue $2 $3 } - | 'MulValue' Value Value { Language.Marlowe.Syntax.AbsMarlowe.MulValue $2 $3 } - | 'DivValue' Value Value { Language.Marlowe.Syntax.AbsMarlowe.DivValue $2 $3 } - | 'ChoiceValue' ChoiceId { Language.Marlowe.Syntax.AbsMarlowe.ChoiceValue $2 } - | 'TimeIntervalStart' { Language.Marlowe.Syntax.AbsMarlowe.TimeIntervalStart } - | 'TimeIntervalEnd' { Language.Marlowe.Syntax.AbsMarlowe.TimeIntervalEnd } - | 'UseValue' ValueId { Language.Marlowe.Syntax.AbsMarlowe.UseValue $2 } - | 'Cond' Observation Value Value { Language.Marlowe.Syntax.AbsMarlowe.Cond $2 $3 $4 } - | '(' Value ')' { $2 } - -Observation :: { Language.Marlowe.Syntax.AbsMarlowe.Observation } -Observation - : 'AndObs' Observation Observation { Language.Marlowe.Syntax.AbsMarlowe.AndObs $2 $3 } - | 'OrObs' Observation Observation { Language.Marlowe.Syntax.AbsMarlowe.OrObs $2 $3 } - | 'NotObs' Observation { Language.Marlowe.Syntax.AbsMarlowe.NotObs $2 } - | 'ChoseSomething' ChoiceId { Language.Marlowe.Syntax.AbsMarlowe.ChoseSomething $2 } - | 'ValueGE' Value Value { Language.Marlowe.Syntax.AbsMarlowe.ValueGE $2 $3 } - | 'ValueGT' Value Value { Language.Marlowe.Syntax.AbsMarlowe.ValueGT $2 $3 } - | 'ValueLT' Value Value { Language.Marlowe.Syntax.AbsMarlowe.ValueLT $2 $3 } - | 'ValueLE' Value Value { Language.Marlowe.Syntax.AbsMarlowe.ValueLE $2 $3 } - | 'ValueEQ' Value Value { Language.Marlowe.Syntax.AbsMarlowe.ValueEQ $2 $3 } - | 'TrueObs' { Language.Marlowe.Syntax.AbsMarlowe.TrueObs } - | 'FalseObs' { Language.Marlowe.Syntax.AbsMarlowe.FalseObs } - | '(' Observation ')' { $2 } - -Party :: { Language.Marlowe.Syntax.AbsMarlowe.Party } -Party - : 'Address' String { Language.Marlowe.Syntax.AbsMarlowe.Address $2 } - | 'Role' String { Language.Marlowe.Syntax.AbsMarlowe.Role $2 } - | '(' Party ')' { $2 } - -Payee :: { Language.Marlowe.Syntax.AbsMarlowe.Payee } -Payee - : 'Account' Party { Language.Marlowe.Syntax.AbsMarlowe.Account $2 } - | 'Party' Party { Language.Marlowe.Syntax.AbsMarlowe.Party $2 } - | '(' Payee ')' { $2 } - -Timeout :: { Language.Marlowe.Syntax.AbsMarlowe.Timeout } -Timeout : Integer { Language.Marlowe.Syntax.AbsMarlowe.Timeout $1 } - -Bound :: { Language.Marlowe.Syntax.AbsMarlowe.Bound } -Bound - : 'Bound' Integer Integer { Language.Marlowe.Syntax.AbsMarlowe.Bound $2 $3 } - -ListBound :: { [Language.Marlowe.Syntax.AbsMarlowe.Bound] } -ListBound - : {- empty -} { [] } - | Bound { (:[]) $1 } - | Bound ',' ListBound { (:) $1 $3 } - | {- empty -} { [] } - | Bound ListBound { (:) $1 $2 } - -Token :: { Language.Marlowe.Syntax.AbsMarlowe.Token } -Token - : 'Token' String String { Language.Marlowe.Syntax.AbsMarlowe.Token $2 $3 } - | '(' Token ')' { $2 } - -ChoiceId :: { Language.Marlowe.Syntax.AbsMarlowe.ChoiceId } -ChoiceId - : 'ChoiceId' String Party { Language.Marlowe.Syntax.AbsMarlowe.ChoiceId $2 $3 } - | '(' ChoiceId ')' { $2 } - -ValueId :: { Language.Marlowe.Syntax.AbsMarlowe.ValueId } -ValueId : String { Language.Marlowe.Syntax.AbsMarlowe.ValueId $1 } - -{ - -type Err = Either String - -happyError :: [Token] -> Err a -happyError ts = Left $ - "syntax error at " ++ tokenPos ts ++ - case ts of - [] -> [] - [Err _] -> " due to lexer error" - t:_ -> " before `" ++ (prToken t) ++ "'" - -myLexer :: BS.ByteString -> [Token] -myLexer = tokens - -} - diff --git a/haskell/src/Language/Marlowe/Syntax/Translate.hs b/haskell/src/Language/Marlowe/Syntax/Translate.hs deleted file mode 100644 index b976b24f..00000000 --- a/haskell/src/Language/Marlowe/Syntax/Translate.hs +++ /dev/null @@ -1,91 +0,0 @@ -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE FlexibleInstances #-} - -module Language.Marlowe.Syntax.Translate where - -import Language.Marlowe.Syntax.AbsMarlowe -import qualified Language.Marlowe.Semantics.Types as S -import Data.ByteString (ByteString) -import Data.ByteString.Char8 as BS (pack) -import Data.Text as T (Text, pack) - -class Translate a b where - translate :: a -> b - -instance Translate Value S.Value where - translate (Constant c) = S.Constant c - translate (AvailableMoney accId tok) = S.AvailableMoney (translate accId) (translate tok) - translate (NegValue v) = S.NegValue $ translate v - translate (AddValue lhs rhs) = S.AddValue (translate lhs) (translate rhs) - translate (SubValue lhs rhs) = S.SubValue (translate lhs) (translate rhs) - translate (MulValue lhs rhs) = S.MulValue (translate lhs) (translate rhs) - translate (DivValue lhs rhs) = S.DivValue (translate lhs) (translate rhs) - translate (ChoiceValue choId) = S.ChoiceValue (translate choId) - translate TimeIntervalStart = S.TimeIntervalStart - translate TimeIntervalEnd = S.TimeIntervalEnd - translate (UseValue vId) = S.UseValue (translate vId) - translate (Cond obs lhs rhs) = S.Cond (translate obs) (translate lhs) (translate rhs) - -instance Translate Observation S.Observation where - translate (AndObs lhs rhs) = S.AndObs (translate lhs) (translate rhs) - translate (OrObs lhs rhs) = S.OrObs (translate lhs) (translate rhs) - translate (NotObs v) = S.NotObs $ translate v - translate (ChoseSomething choId) = S.ChoseSomething (translate choId) - translate (ValueGE lhs rhs) = S.ValueGE (translate lhs) (translate rhs) - translate (ValueGT lhs rhs) = S.ValueGT (translate lhs) (translate rhs) - translate (ValueLT lhs rhs) = S.ValueLT (translate lhs) (translate rhs) - translate (ValueLE lhs rhs) = S.ValueLE (translate lhs) (translate rhs) - translate (ValueEQ lhs rhs) = S.ValueEQ (translate lhs) (translate rhs) - translate TrueObs = S.TrueObs - translate FalseObs = S.FalseObs - -instance Translate Action S.Action where - translate (Deposit accId party tok val) = S.Deposit (translate accId) (translate party) (translate tok) (translate val) - translate (Choice choId bounds) = S.Choice (translate choId) (translate bounds) - translate (Notify obs) = S.Notify $ translate obs - -instance Translate Contract S.Contract where - translate Close = S.Close - translate (Pay accountId payee token value contract) = S.Pay (translate accountId) (translate payee) (translate token) (translate value) (translate contract) - translate (If obs contract1 contract2) = S.If (translate obs) (translate contract1) (translate contract2) - translate (When cases timeout contract) = S.When (translate <$> cases) (translate timeout) (translate contract) - translate (Let valueId val contract) = S.Let (translate valueId) (translate val) (translate contract) - translate (Assert obs contract) = S.Assert (translate obs) (translate contract) - -instance Translate a b => Translate [a] [b] where - translate = fmap translate - -instance Translate String ByteString where - translate = BS.pack - -instance Translate String Text where - translate = T.pack - -instance Translate Case S.Case where - translate (Case action contract) = S.Case (translate action) (translate contract) - translate (MerkleizedCase action hash) = S.MerkleizedCase (translate action) (translate hash) - -instance Translate Timeout S.Timeout where - translate (Timeout i) = S.POSIXTime i - -instance Translate Party S.Party where - translate (Address address) = S.Address (translate address) - translate (Role role) = S.Role (translate role) - -instance Translate Bound S.Bound where - translate (Bound i j) = S.Bound i j - -instance Translate ValueId S.ValueId where - translate (ValueId valueId) = S.ValueId (translate valueId) - -instance Translate ChoiceId S.ChoiceId where - translate (ChoiceId choiceId party) = S.ChoiceId (translate choiceId) (translate party) - -instance Translate Token S.Token where - translate (Token currencySymbol tokenName) = S.Token (translate currencySymbol) (translate tokenName) - -type AccountId = Party - -instance Translate Payee S.Payee where - translate (Account accountId) = S.Account (translate accountId) - translate (Party party) = S.Party (translate party) diff --git a/nix/scripts.nix b/nix/scripts.nix index 5e81f48a..835544f7 100644 --- a/nix/scripts.nix +++ b/nix/scripts.nix @@ -24,7 +24,6 @@ isabelle build -v -b -d isabelle StaticAnalysis ''; - build-marlowe-docs = writeShellScriptBinInRepoRoot "build-marlowe-docs" '' echo "Generating Literate Haskell Tex" lhs2TeX isabelle/haskell/MarloweCoreJson.lhs | sed '1,/PATTERN FOR SED/d' > isabelle/Doc/Specification/document/marlowe-core-json.tex @@ -33,8 +32,15 @@ isabelle document -v -V -d isabelle -P papers Cheatsheet isabelle document -v -V -d isabelle -P papers Specification ''; + edit-marlowe-proofs = writeShellScriptBinInRepoRoot "edit-marlowe-proofs" '' cd isabelle isabelle jedit -d . -u Doc/Specification/Specification.thy ''; + + generate-marlowe-language-specification = writeShellScriptBinInRepoRoot "generate-marlowe-language-specification" '' + ROOT=papers/language_specification + bnfc --latex -o $ROOT $ROOT/Marlowe.cf + pdflatex --output-directory $ROOT $ROOT/Marlowe.tex + ''; } diff --git a/haskell/src/Language/Marlowe/Syntax/Marlowe.cf b/papers/language_specification/Marlowe.cf similarity index 100% rename from haskell/src/Language/Marlowe/Syntax/Marlowe.cf rename to papers/language_specification/Marlowe.cf