digital-asset/daml
1
1
Fork 0
mirror of https://github.com/digital-asset/daml.git synced 2024-09-20 01:07:18 +03:00
Code Issues Projects Releases Wiki Activity

Add interfaces to LF spec (#13020)

Browse Source 
* Add interfaces to LF spec.

Part of #11349. This PR adds the interface & implements declarations, deals with "requires", and name collisions. I'm leaving expression types and operational semantics to a future PR.

changelog_begin
changelog_end

* missing curly

* change T to I for interfaces

* revisions from Remy
This commit is contained in:
Sofia Faro 2022-02-24 17:09:20 +00:00 committed by GitHub
parent 0ea4866adc
commit 0e03e2f100
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 71 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

76
daml-lf/spec/daml-lf-1.rst
View File

@ -439,7 +439,7 @@ strings as *package identifiers*. ::
W ::= Name -- ValRef
Type constructors
T ::= Name -- TyCon
T, I ::= Name -- TyCon
Type synonym
S ::= Name -- TySyn
@ -761,6 +761,12 @@ available for usage::
ChDef ::= 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ e
-- ChDef
Interface implementation definition
ImplDef ::= 'implements' Mod:I -- ImplDef [Daml-LF ≥ 1.dev]
{ 'methods { f₁ = e₁, …, fₙ = eₙ }
, 'choices' { Ch₁, …, Chₘ }
}
Definitions
Def
::=
@ -778,8 +784,15 @@ available for usage::
, 'agreement' e₄
, 'choices' { ChDef₁, …, ChDefₘ }
, KeyDef
, ImplDef₁, …, ImplDefₖ
}
| 'exception' T ↦ { 'message' e } -- DefException [Daml-LF ≥ 1.14]
| 'interface' (x : I) ↦ -- DefInterface [Daml-LF ≥ 1.dev]
{ 'requires' { Mod₁:I₁, …, Modₖ:Iₖ }
, 'precondition' e
, 'methods' { f₁ : τ₁, …, fₙ : τₙ }
, 'choices' { ChDef₁, …, ChDefₘ }
}
Module (mnemonic: delta for definitions)
Δ ::= ε -- DefCtxEmpty
@ -998,6 +1011,10 @@ We now formally define *well-formed types*. ::
————————————————————————————————————————————— TyEnumCon
Γ ⊢ Mod:T : ⋆
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
————————————————————————————————————————————— TyInterfaceCon
Γ ⊢ Mod:I : ⋆
Γ ⊢ τ₁ : ⋆ … Γ ⊢ τₙ : ⋆
f₁ < … < fₙ lexicographically
————————————————————————————————————————————— TyStruct
@ -1541,15 +1558,15 @@ for the ``DefTemplate`` rule). ::
Well-formed definitions │ ⊢ Def │
└────────┘
τ ↠ τ₁' αₙ : kₙ · … · α₁ : k₁ ⊢ τ₁' : ⋆
τ₁ ↠ τ₁' αₙ : kₙ · … · α₁ : k₁ ⊢ τ₁' : ⋆
⋮
τ ↠ τₘ' αₙ : kₙ · … · α₁ : k₁ ⊢ τₘ' : ⋆
τₘ ↠ τₘ' αₙ : kₙ · … · α₁ : k₁ ⊢ τₘ' : ⋆
——————————————————————————————————————————————————————————————— DefRec
⊢ 'record' T (α₁: k₁) … (αₙ: kₙ) ↦ { f₁: τ₁, …, fₘ: τₘ }
τ ↠ τ₁' αₙ : kₙ · … · α₁ : k₁ ⊢ τ₁' : ⋆
τ₁ ↠ τ₁' αₙ : kₙ · … · α₁ : k₁ ⊢ τ₁' : ⋆
⋮
τ ↠ τₘ' αₙ : kₙ · … · α₁ : k₁ ⊢ τₘ' : ⋆
τₘ ↠ τₘ' αₙ : kₙ · … · α₁ : k₁ ⊢ τₘ' : ⋆
——————————————————————————————————————————————————————————————— DefVariant
⊢ 'record' T (α₁: k₁) … (αₙ: kₙ) ↦ V₁: τ₁ | … | Vₘ: τₘ
@ -1572,6 +1589,7 @@ for the ``DefTemplate`` rule). ::
x : Mod:T ⊢ eₐ : 'Text'
x : Mod:T ⊢ ChDef₁ ⋯ x : Mod:T ⊢ ChDefₘ
x : Mod:T ⊢ KeyDef
x : Mod:T ⊢ ImplDef₁ ⋯ x : Mod:T ⊢ ImplDefₖ
——————————————————————————————————————————————————————————————— DefTemplate
⊢ 'tpl' (x : T) ↦
{ 'precondition' eₚ
@ -1580,6 +1598,7 @@ for the ``DefTemplate`` rule). ::
, 'agreement' eₐ
, 'choices' { ChDef₁, …, ChDefₘ }
, KeyDef
, ImplDef₁, …, ImplDefₖ
}
'record' T ↦ { f₁ : τ₁, …, fₙ : τₙ } ∈ 〚Ξ〛Mod
@ -1588,6 +1607,23 @@ for the ``DefTemplate`` rule). ::
——————————————————————————————————————————————————————————————— DefException [Daml-LF ≥ 1.14]
⊢ 'exception' T ↦ { 'message' e }
Mod:I ∉ { Mod₁:I₁, …, Modₖ:Iₖ }
'interface' (x₁ : I₁) ↦ { 'requires' R₁ , … } ∈ 〚Ξ〛Mod₁ R₁ ⊆ { Mod₁:I₁, …, Modₖ:Iₖ }
⋮
'interface' (xₖ : Iₖ) ↦ { 'requires' Rₖ , … } ∈ 〚Ξ〛Modₖ Rₖ ⊆ { Mod₁:I₁, …, Modₖ:Iₖ }
x : Mod:I ⊢ eₚ : 'Bool'
τ₁ ↠ τ₁' ⊢ τ₁' : ⋆
⋮
τₙ ↠ τₙ' ⊢ τₙ' : ⋆
x : Mod:I ⊢ ChDef₁ ⋯ x : Mod:I ⊢ ChDefₘ
——————————————————————————————————————————————————————————————— DefInterface [Daml-LF ≥ 1.dev]
⊢ 'interface' (x : I) ↦
{ 'requires' { Mod₁:I₁, …, Modₖ:Iₖ }
, 'precondition' eₚ
, 'methods' { f₁ : τ₁, …, fₙ : τₙ }
, 'choices' { ChDef₁, …, ChDefₘ }
}
┌───────────────────┐
Well-formed choices │ x : Mod:T ⊢ ChDef │
└───────────────────┘
@ -1599,6 +1635,27 @@ for the ``DefTemplate`` rule). ::
——————————————————————————————————————————————————————————————— ChDef
x : Mod:T ⊢ 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ e
┌─────────────────────┐
Well-formed interface implementations │ x : Mod:T ⊢ ImplDef │
└─────────────────────┘
'interface' (y : I) ↦
{ 'requires' R
, 'precondition' eₚ
, 'methods' { f₁ : τ₁, …, fₘ = τₘ }
, 'choices' { 'choice' ChKind₁ Ch₁ …, …, 'choice' ChKindₘ Chₘ … }
} ∈ 〚Ξ〛Mod'
'tpl' (x : T) ↦ { …, 'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
R ⊆ { Mod₁:I₁, …, Modₖ:Iₖ }
τ₁ ↠ τ₁' x : Mod:T ⊢ e₁ : τ₁'
⋮
τₘ ↠ τₘ' x : Mod:T ⊢ eₘ : τₘ'
——————————————————————————————————————————————————————————————— ImplDef
x : Mod:T ⊢ 'implements' Mod':I
{ 'methods' { f₁ = e₁, …, fₙ = eₙ }
, 'choices' { Ch₁, …, Chₘ }
}
┌────────────┐
Valid key │ ⊢ₖ e : τ │
└────────────┘
@ -1713,6 +1770,15 @@ name* construct as follows:
* The *fully resolved name* of a choice ``Ch`` of a template
definition ``'tpl' (x : T) ↦ { …, 'choices' { …, 'choice' ChKind Ch
… ↦ …, … } }`` defined in the module ``Mod`` is ``Mod.T.Ch``.
* The *fully resolved name* of an inherited choice ``Ch`` of a template
definition ``'tpl' (x : T) ↦ { …, 'implements' { …, 'choices' { …, Ch,
… } } }`` defined in the module ``Mod`` is ``Mod.T.Ch``.
* The *fully resolved name* of a choice ``Ch`` of an interface
definition ``'interface' (x : I) ↦ { …, 'choices' { …, 'choice' ChKind Ch
… ↦ …, … } }`` defined in the module ``Mod`` is ``Mod.I.Ch``.
* The *fully resolved name* of a method ``fᵢ`` of an interface
definition ``'interface' (x : I) ↦ { …, 'methods' { …, fᵢ: τᵢ, … } }``
defined in the module ``Mod`` is ``Mod.I.fᵢ``.
Name collisions