diff --git a/eo b/eo new file mode 160000 index 000000000..33bb3b6c6 --- /dev/null +++ b/eo @@ -0,0 +1 @@ +Subproject commit 33bb3b6c6bd5a2df6b641d364d8d841a967687c3 diff --git a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf index 29d0d171f..ba0a995a8 100644 --- a/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf +++ b/eo-phi-normalizer/grammar/EO/Phi/Syntax.cf @@ -11,7 +11,7 @@ token AlphaIndex ({"α0"} | {"α"} (digit - ["0"]) (digit)* ) ; token MetaId {"!"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ; token MetaFunctionName {"@"} (char - [" \r\n\t,.|':;!-?][}{)(⟧⟦"])* ; -Program. Program ::= "{" [Binding] "}" ; +Program. Program ::= "{" "⟦" [Binding] "⟧" "}" ; Formation. Object ::= "⟦" [Binding] "⟧" ; Application. Object ::= Object "(" [Binding] ")" ; diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt index a80517a82..8d38f607b 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt @@ -1,104 +1,104 @@ -The Language Syntax -BNF Converter - - -%Process by txt2tags to generate html or latex - - - -This document was automatically generated by the //BNF-Converter//. It was generated together with the lexer, the parser, and the abstract syntax module, which guarantees that the document matches with the implementation of the language (provided no hand-hacking has taken place). - -==The lexical structure of Syntax== - -===Literals=== - - - - - - - -Bytes literals are recognized by the regular expression -`````{"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] '-' | ["0123456789ABCDEF"] ["0123456789ABCDEF"] ('-' ["0123456789ABCDEF"] ["0123456789ABCDEF"])+````` - -Function literals are recognized by the regular expression -`````upper (char - [" - !'(),-.:;?[]{|}⟦⟧"])*````` - -LabelId literals are recognized by the regular expression -`````lower (char - [" - !'(),.:;?[]{|}⟦⟧"])*````` - -AlphaIndex literals are recognized by the regular expression -`````{"α0"} | 'α' (digit - '0') digit*````` - -MetaId literals are recognized by the regular expression -`````'!' (char - [" - !'(),-.:;?[]{|}⟦⟧"])*````` - -MetaFunctionName literals are recognized by the regular expression -`````'@' (char - [" - !'(),-.:;?[]{|}⟦⟧"])*````` - - -===Reserved words and symbols=== -The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions. - -The reserved words used in Syntax are the following: - | ``Δ`` | ``Φ`` | ``λ`` | ``ν`` - | ``ξ`` | ``ρ`` | ``σ`` | ``φ`` - -The symbols used in Syntax are the following: - | { | } | ⟦ | ⟧ - | ( | ) | . | ⊥ - | ↦ | ∅ | ⤍ | , - -===Comments=== -There are no single-line comments in the grammar.There are no multiple-line comments in the grammar. - -==The syntactic structure of Syntax== -Non-terminals are enclosed between < and >. -The symbols -> (production), **|** (union) -and **eps** (empty rule) belong to the BNF notation. -All other symbols are terminals. - - | //Program// | -> | ``{`` //[Binding]// ``}`` - | //Object// | -> | ``⟦`` //[Binding]// ``⟧`` - | | **|** | //Object// ``(`` //[Binding]// ``)`` - | | **|** | //Object// ``.`` //Attribute// - | | **|** | ``Φ`` - | | **|** | ``ξ`` - | | **|** | ``⊥`` - | | **|** | //MetaId// - | | **|** | //MetaFunctionName// ``(`` //Object// ``)`` - | //Binding// | -> | //Attribute// ``↦`` //Object// - | | **|** | //Attribute// ``↦`` ``∅`` - | | **|** | ``Δ`` ``⤍`` //Bytes// - | | **|** | ``λ`` ``⤍`` //Function// - | | **|** | //MetaId// - | //[Binding]// | -> | **eps** - | | **|** | //Binding// - | | **|** | //Binding// ``,`` //[Binding]// - | //Attribute// | -> | ``φ`` - | | **|** | ``ρ`` - | | **|** | ``σ`` - | | **|** | ``ν`` - | | **|** | //LabelId// - | | **|** | //AlphaIndex// - | | **|** | //MetaId// - | //RuleAttribute// | -> | //Attribute// - | | **|** | ``Δ`` - | | **|** | ``λ`` - | //PeeledObject// | -> | //ObjectHead// //[ObjectAction]// - | //ObjectHead// | -> | ``⟦`` //[Binding]// ``⟧`` - | | **|** | ``Φ`` - | | **|** | ``ξ`` - | | **|** | ``⊥`` - | //ObjectAction// | -> | ``(`` //[Binding]// ``)`` - | | **|** | ``.`` //Attribute// - | //[ObjectAction]// | -> | **eps** - | | **|** | //ObjectAction// //[ObjectAction]// - - - -%% File generated by the BNF Converter (bnfc 2.9.5). +The Language Syntax +BNF Converter + + +%Process by txt2tags to generate html or latex + + + +This document was automatically generated by the //BNF-Converter//. It was generated together with the lexer, the parser, and the abstract syntax module, which guarantees that the document matches with the implementation of the language (provided no hand-hacking has taken place). + +==The lexical structure of Syntax== + +===Literals=== + + + + + + + +Bytes literals are recognized by the regular expression +`````{"--"} | ["0123456789ABCDEF"] ["0123456789ABCDEF"] '-' | ["0123456789ABCDEF"] ["0123456789ABCDEF"] ('-' ["0123456789ABCDEF"] ["0123456789ABCDEF"])+````` + +Function literals are recognized by the regular expression +`````upper (char - [" + !'(),-.:;?[]{|}⟦⟧"])*````` + +LabelId literals are recognized by the regular expression +`````lower (char - [" + !'(),.:;?[]{|}⟦⟧"])*````` + +AlphaIndex literals are recognized by the regular expression +`````{"α0"} | 'α' (digit - '0') digit*````` + +MetaId literals are recognized by the regular expression +`````'!' (char - [" + !'(),-.:;?[]{|}⟦⟧"])*````` + +MetaFunctionName literals are recognized by the regular expression +`````'@' (char - [" + !'(),-.:;?[]{|}⟦⟧"])*````` + + +===Reserved words and symbols=== +The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions. + +The reserved words used in Syntax are the following: + | ``Δ`` | ``Φ`` | ``λ`` | ``ν`` + | ``ξ`` | ``ρ`` | ``σ`` | ``φ`` + +The symbols used in Syntax are the following: + | { | ⟦ | ⟧ | } + | ( | ) | . | ⊥ + | ↦ | ∅ | ⤍ | , + +===Comments=== +There are no single-line comments in the grammar.There are no multiple-line comments in the grammar. + +==The syntactic structure of Syntax== +Non-terminals are enclosed between < and >. +The symbols -> (production), **|** (union) +and **eps** (empty rule) belong to the BNF notation. +All other symbols are terminals. + + | //Program// | -> | ``{`` ``⟦`` //[Binding]// ``⟧`` ``}`` + | //Object// | -> | ``⟦`` //[Binding]// ``⟧`` + | | **|** | //Object// ``(`` //[Binding]// ``)`` + | | **|** | //Object// ``.`` //Attribute// + | | **|** | ``Φ`` + | | **|** | ``ξ`` + | | **|** | ``⊥`` + | | **|** | //MetaId// + | | **|** | //MetaFunctionName// ``(`` //Object// ``)`` + | //Binding// | -> | //Attribute// ``↦`` //Object// + | | **|** | //Attribute// ``↦`` ``∅`` + | | **|** | ``Δ`` ``⤍`` //Bytes// + | | **|** | ``λ`` ``⤍`` //Function// + | | **|** | //MetaId// + | //[Binding]// | -> | **eps** + | | **|** | //Binding// + | | **|** | //Binding// ``,`` //[Binding]// + | //Attribute// | -> | ``φ`` + | | **|** | ``ρ`` + | | **|** | ``σ`` + | | **|** | ``ν`` + | | **|** | //LabelId// + | | **|** | //AlphaIndex// + | | **|** | //MetaId// + | //RuleAttribute// | -> | //Attribute// + | | **|** | ``Δ`` + | | **|** | ``λ`` + | //PeeledObject// | -> | //ObjectHead// //[ObjectAction]// + | //ObjectHead// | -> | ``⟦`` //[Binding]// ``⟧`` + | | **|** | ``Φ`` + | | **|** | ``ξ`` + | | **|** | ``⊥`` + | //ObjectAction// | -> | ``(`` //[Binding]// ``)`` + | | **|** | ``.`` //Attribute// + | //[ObjectAction]// | -> | **eps** + | | **|** | //ObjectAction// //[ObjectAction]// + + + +%% File generated by the BNF Converter (bnfc 2.9.5). diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x index 44a8ecd8e..080e6b0a0 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x @@ -28,7 +28,7 @@ $u = [. \n] -- universal: any character -- Symbols and non-identifier-like reserved words -@rsyms = \Φ | \ξ | \Δ | \λ | \φ | \ρ | \σ | \ν | \{ | \} | \⟦ | \⟧ | \( | \) | \. | \⊥ | \↦ | \∅ | \⤍ | \, +@rsyms = \Φ | \ξ | \Δ | \λ | \φ | \ρ | \σ | \ν | \{ | \⟦ | \⟧ | \} | \( | \) | \. | \⊥ | \↦ | \∅ | \⤍ | \, :- diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y index 4deb4ab03..144354aa0 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y @@ -90,7 +90,7 @@ MetaFunctionName : L_MetaFunctionName { Language.EO.Phi.Syntax.Abs.MetaFunction Program :: { Language.EO.Phi.Syntax.Abs.Program } Program - : '{' ListBinding '}' { Language.EO.Phi.Syntax.Abs.Program $2 } + : '{' '⟦' ListBinding '⟧' '}' { Language.EO.Phi.Syntax.Abs.Program $3 } Object :: { Language.EO.Phi.Syntax.Abs.Object } Object diff --git a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs index cef0892d5..112ffea63 100644 --- a/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs +++ b/eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs @@ -151,7 +151,7 @@ instance Print Language.EO.Phi.Syntax.Abs.MetaFunctionName where prt _ (Language.EO.Phi.Syntax.Abs.MetaFunctionName i) = doc $ showString i instance Print Language.EO.Phi.Syntax.Abs.Program where prt i = \case - Language.EO.Phi.Syntax.Abs.Program bindings -> prPrec i 0 (concatD [doc (showString "{"), prt 0 bindings, doc (showString "}")]) + Language.EO.Phi.Syntax.Abs.Program bindings -> prPrec i 0 (concatD [doc (showString "{"), doc (showString "\10214"), prt 0 bindings, doc (showString "\10215"), doc (showString "}")]) instance Print Language.EO.Phi.Syntax.Abs.Object where prt i = \case diff --git a/eo-phi-normalizer/test/eo/phi/from-eo/as-phi.yaml b/eo-phi-normalizer/test/eo/phi/from-eo/as-phi.yaml index 1469533f9..54bda82dc 100644 --- a/eo-phi-normalizer/test/eo/phi/from-eo/as-phi.yaml +++ b/eo-phi-normalizer/test/eo/phi/from-eo/as-phi.yaml @@ -2,8 +2,8 @@ title: Processing terms generated from EO tests: - name: "A program that prints itself" input: | - {org ↦ ⟦eolang ↦ ⟦prints-itself ↦ ⟦φ ↦ Φ.org.eolang.as-phi(α0 ↦ ξ).length.gt(α0 ↦ Φ.org.eolang.int(α0 ↦ Φ.org.eolang.bytes(Δ ⤍ 00-00-00-00-00-00-00-00)))⟧, prints-itself-to-console ↦ ⟦x ↦ Φ.org.eolang.int(α0 ↦ Φ.org.eolang.bytes(Δ ⤍ 00-00-00-00-00-00-00-2A)), φ ↦ Φ.org.eolang.io.stdout(α0 ↦ Φ.org.eolang.as-phi(α0 ↦ ξ))⟧, λ ⤍ Package⟧, λ ⤍ Package⟧} + {⟦org ↦ ⟦eolang ↦ ⟦prints-itself ↦ ⟦φ ↦ Φ.org.eolang.as-phi(α0 ↦ ξ).length.gt(α0 ↦ Φ.org.eolang.int(α0 ↦ Φ.org.eolang.bytes(Δ ⤍ 00-00-00-00-00-00-00-00)))⟧, prints-itself-to-console ↦ ⟦x ↦ Φ.org.eolang.int(α0 ↦ Φ.org.eolang.bytes(Δ ⤍ 00-00-00-00-00-00-00-2A)), φ ↦ Φ.org.eolang.io.stdout(α0 ↦ Φ.org.eolang.as-phi(α0 ↦ ξ))⟧, λ ⤍ Package⟧, λ ⤍ Package⟧⟧} normalized: | - { ν ↦ ⟦ Δ ⤍ 04- ⟧, org ↦ ⟦ ν ↦ ⟦ Δ ⤍ 03- ⟧, eolang ↦ ⟦ ν ↦ ⟦ Δ ⤍ 02- ⟧, prints-itself ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧, φ ↦ Φ.org.eolang.as-phi (α0 ↦ ξ).length.gt (α0 ↦ Φ.org.eolang.int (α0 ↦ Φ.org.eolang.bytes (Δ ⤍ 00-00-00-00-00-00-00-00))) ⟧, prints-itself-to-console ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, x ↦ Φ.org.eolang.int (α0 ↦ Φ.org.eolang.bytes (Δ ⤍ 00-00-00-00-00-00-00-2A)), φ ↦ Φ.org.eolang.io.stdout (α0 ↦ Φ.org.eolang.as-phi (α0 ↦ ξ)) ⟧, λ ⤍ Package ⟧, λ ⤍ Package ⟧ } + { ⟦ ν ↦ ⟦ Δ ⤍ 04- ⟧, org ↦ ⟦ ν ↦ ⟦ Δ ⤍ 03- ⟧, eolang ↦ ⟦ ν ↦ ⟦ Δ ⤍ 02- ⟧, prints-itself ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧, φ ↦ Φ.org.eolang.as-phi (α0 ↦ ξ).length.gt (α0 ↦ Φ.org.eolang.int (α0 ↦ Φ.org.eolang.bytes (Δ ⤍ 00-00-00-00-00-00-00-00))) ⟧, prints-itself-to-console ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, x ↦ Φ.org.eolang.int (α0 ↦ Φ.org.eolang.bytes (Δ ⤍ 00-00-00-00-00-00-00-2A)), φ ↦ Φ.org.eolang.io.stdout (α0 ↦ Φ.org.eolang.as-phi (α0 ↦ ξ)) ⟧, λ ⤍ Package ⟧, λ ⤍ Package ⟧ ⟧ } prettified: | - { org ↦ ⟦ eolang ↦ ⟦ prints-itself ↦ ⟦ φ ↦ Φ.org.eolang.as-phi (α0 ↦ ξ).length.gt (α0 ↦ Φ.org.eolang.int (α0 ↦ Φ.org.eolang.bytes (Δ ⤍ 00-00-00-00-00-00-00-00))) ⟧, prints-itself-to-console ↦ ⟦ x ↦ Φ.org.eolang.int (α0 ↦ Φ.org.eolang.bytes (Δ ⤍ 00-00-00-00-00-00-00-2A)), φ ↦ Φ.org.eolang.io.stdout (α0 ↦ Φ.org.eolang.as-phi (α0 ↦ ξ)) ⟧, λ ⤍ Package ⟧, λ ⤍ Package ⟧ } + { ⟦ org ↦ ⟦ eolang ↦ ⟦ prints-itself ↦ ⟦ φ ↦ Φ.org.eolang.as-phi (α0 ↦ ξ).length.gt (α0 ↦ Φ.org.eolang.int (α0 ↦ Φ.org.eolang.bytes (Δ ⤍ 00-00-00-00-00-00-00-00))) ⟧, prints-itself-to-console ↦ ⟦ x ↦ Φ.org.eolang.int (α0 ↦ Φ.org.eolang.bytes (Δ ⤍ 00-00-00-00-00-00-00-2A)), φ ↦ Φ.org.eolang.io.stdout (α0 ↦ Φ.org.eolang.as-phi (α0 ↦ ξ)) ⟧, λ ⤍ Package ⟧, λ ⤍ Package ⟧ ⟧ } diff --git a/eo-phi-normalizer/test/eo/phi/metrics.yaml b/eo-phi-normalizer/test/eo/phi/metrics.yaml index 5a3858017..b23075374 100644 --- a/eo-phi-normalizer/test/eo/phi/metrics.yaml +++ b/eo-phi-normalizer/test/eo/phi/metrics.yaml @@ -2,36 +2,37 @@ title: Metrics tests tests: - title: prints-itself phi: | - { - org ↦ ⟦ - eolang ↦ ⟦ - prints-itself ↦ ⟦ - φ ↦ - Φ.org.eolang.as-phi( - α0 ↦ ξ - ).length.gt( - α0 ↦ Φ.org.eolang.int( - α0 ↦ Φ.org.eolang.bytes( - Δ ⤍ 00-00-00-00-00-00-00-00 + { ⟦ + org ↦ ⟦ + eolang ↦ ⟦ + prints-itself ↦ ⟦ + φ ↦ + Φ.org.eolang.as-phi( + α0 ↦ ξ + ).length.gt( + α0 ↦ Φ.org.eolang.int( + α0 ↦ Φ.org.eolang.bytes( + Δ ⤍ 00-00-00-00-00-00-00-00 + ) ) ) + ⟧, + prints-itself-to-console ↦ ⟦ + x ↦ Φ.org.eolang.int( + α0 ↦ Φ.org.eolang.bytes( + Δ ⤍ 00-00-00-00-00-00-00-2A + ) + ), + φ ↦ Φ.org.eolang.io.stdout( + α0 ↦ Φ.org.eolang.as-phi( + α0 ↦ ξ + ) ) - ⟧, - prints-itself-to-console ↦ ⟦ - x ↦ Φ.org.eolang.int( - α0 ↦ Φ.org.eolang.bytes( - Δ ⤍ 00-00-00-00-00-00-00-2A - ) - ), - φ ↦ Φ.org.eolang.io.stdout( - α0 ↦ Φ.org.eolang.as-phi( - α0 ↦ ξ - ) - ) + ⟧, + λ ⤍ Package ⟧, λ ⤍ Package - ⟧, - λ ⤍ Package + ⟧ ⟧ } metrics: diff --git a/eo-phi-normalizer/test/eo/phi/rule-1.yaml b/eo-phi-normalizer/test/eo/phi/rule-1.yaml index 9c001884b..8b1afe3b9 100644 --- a/eo-phi-normalizer/test/eo/phi/rule-1.yaml +++ b/eo-phi-normalizer/test/eo/phi/rule-1.yaml @@ -2,24 +2,24 @@ title: Tests for Rule 1 tests: - name: 'Program without vertices (1)' input: | - {a ↦ ⟦ ⟧ } + {⟦ a ↦ ⟦ ⟧ ⟧} normalized: | - { a ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ } + { ⟦ a ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧ } prettified: | - { } + { ⟦ a ↦ ⟦ ⟧ ⟧ } - name: 'Program without vertices (2)' input: | - { a ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ ⟧ } + { ⟦ a ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ ⟧ ⟧ } normalized: | - { a ↦ ⟦ ν ↦ ⟦ Δ ⤍ 03- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 02- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧ ⟧ ⟧ } + { ⟦ a ↦ ⟦ ν ↦ ⟦ Δ ⤍ 03- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 02- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧ ⟧ ⟧ ⟧ ⟧ } prettified: | - { a ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ ⟧ } + { ⟦ a ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ ⟧ ⟧ ⟧ ⟧ ⟧ } - name: 'Program without vertices (3)' input: | - { a ↦ ⟦ φ ↦ ⟦ ⟧ , a ↦ ξ.φ ⟧ } + { ⟦ a ↦ ⟦ φ ↦ ⟦ ⟧ , a ↦ ξ.φ ⟧ ⟧ } normalized: | - { a ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, a ↦ ξ.φ ⟧ } + { ⟦ a ↦ ⟦ ν ↦ ⟦ Δ ⤍ 01- ⟧, φ ↦ ⟦ ν ↦ ⟦ Δ ⤍ 00- ⟧ ⟧, a ↦ ξ.φ ⟧ ⟧ } prettified: | - { a ↦ ⟦ φ ↦ ⟦ ⟧, a ↦ ξ.φ ⟧ } + { ⟦ a ↦ ⟦ φ ↦ ⟦ ⟧, a ↦ ξ.φ ⟧ ⟧ } diff --git a/eo-phi-normalizer/test/eo/phi/rule-6.yaml b/eo-phi-normalizer/test/eo/phi/rule-6.yaml index d48273e10..26371c8df 100644 --- a/eo-phi-normalizer/test/eo/phi/rule-6.yaml +++ b/eo-phi-normalizer/test/eo/phi/rule-6.yaml @@ -2,14 +2,14 @@ title: Tests for Rule 6 tests: - name: "Case (1)" input: | - { a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b } + { ⟦ a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b ⟧ } normalized: | - { a ↦ ⟦ Δ ⤍ 00- ⟧(ρ ↦ ⟦ c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧) } + { ⟦ a ↦ ⟦ Δ ⤍ 00- ⟧(ρ ↦ ⟦ c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧) ⟧ } prettified: | - { a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b } + { ⟦ a ↦ ⟦ b ↦ ⟦ Δ ⤍ 00- ⟧, c ↦ ⟦ Δ ⤍ 03- ⟧ ⟧.b ⟧ } - name: "Case (2)" input: | - { + { ⟦ a ↦ ⟦ b ↦ @@ -19,11 +19,12 @@ tests: ⟧, e ↦ ξ.b(c ↦ ⟦⟧).d ⟧.e + ⟧ } normalized: | - { a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧ ⟧) } + { ⟦ a ↦ ξ.b (c ↦ ⟦ ⟧).d (ρ ↦ ⟦ b ↦ ⟦ c ↦ ∅, d ↦ ⟦ φ ↦ ξ.ρ.c ⟧ ⟧ ⟧) ⟧ } prettified: | - { + { ⟦ a ↦ ⟦ b ↦ @@ -33,4 +34,5 @@ tests: ⟧, e ↦ ξ.b(c ↦ ⟦⟧).d ⟧.e + ⟧ }