-- POPL.examples -- Client.model (new version) [SortTest~ REC[ -- Interfaces Points: TYPE ObjectType~@Points.mesa[][]; Names: TYPE ObjectType~@Names.mesa[][]; Sort: [T: TYPE ObjectType]->([]->[TYPE Sort])~@Sort.mesa; SortP: TYPE Sort~Sort[Points][]; SortN: TYPE Sort~Sort[Names][]; -- Implementation Quicksort: [I: TYPE Sort]->([]->I)~@Quicksort.mesa; Heapsort: [I: TYPE Sort]->([]->I)~@Heapsort.mesa; -- Now the instances and client Client: CONTROL ~ @ClientImpl.mesa[SortPoints~SortP, SortNames~SortN][ QuicksortP~Quicksort[SortP][], QuicksortN~Quicksort[SortN][], HeapsortP~Heapsort[SortP][], HeapsortN~Heapsort[SortN][]] ]] -- ClientDefaulted.model [SortTest~REC[ -- Interfaces Points: TYPE ObjectType~@Points.mesa*[][]; Names: TYPE ObjectType~@Names.mesa*[][]; Sort: [T: TYPE ObjectType]->([]->TYPE Sort)~@Sort.mesa; SortPoints: TYPE Sort~Sort*[T~Points][]; SortNames: TYPE Sort~Sort*[T~Names][]; -- Implementation Quicksort: [I: TYPE Sort]->([]->I)~@Quicksort.mesa; Heapsort: [I: TYPE Sort]->([]->I)~@Heapsort.mesa; -- Now the instances and client Client: CONTROL ~ @ClientImpl.mesa*[ QuicksortP~Quicksort*[SortPoints][], QuicksortN~Quicksort*[SortNames][], HeapsortP~Heapsort*[SortPoints][], HeapsortN~Heapsort*[SortNames][]] ]] -- expressions REC [x: STRING~"lit", y: STRING~x] LET [C~@Cedar.model] IN [C.Rope, C.Space] LET @Cedar.model IN [Rope, Space] []->[TYPE Sort] REC [ Identity: ([in: STRING] -> STRING) ~ LAMBDA [in: STRING] => STRING IN in, Silly: ([in: STRING] -> STRING) ~ LAMBDA [in: STRING] => STRING IN REC [ Outer ~ LAMBDA [x: STRING] => STRING IN REC [ Inner ~ LAMBDA [x: STRING] => STRING IN [ a: STRING ~ "InnerA", b: STRING ~ x].b, a: STRING ~ "OuterA", b: STRING ~ Inner[a]].b, a: STRING ~ Outer[in]].a, a: STRING ~ "a", b: STRING ~ "b", c: STRING ~ Identity[a], d: STRING ~ Identity[b], e: STRING ~ Identity["qwerty"], f: STRING ~ Silly[a], g: STRING ~ Silly[b] ] [BTreeInterface: TYPE BTree ~ @BTreeModule.mesa[SortParameter~SortInterface]] [x: STRING~"lit", y: TYPE Y~Defs]^[x: STRING] [x: STRING, y: TYPE Y]-[x: STRING~"lit"] [ P: [x: STRING, y: TYPE Y]->[z: TYPE Z]~[]; PSplit: [x: STRING]->([y: TYPE Y]->[z: TYPE Z]) ~ P\[x: STRING]; P1: [y: TYPE Y]->[z: TYPE Z] ~ PSplit["lit"]; z1: TYPE Z ~ P1[y]; P2: [y: TYPE Y] -> [z: TYPE Z]~(P/[y: TYPE Y])*[]; z2: TYPE Z ~ P2*[]; P3 ~ (P/[y: TYPE Y])*[]; z3: TYPE Z ~ P3*[] ] -- Cedar.model [Ascii: TYPE Ascii ~ @Ascii.mesa[], Rope: TYPE Rope ~ @Rope.mesa*[], IO: TYPE IO ~ @IO.mesa*[], Space: TYPE Space ~ @Space.mesa*[]] -- CedarInsts.model ********** LAMBDA [Interfaces: [Ascii~TYPE Ascii, Rope~TYPE Rope, IO~TYPE IO, Space~TYPE Space]] => Interfaces IN [[Ascii, Rope, IO, Space] ~ LET Interfaces IN [ @AsciiImpl.mesa[], @RopeImpl.mesa*[], @IOImpl.mesa*[], @SpaceImpl.mesa*[] ]] -- BTree1.model LET [ Ascii: TYPE Ascii ~ @Ascii.mesa[], Rope: TYPE Rope ~ @Rope.mesa*[], IO: TYPE IO ~ @IO.mesa*[], Space: TYPE Space ~ @Space.mesa*[]] IN [ BTreeProc ~ LAMBDA [RopeInst: Rope, IOInst: IO, SpaceInst: Space] => [BTree: TYPE BTree, BTreeInst: BTree] IN [ BTree: TYPE BTree ~ @BTree.mesa[Ascii], BTreeInst: BTree ~ @BTreeImpl.mesa [BTree, Rope, IO, Space, RopeInst, IOInst, SpaceInst] ]] -- BTree2.model LET @Cedar.model IN [ BTreeProc ~ LAMBDA [RopeInst: Rope, IOInst: IO, SpaceInst: Space] => [BTree: TYPE BTree, BTreeInst: BTree] IN [ BTree: TYPE BTree ~ @BTree.mesa[Ascii], BTreeInst: BTree ~ @BTreeImpl.mesa*[RopeInst, IOInst, SpaceInst]]] -- BTree3.model [BTreeProc ~ LAMBDA[ Interfaces: [Ascii~TYPE Ascii, Rope~TYPE Rope, IO~TYPE IO, Space~TYPE Space], Inst: Interfaces] => [BTree: TYPE BTree, BTreeInst: BTree] IN LET Interfaces IN [ BTree: TYPE BTree ~ @BTree.mesa[Ascii], BTreeInst: BTree ~ @BTreeImpl.mesa*[Inst.Rope, Inst.IO, Inst.Space]] ] -- TabGen.model [] -> [Tables: [] -> [T: TYPE PGSTables], TablesImpl: Tables, Actions: ActionsInterface + OtherParameters + [T: TYPE PGSTables, TImpl: T, Parser: TYPE Parser, ParserImpl: Parser] -> [AI: ActionsInterface]] -- Pacal Parser [[PascalTables: [] -> [T: TYPE PGSTables], PascalTablesImpl: PascalTables, PascalActions: [PascalParser: TYPE PP, X: TYPE X, XI: X, T: TYPE PGSTables, TImpl: T, Parser: TYPE Parser, ParserImpl: Parser] -> [PascalParserImpl: PascalParser]]~ @PascalGrammar.pgs[]] [PascalParserInstance: PascalParser ~ PascalActions*[T~PascalTables[], TImpl~PascalTablesImpl]]