mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
Remove Coordination.gf from Nep, Pes, Pun, Sin folders
They were just copies of prelude/Coordination.gf
This commit is contained in:
john.j.camilleri
@@ -1,170 +0,0 @@
|
||||
resource Coordination = open Prelude in {
|
||||
|
||||
param
|
||||
ListSize = TwoElem | ManyElem ;
|
||||
|
||||
oper
|
||||
ListX = {s1,s2 : Str} ;
|
||||
|
||||
twoStr : (x,y : Str) -> ListX = \x,y ->
|
||||
{s1 = x ; s2 = y} ;
|
||||
consStr : Str -> ListX -> Str -> ListX = \comma,xs,x ->
|
||||
{s1 = xs.s1 ++ comma ++ xs.s2 ; s2 = x } ;
|
||||
|
||||
twoSS : (_,_ : SS) -> ListX = \x,y ->
|
||||
twoStr x.s y.s ;
|
||||
consSS : Str -> ListX -> SS -> ListX = \comma,xs,x ->
|
||||
consStr comma xs x.s ;
|
||||
|
||||
Conjunction : Type = SS ;
|
||||
ConjunctionDistr : Type = {s1 : Str ; s2 : Str} ;
|
||||
|
||||
conjunctX : Conjunction -> ListX -> Str = \or,xs ->
|
||||
xs.s1 ++ or.s ++ xs.s2 ;
|
||||
|
||||
conjunctDistrX : ConjunctionDistr -> ListX -> Str = \or,xs ->
|
||||
or.s1 ++ xs.s1 ++ or.s2 ++ xs.s2 ;
|
||||
|
||||
conjunctSS : Conjunction -> ListX -> SS = \or,xs ->
|
||||
ss (xs.s1 ++ or.s ++ xs.s2) ;
|
||||
|
||||
conjunctDistrSS : ConjunctionDistr -> ListX -> SS = \or,xs ->
|
||||
ss (or.s1 ++ xs.s1 ++ or.s2 ++ xs.s2) ;
|
||||
|
||||
-- all this lifted to tables
|
||||
|
||||
ListTable : Type -> Type = \P -> {s1,s2 : P => Str} ;
|
||||
|
||||
twoTable : (P : Type) -> (_,_ : {s : P => Str}) -> ListTable P = \_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable : (P : Type) -> Str -> ListTable P -> {s : P => Str} -> ListTable P =
|
||||
\P,c,xs,x ->
|
||||
{s1 = table P {o => xs.s1 ! o ++ c ++ xs.s2 ! o} ; s2 = x.s} ;
|
||||
|
||||
conjunctTable : (P : Type) -> Conjunction -> ListTable P -> {s : P => Str} =
|
||||
\P,or,xs ->
|
||||
{s = table P {p => xs.s1 ! p ++ or.s ++ xs.s2 ! p}} ;
|
||||
|
||||
conjunctDistrTable :
|
||||
(P : Type) -> ConjunctionDistr -> ListTable P -> {s : P => Str} = \P,or,xs ->
|
||||
{s = table P {p => or.s1++ xs.s1 ! p ++ or.s2 ++ xs.s2 ! p}} ;
|
||||
|
||||
-- ... and to two- and three-argument tables: how clumsy! ---
|
||||
|
||||
ListTable2 : Type -> Type -> Type = \P,Q ->
|
||||
{s1,s2 : P => Q => Str} ;
|
||||
|
||||
twoTable2 : (P,Q : Type) -> (_,_ : {s : P => Q => Str}) -> ListTable2 P Q =
|
||||
\_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable2 :
|
||||
(P,Q : Type) -> Str -> ListTable2 P Q -> {s : P => Q => Str} -> ListTable2 P Q =
|
||||
\P,Q,c,xs,x ->
|
||||
{s1 = table P {p => table Q {q => xs.s1 ! p ! q ++ c ++ xs.s2 ! p! q}} ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable2 :
|
||||
(P,Q : Type) -> Conjunction -> ListTable2 P Q -> {s : P => Q => Str} =
|
||||
\P,Q,or,xs ->
|
||||
{s = table P {p => table Q {q => xs.s1 ! p ! q ++ or.s ++ xs.s2 ! p ! q}}} ;
|
||||
|
||||
conjunctDistrTable2 :
|
||||
(P,Q : Type) -> ConjunctionDistr -> ListTable2 P Q -> {s : P => Q => Str} =
|
||||
\P,Q,or,xs ->
|
||||
{s =
|
||||
table P {p => table Q {q => or.s1++ xs.s1 ! p ! q ++ or.s2 ++ xs.s2 ! p ! q}}} ;
|
||||
|
||||
ListTable3 : Type -> Type -> Type -> Type = \P,Q,R ->
|
||||
{s1,s2 : P => Q => R => Str} ;
|
||||
|
||||
twoTable3 : (P,Q,R : Type) -> (_,_ : {s : P => Q => R => Str}) ->
|
||||
ListTable3 P Q R =
|
||||
\_,_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable3 :
|
||||
(P,Q,R : Type) -> Str -> ListTable3 P Q R -> {s : P => Q => R => Str} ->
|
||||
ListTable3 P Q R =
|
||||
\P,Q,R,c,xs,x ->
|
||||
{s1 = \\p,q,r => xs.s1 ! p ! q ! r ++ c ++ xs.s2 ! p ! q ! r ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable3 :
|
||||
(P,Q,R : Type) -> Conjunction -> ListTable3 P Q R -> {s : P => Q => R => Str} =
|
||||
\P,Q,R,or,xs ->
|
||||
{s = \\p,q,r => xs.s1 ! p ! q ! r ++ or.s ++ xs.s2 ! p ! q ! r} ;
|
||||
|
||||
conjunctDistrTable3 :
|
||||
(P,Q,R : Type) -> ConjunctionDistr -> ListTable3 P Q R ->
|
||||
{s : P => Q => R => Str} =
|
||||
\P,Q,R,or,xs ->
|
||||
{s = \\p,q,r => or.s1++ xs.s1 ! p ! q ! r ++ or.s2 ++ xs.s2 ! p ! q ! r} ;
|
||||
|
||||
---------
|
||||
ListTable4 : Type -> Type -> Type -> Type -> Type = \P,Q,R,T ->
|
||||
{s1,s2 : P => Q => R => T => Str} ;
|
||||
|
||||
twoTable4 : (P,Q,R,T : Type) -> (_,_ : {s : P => Q => R => T => Str}) ->
|
||||
ListTable4 P Q R T =
|
||||
\_,_,_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable4 :
|
||||
(P,Q,R,T : Type) -> Str -> ListTable4 P Q R T -> {s : P => Q => R => T => Str} ->
|
||||
ListTable4 P Q R T =
|
||||
\P,Q,R,T,c,xs,x ->
|
||||
{s1 = \\p,q,r,t => xs.s1 ! p ! q ! r ! t ++ c ++ xs.s2 ! p ! q ! r ! t ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable4 :
|
||||
(P,Q,R,T : Type) -> Conjunction -> ListTable4 P Q R T -> {s : P => Q => R => T => Str} =
|
||||
\P,Q,R,T,or,xs ->
|
||||
{s = \\p,q,r,t => xs.s1 ! p ! q ! r ! t ++ or.s ++ xs.s2 ! p ! q ! r ! t} ;
|
||||
|
||||
conjunctDistrTable4 :
|
||||
(P,Q,R,T : Type) -> ConjunctionDistr -> ListTable4 P Q R T ->
|
||||
{s : P => Q => R => T => Str} =
|
||||
\P,Q,R,T,or,xs ->
|
||||
{s = \\p,q,r,t => or.s1++ xs.s1 ! p ! q ! r ! t ++ or.s2 ++ xs.s2 ! p ! q ! r ! t} ;
|
||||
--------------
|
||||
|
||||
comma = "," ;
|
||||
|
||||
-- you can also do this to right-associative lists:
|
||||
|
||||
consrStr : Str -> Str -> ListX -> ListX = \comma,x,xs ->
|
||||
{s1 = x ++ comma ++ xs.s1 ; s2 = xs.s2 } ;
|
||||
|
||||
consrSS : Str -> SS -> ListX -> ListX = \comma,x,xs ->
|
||||
consrStr comma x.s xs ;
|
||||
|
||||
consrTable : (P : Type) -> Str -> {s : P => Str} -> ListTable P -> ListTable P =
|
||||
\P,c,x,xs ->
|
||||
{s1 = table P {o => x.s ! o ++ c ++ xs.s1 ! o} ; s2 = xs.s2} ;
|
||||
|
||||
consrTable2 : (P,Q : Type) -> Str -> {s : P => Q => Str} ->
|
||||
ListTable2 P Q -> ListTable2 P Q =
|
||||
\P,Q,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => x.s ! p ! q ++ c ++ xs.s1 ! p ! q}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
consrTable4 : (P,Q,R,T : Type) -> Str -> {s : P => Q => R => T => Str} ->
|
||||
ListTable4 P Q R T -> ListTable4 P Q R T =
|
||||
\P,Q,R,T,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => table R { r => table T {t => x.s ! p ! q ! r ! t ++ c ++ xs.s1 ! p ! q ! r ! t}}}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
consrTable3 : (P,Q,R : Type) -> Str -> {s : P => Q => R => Str} ->
|
||||
ListTable3 P Q R -> ListTable3 P Q R =
|
||||
\P,Q,R,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => table R {t => x.s ! p ! q ! t ++ c ++ xs.s1 ! p ! q ! t }}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
|
||||
|
||||
} ;
|
||||
@@ -1,170 +0,0 @@
|
||||
resource Coordination = open Prelude in {
|
||||
|
||||
param
|
||||
ListSize = TwoElem | ManyElem ;
|
||||
|
||||
oper
|
||||
ListX = {s1,s2 : Str} ;
|
||||
|
||||
twoStr : (x,y : Str) -> ListX = \x,y ->
|
||||
{s1 = x ; s2 = y} ;
|
||||
consStr : Str -> ListX -> Str -> ListX = \comma,xs,x ->
|
||||
{s1 = xs.s1 ++ comma ++ xs.s2 ; s2 = x } ;
|
||||
|
||||
twoSS : (_,_ : SS) -> ListX = \x,y ->
|
||||
twoStr x.s y.s ;
|
||||
consSS : Str -> ListX -> SS -> ListX = \comma,xs,x ->
|
||||
consStr comma xs x.s ;
|
||||
|
||||
Conjunction : Type = SS ;
|
||||
ConjunctionDistr : Type = {s1 : Str ; s2 : Str} ;
|
||||
|
||||
conjunctX : Conjunction -> ListX -> Str = \or,xs ->
|
||||
xs.s1 ++ or.s ++ xs.s2 ;
|
||||
|
||||
conjunctDistrX : ConjunctionDistr -> ListX -> Str = \or,xs ->
|
||||
or.s1 ++ xs.s1 ++ or.s2 ++ xs.s2 ;
|
||||
|
||||
conjunctSS : Conjunction -> ListX -> SS = \or,xs ->
|
||||
ss (xs.s1 ++ or.s ++ xs.s2) ;
|
||||
|
||||
conjunctDistrSS : ConjunctionDistr -> ListX -> SS = \or,xs ->
|
||||
ss (or.s1 ++ xs.s1 ++ or.s2 ++ xs.s2) ;
|
||||
|
||||
-- all this lifted to tables
|
||||
|
||||
ListTable : Type -> Type = \P -> {s1,s2 : P => Str} ;
|
||||
|
||||
twoTable : (P : Type) -> (_,_ : {s : P => Str}) -> ListTable P = \_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable : (P : Type) -> Str -> ListTable P -> {s : P => Str} -> ListTable P =
|
||||
\P,c,xs,x ->
|
||||
{s1 = table P {o => xs.s1 ! o ++ c ++ xs.s2 ! o} ; s2 = x.s} ;
|
||||
|
||||
conjunctTable : (P : Type) -> Conjunction -> ListTable P -> {s : P => Str} =
|
||||
\P,or,xs ->
|
||||
{s = table P {p => xs.s1 ! p ++ or.s ++ xs.s2 ! p}} ;
|
||||
|
||||
conjunctDistrTable :
|
||||
(P : Type) -> ConjunctionDistr -> ListTable P -> {s : P => Str} = \P,or,xs ->
|
||||
{s = table P {p => or.s1++ xs.s1 ! p ++ or.s2 ++ xs.s2 ! p}} ;
|
||||
|
||||
-- ... and to two- and three-argument tables: how clumsy! ---
|
||||
|
||||
ListTable2 : Type -> Type -> Type = \P,Q ->
|
||||
{s1,s2 : P => Q => Str} ;
|
||||
|
||||
twoTable2 : (P,Q : Type) -> (_,_ : {s : P => Q => Str}) -> ListTable2 P Q =
|
||||
\_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable2 :
|
||||
(P,Q : Type) -> Str -> ListTable2 P Q -> {s : P => Q => Str} -> ListTable2 P Q =
|
||||
\P,Q,c,xs,x ->
|
||||
{s1 = table P {p => table Q {q => xs.s1 ! p ! q ++ c ++ xs.s2 ! p! q}} ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable2 :
|
||||
(P,Q : Type) -> Conjunction -> ListTable2 P Q -> {s : P => Q => Str} =
|
||||
\P,Q,or,xs ->
|
||||
{s = table P {p => table Q {q => xs.s1 ! p ! q ++ or.s ++ xs.s2 ! p ! q}}} ;
|
||||
|
||||
conjunctDistrTable2 :
|
||||
(P,Q : Type) -> ConjunctionDistr -> ListTable2 P Q -> {s : P => Q => Str} =
|
||||
\P,Q,or,xs ->
|
||||
{s =
|
||||
table P {p => table Q {q => or.s1++ xs.s1 ! p ! q ++ or.s2 ++ xs.s2 ! p ! q}}} ;
|
||||
|
||||
ListTable3 : Type -> Type -> Type -> Type = \P,Q,R ->
|
||||
{s1,s2 : P => Q => R => Str} ;
|
||||
|
||||
twoTable3 : (P,Q,R : Type) -> (_,_ : {s : P => Q => R => Str}) ->
|
||||
ListTable3 P Q R =
|
||||
\_,_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable3 :
|
||||
(P,Q,R : Type) -> Str -> ListTable3 P Q R -> {s : P => Q => R => Str} ->
|
||||
ListTable3 P Q R =
|
||||
\P,Q,R,c,xs,x ->
|
||||
{s1 = \\p,q,r => xs.s1 ! p ! q ! r ++ c ++ xs.s2 ! p ! q ! r ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable3 :
|
||||
(P,Q,R : Type) -> Conjunction -> ListTable3 P Q R -> {s : P => Q => R => Str} =
|
||||
\P,Q,R,or,xs ->
|
||||
{s = \\p,q,r => xs.s1 ! p ! q ! r ++ or.s ++ xs.s2 ! p ! q ! r} ;
|
||||
|
||||
conjunctDistrTable3 :
|
||||
(P,Q,R : Type) -> ConjunctionDistr -> ListTable3 P Q R ->
|
||||
{s : P => Q => R => Str} =
|
||||
\P,Q,R,or,xs ->
|
||||
{s = \\p,q,r => or.s1++ xs.s1 ! p ! q ! r ++ or.s2 ++ xs.s2 ! p ! q ! r} ;
|
||||
|
||||
---------
|
||||
ListTable4 : Type -> Type -> Type -> Type -> Type = \P,Q,R,T ->
|
||||
{s1,s2 : P => Q => R => T => Str} ;
|
||||
|
||||
twoTable4 : (P,Q,R,T : Type) -> (_,_ : {s : P => Q => R => T => Str}) ->
|
||||
ListTable4 P Q R T =
|
||||
\_,_,_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable4 :
|
||||
(P,Q,R,T : Type) -> Str -> ListTable4 P Q R T -> {s : P => Q => R => T => Str} ->
|
||||
ListTable4 P Q R T =
|
||||
\P,Q,R,T,c,xs,x ->
|
||||
{s1 = \\p,q,r,t => xs.s1 ! p ! q ! r ! t ++ c ++ xs.s2 ! p ! q ! r ! t ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable4 :
|
||||
(P,Q,R,T : Type) -> Conjunction -> ListTable4 P Q R T -> {s : P => Q => R => T => Str} =
|
||||
\P,Q,R,T,or,xs ->
|
||||
{s = \\p,q,r,t => xs.s1 ! p ! q ! r ! t ++ or.s ++ xs.s2 ! p ! q ! r ! t} ;
|
||||
|
||||
conjunctDistrTable4 :
|
||||
(P,Q,R,T : Type) -> ConjunctionDistr -> ListTable4 P Q R T ->
|
||||
{s : P => Q => R => T => Str} =
|
||||
\P,Q,R,T,or,xs ->
|
||||
{s = \\p,q,r,t => or.s1++ xs.s1 ! p ! q ! r ! t ++ or.s2 ++ xs.s2 ! p ! q ! r ! t} ;
|
||||
--------------
|
||||
|
||||
comma = "," ;
|
||||
|
||||
-- you can also do this to right-associative lists:
|
||||
|
||||
consrStr : Str -> Str -> ListX -> ListX = \comma,x,xs ->
|
||||
{s1 = x ++ comma ++ xs.s1 ; s2 = xs.s2 } ;
|
||||
|
||||
consrSS : Str -> SS -> ListX -> ListX = \comma,x,xs ->
|
||||
consrStr comma x.s xs ;
|
||||
|
||||
consrTable : (P : Type) -> Str -> {s : P => Str} -> ListTable P -> ListTable P =
|
||||
\P,c,x,xs ->
|
||||
{s1 = table P {o => x.s ! o ++ c ++ xs.s1 ! o} ; s2 = xs.s2} ;
|
||||
|
||||
consrTable2 : (P,Q : Type) -> Str -> {s : P => Q => Str} ->
|
||||
ListTable2 P Q -> ListTable2 P Q =
|
||||
\P,Q,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => x.s ! p ! q ++ c ++ xs.s1 ! p ! q}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
consrTable4 : (P,Q,R,T : Type) -> Str -> {s : P => Q => R => T => Str} ->
|
||||
ListTable4 P Q R T -> ListTable4 P Q R T =
|
||||
\P,Q,R,T,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => table R { r => table T {t => x.s ! p ! q ! r ! t ++ c ++ xs.s1 ! p ! q ! r ! t}}}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
consrTable3 : (P,Q,R : Type) -> Str -> {s : P => Q => R => Str} ->
|
||||
ListTable3 P Q R -> ListTable3 P Q R =
|
||||
\P,Q,R,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => table R {t => x.s ! p ! q ! t ++ c ++ xs.s1 ! p ! q ! t }}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
|
||||
|
||||
} ;
|
||||
@@ -1,170 +0,0 @@
|
||||
resource Coordination = open Prelude in {
|
||||
|
||||
param
|
||||
ListSize = TwoElem | ManyElem ;
|
||||
|
||||
oper
|
||||
ListX = {s1,s2 : Str} ;
|
||||
|
||||
twoStr : (x,y : Str) -> ListX = \x,y ->
|
||||
{s1 = x ; s2 = y} ;
|
||||
consStr : Str -> ListX -> Str -> ListX = \comma,xs,x ->
|
||||
{s1 = xs.s1 ++ comma ++ xs.s2 ; s2 = x } ;
|
||||
|
||||
twoSS : (_,_ : SS) -> ListX = \x,y ->
|
||||
twoStr x.s y.s ;
|
||||
consSS : Str -> ListX -> SS -> ListX = \comma,xs,x ->
|
||||
consStr comma xs x.s ;
|
||||
|
||||
Conjunction : Type = SS ;
|
||||
ConjunctionDistr : Type = {s1 : Str ; s2 : Str} ;
|
||||
|
||||
conjunctX : Conjunction -> ListX -> Str = \or,xs ->
|
||||
xs.s1 ++ or.s ++ xs.s2 ;
|
||||
|
||||
conjunctDistrX : ConjunctionDistr -> ListX -> Str = \or,xs ->
|
||||
or.s1 ++ xs.s1 ++ or.s2 ++ xs.s2 ;
|
||||
|
||||
conjunctSS : Conjunction -> ListX -> SS = \or,xs ->
|
||||
ss (xs.s1 ++ or.s ++ xs.s2) ;
|
||||
|
||||
conjunctDistrSS : ConjunctionDistr -> ListX -> SS = \or,xs ->
|
||||
ss (or.s1 ++ xs.s1 ++ or.s2 ++ xs.s2) ;
|
||||
|
||||
-- all this lifted to tables
|
||||
|
||||
ListTable : Type -> Type = \P -> {s1,s2 : P => Str} ;
|
||||
|
||||
twoTable : (P : Type) -> (_,_ : {s : P => Str}) -> ListTable P = \_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable : (P : Type) -> Str -> ListTable P -> {s : P => Str} -> ListTable P =
|
||||
\P,c,xs,x ->
|
||||
{s1 = table P {o => xs.s1 ! o ++ c ++ xs.s2 ! o} ; s2 = x.s} ;
|
||||
|
||||
conjunctTable : (P : Type) -> Conjunction -> ListTable P -> {s : P => Str} =
|
||||
\P,or,xs ->
|
||||
{s = table P {p => xs.s1 ! p ++ or.s ++ xs.s2 ! p}} ;
|
||||
|
||||
conjunctDistrTable :
|
||||
(P : Type) -> ConjunctionDistr -> ListTable P -> {s : P => Str} = \P,or,xs ->
|
||||
{s = table P {p => or.s1++ xs.s1 ! p ++ or.s2 ++ xs.s2 ! p}} ;
|
||||
|
||||
-- ... and to two- and three-argument tables: how clumsy! ---
|
||||
|
||||
ListTable2 : Type -> Type -> Type = \P,Q ->
|
||||
{s1,s2 : P => Q => Str} ;
|
||||
|
||||
twoTable2 : (P,Q : Type) -> (_,_ : {s : P => Q => Str}) -> ListTable2 P Q =
|
||||
\_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable2 :
|
||||
(P,Q : Type) -> Str -> ListTable2 P Q -> {s : P => Q => Str} -> ListTable2 P Q =
|
||||
\P,Q,c,xs,x ->
|
||||
{s1 = table P {p => table Q {q => xs.s1 ! p ! q ++ c ++ xs.s2 ! p! q}} ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable2 :
|
||||
(P,Q : Type) -> Conjunction -> ListTable2 P Q -> {s : P => Q => Str} =
|
||||
\P,Q,or,xs ->
|
||||
{s = table P {p => table Q {q => xs.s1 ! p ! q ++ or.s ++ xs.s2 ! p ! q}}} ;
|
||||
|
||||
conjunctDistrTable2 :
|
||||
(P,Q : Type) -> ConjunctionDistr -> ListTable2 P Q -> {s : P => Q => Str} =
|
||||
\P,Q,or,xs ->
|
||||
{s =
|
||||
table P {p => table Q {q => or.s1++ xs.s1 ! p ! q ++ or.s2 ++ xs.s2 ! p ! q}}} ;
|
||||
|
||||
ListTable3 : Type -> Type -> Type -> Type = \P,Q,R ->
|
||||
{s1,s2 : P => Q => R => Str} ;
|
||||
|
||||
twoTable3 : (P,Q,R : Type) -> (_,_ : {s : P => Q => R => Str}) ->
|
||||
ListTable3 P Q R =
|
||||
\_,_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable3 :
|
||||
(P,Q,R : Type) -> Str -> ListTable3 P Q R -> {s : P => Q => R => Str} ->
|
||||
ListTable3 P Q R =
|
||||
\P,Q,R,c,xs,x ->
|
||||
{s1 = \\p,q,r => xs.s1 ! p ! q ! r ++ c ++ xs.s2 ! p ! q ! r ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable3 :
|
||||
(P,Q,R : Type) -> Conjunction -> ListTable3 P Q R -> {s : P => Q => R => Str} =
|
||||
\P,Q,R,or,xs ->
|
||||
{s = \\p,q,r => xs.s1 ! p ! q ! r ++ or.s ++ xs.s2 ! p ! q ! r} ;
|
||||
|
||||
conjunctDistrTable3 :
|
||||
(P,Q,R : Type) -> ConjunctionDistr -> ListTable3 P Q R ->
|
||||
{s : P => Q => R => Str} =
|
||||
\P,Q,R,or,xs ->
|
||||
{s = \\p,q,r => or.s1++ xs.s1 ! p ! q ! r ++ or.s2 ++ xs.s2 ! p ! q ! r} ;
|
||||
|
||||
---------
|
||||
ListTable4 : Type -> Type -> Type -> Type -> Type = \P,Q,R,T ->
|
||||
{s1,s2 : P => Q => R => T => Str} ;
|
||||
|
||||
twoTable4 : (P,Q,R,T : Type) -> (_,_ : {s : P => Q => R => T => Str}) ->
|
||||
ListTable4 P Q R T =
|
||||
\_,_,_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable4 :
|
||||
(P,Q,R,T : Type) -> Str -> ListTable4 P Q R T -> {s : P => Q => R => T => Str} ->
|
||||
ListTable4 P Q R T =
|
||||
\P,Q,R,T,c,xs,x ->
|
||||
{s1 = \\p,q,r,t => xs.s1 ! p ! q ! r ! t ++ c ++ xs.s2 ! p ! q ! r ! t ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable4 :
|
||||
(P,Q,R,T : Type) -> Conjunction -> ListTable4 P Q R T -> {s : P => Q => R => T => Str} =
|
||||
\P,Q,R,T,or,xs ->
|
||||
{s = \\p,q,r,t => xs.s1 ! p ! q ! r ! t ++ or.s ++ xs.s2 ! p ! q ! r ! t} ;
|
||||
|
||||
conjunctDistrTable4 :
|
||||
(P,Q,R,T : Type) -> ConjunctionDistr -> ListTable4 P Q R T ->
|
||||
{s : P => Q => R => T => Str} =
|
||||
\P,Q,R,T,or,xs ->
|
||||
{s = \\p,q,r,t => or.s1++ xs.s1 ! p ! q ! r ! t ++ or.s2 ++ xs.s2 ! p ! q ! r ! t} ;
|
||||
--------------
|
||||
|
||||
comma = "," ;
|
||||
|
||||
-- you can also do this to right-associative lists:
|
||||
|
||||
consrStr : Str -> Str -> ListX -> ListX = \comma,x,xs ->
|
||||
{s1 = x ++ comma ++ xs.s1 ; s2 = xs.s2 } ;
|
||||
|
||||
consrSS : Str -> SS -> ListX -> ListX = \comma,x,xs ->
|
||||
consrStr comma x.s xs ;
|
||||
|
||||
consrTable : (P : Type) -> Str -> {s : P => Str} -> ListTable P -> ListTable P =
|
||||
\P,c,x,xs ->
|
||||
{s1 = table P {o => x.s ! o ++ c ++ xs.s1 ! o} ; s2 = xs.s2} ;
|
||||
|
||||
consrTable2 : (P,Q : Type) -> Str -> {s : P => Q => Str} ->
|
||||
ListTable2 P Q -> ListTable2 P Q =
|
||||
\P,Q,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => x.s ! p ! q ++ c ++ xs.s1 ! p ! q}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
consrTable4 : (P,Q,R,T : Type) -> Str -> {s : P => Q => R => T => Str} ->
|
||||
ListTable4 P Q R T -> ListTable4 P Q R T =
|
||||
\P,Q,R,T,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => table R { r => table T {t => x.s ! p ! q ! r ! t ++ c ++ xs.s1 ! p ! q ! r ! t}}}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
consrTable3 : (P,Q,R : Type) -> Str -> {s : P => Q => R => Str} ->
|
||||
ListTable3 P Q R -> ListTable3 P Q R =
|
||||
\P,Q,R,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => table R {t => x.s ! p ! q ! t ++ c ++ xs.s1 ! p ! q ! t }}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
|
||||
|
||||
} ;
|
||||
@@ -1,170 +0,0 @@
|
||||
resource Coordination = open Prelude in {
|
||||
|
||||
param
|
||||
ListSize = TwoElem | ManyElem ;
|
||||
|
||||
oper
|
||||
ListX = {s1,s2 : Str} ;
|
||||
|
||||
twoStr : (x,y : Str) -> ListX = \x,y ->
|
||||
{s1 = x ; s2 = y} ;
|
||||
consStr : Str -> ListX -> Str -> ListX = \comma,xs,x ->
|
||||
{s1 = xs.s1 ++ comma ++ xs.s2 ; s2 = x } ;
|
||||
|
||||
twoSS : (_,_ : SS) -> ListX = \x,y ->
|
||||
twoStr x.s y.s ;
|
||||
consSS : Str -> ListX -> SS -> ListX = \comma,xs,x ->
|
||||
consStr comma xs x.s ;
|
||||
|
||||
Conjunction : Type = SS ;
|
||||
ConjunctionDistr : Type = {s1 : Str ; s2 : Str} ;
|
||||
|
||||
conjunctX : Conjunction -> ListX -> Str = \or,xs ->
|
||||
xs.s1 ++ or.s ++ xs.s2 ;
|
||||
|
||||
conjunctDistrX : ConjunctionDistr -> ListX -> Str = \or,xs ->
|
||||
or.s1 ++ xs.s1 ++ or.s2 ++ xs.s2 ;
|
||||
|
||||
conjunctSS : Conjunction -> ListX -> SS = \or,xs ->
|
||||
ss (xs.s1 ++ or.s ++ xs.s2) ;
|
||||
|
||||
conjunctDistrSS : ConjunctionDistr -> ListX -> SS = \or,xs ->
|
||||
ss (or.s1 ++ xs.s1 ++ or.s2 ++ xs.s2) ;
|
||||
|
||||
-- all this lifted to tables
|
||||
|
||||
ListTable : Type -> Type = \P -> {s1,s2 : P => Str} ;
|
||||
|
||||
twoTable : (P : Type) -> (_,_ : {s : P => Str}) -> ListTable P = \_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable : (P : Type) -> Str -> ListTable P -> {s : P => Str} -> ListTable P =
|
||||
\P,c,xs,x ->
|
||||
{s1 = table P {o => xs.s1 ! o ++ c ++ xs.s2 ! o} ; s2 = x.s} ;
|
||||
|
||||
conjunctTable : (P : Type) -> Conjunction -> ListTable P -> {s : P => Str} =
|
||||
\P,or,xs ->
|
||||
{s = table P {p => xs.s1 ! p ++ or.s ++ xs.s2 ! p}} ;
|
||||
|
||||
conjunctDistrTable :
|
||||
(P : Type) -> ConjunctionDistr -> ListTable P -> {s : P => Str} = \P,or,xs ->
|
||||
{s = table P {p => or.s1++ xs.s1 ! p ++ or.s2 ++ xs.s2 ! p}} ;
|
||||
|
||||
-- ... and to two- and three-argument tables: how clumsy! ---
|
||||
|
||||
ListTable2 : Type -> Type -> Type = \P,Q ->
|
||||
{s1,s2 : P => Q => Str} ;
|
||||
|
||||
twoTable2 : (P,Q : Type) -> (_,_ : {s : P => Q => Str}) -> ListTable2 P Q =
|
||||
\_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable2 :
|
||||
(P,Q : Type) -> Str -> ListTable2 P Q -> {s : P => Q => Str} -> ListTable2 P Q =
|
||||
\P,Q,c,xs,x ->
|
||||
{s1 = table P {p => table Q {q => xs.s1 ! p ! q ++ c ++ xs.s2 ! p! q}} ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable2 :
|
||||
(P,Q : Type) -> Conjunction -> ListTable2 P Q -> {s : P => Q => Str} =
|
||||
\P,Q,or,xs ->
|
||||
{s = table P {p => table Q {q => xs.s1 ! p ! q ++ or.s ++ xs.s2 ! p ! q}}} ;
|
||||
|
||||
conjunctDistrTable2 :
|
||||
(P,Q : Type) -> ConjunctionDistr -> ListTable2 P Q -> {s : P => Q => Str} =
|
||||
\P,Q,or,xs ->
|
||||
{s =
|
||||
table P {p => table Q {q => or.s1++ xs.s1 ! p ! q ++ or.s2 ++ xs.s2 ! p ! q}}} ;
|
||||
|
||||
ListTable3 : Type -> Type -> Type -> Type = \P,Q,R ->
|
||||
{s1,s2 : P => Q => R => Str} ;
|
||||
|
||||
twoTable3 : (P,Q,R : Type) -> (_,_ : {s : P => Q => R => Str}) ->
|
||||
ListTable3 P Q R =
|
||||
\_,_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable3 :
|
||||
(P,Q,R : Type) -> Str -> ListTable3 P Q R -> {s : P => Q => R => Str} ->
|
||||
ListTable3 P Q R =
|
||||
\P,Q,R,c,xs,x ->
|
||||
{s1 = \\p,q,r => xs.s1 ! p ! q ! r ++ c ++ xs.s2 ! p ! q ! r ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable3 :
|
||||
(P,Q,R : Type) -> Conjunction -> ListTable3 P Q R -> {s : P => Q => R => Str} =
|
||||
\P,Q,R,or,xs ->
|
||||
{s = \\p,q,r => xs.s1 ! p ! q ! r ++ or.s ++ xs.s2 ! p ! q ! r} ;
|
||||
|
||||
conjunctDistrTable3 :
|
||||
(P,Q,R : Type) -> ConjunctionDistr -> ListTable3 P Q R ->
|
||||
{s : P => Q => R => Str} =
|
||||
\P,Q,R,or,xs ->
|
||||
{s = \\p,q,r => or.s1++ xs.s1 ! p ! q ! r ++ or.s2 ++ xs.s2 ! p ! q ! r} ;
|
||||
|
||||
---------
|
||||
ListTable4 : Type -> Type -> Type -> Type -> Type = \P,Q,R,T ->
|
||||
{s1,s2 : P => Q => R => T => Str} ;
|
||||
|
||||
twoTable4 : (P,Q,R,T : Type) -> (_,_ : {s : P => Q => R => T => Str}) ->
|
||||
ListTable4 P Q R T =
|
||||
\_,_,_,_,x,y ->
|
||||
{s1 = x.s ; s2 = y.s} ;
|
||||
|
||||
consTable4 :
|
||||
(P,Q,R,T : Type) -> Str -> ListTable4 P Q R T -> {s : P => Q => R => T => Str} ->
|
||||
ListTable4 P Q R T =
|
||||
\P,Q,R,T,c,xs,x ->
|
||||
{s1 = \\p,q,r,t => xs.s1 ! p ! q ! r ! t ++ c ++ xs.s2 ! p ! q ! r ! t ;
|
||||
s2 = x.s
|
||||
} ;
|
||||
|
||||
conjunctTable4 :
|
||||
(P,Q,R,T : Type) -> Conjunction -> ListTable4 P Q R T -> {s : P => Q => R => T => Str} =
|
||||
\P,Q,R,T,or,xs ->
|
||||
{s = \\p,q,r,t => xs.s1 ! p ! q ! r ! t ++ or.s ++ xs.s2 ! p ! q ! r ! t} ;
|
||||
|
||||
conjunctDistrTable4 :
|
||||
(P,Q,R,T : Type) -> ConjunctionDistr -> ListTable4 P Q R T ->
|
||||
{s : P => Q => R => T => Str} =
|
||||
\P,Q,R,T,or,xs ->
|
||||
{s = \\p,q,r,t => or.s1++ xs.s1 ! p ! q ! r ! t ++ or.s2 ++ xs.s2 ! p ! q ! r ! t} ;
|
||||
--------------
|
||||
|
||||
comma = "," ;
|
||||
|
||||
-- you can also do this to right-associative lists:
|
||||
|
||||
consrStr : Str -> Str -> ListX -> ListX = \comma,x,xs ->
|
||||
{s1 = x ++ comma ++ xs.s1 ; s2 = xs.s2 } ;
|
||||
|
||||
consrSS : Str -> SS -> ListX -> ListX = \comma,x,xs ->
|
||||
consrStr comma x.s xs ;
|
||||
|
||||
consrTable : (P : Type) -> Str -> {s : P => Str} -> ListTable P -> ListTable P =
|
||||
\P,c,x,xs ->
|
||||
{s1 = table P {o => x.s ! o ++ c ++ xs.s1 ! o} ; s2 = xs.s2} ;
|
||||
|
||||
consrTable2 : (P,Q : Type) -> Str -> {s : P => Q => Str} ->
|
||||
ListTable2 P Q -> ListTable2 P Q =
|
||||
\P,Q,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => x.s ! p ! q ++ c ++ xs.s1 ! p ! q}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
consrTable4 : (P,Q,R,T : Type) -> Str -> {s : P => Q => R => T => Str} ->
|
||||
ListTable4 P Q R T -> ListTable4 P Q R T =
|
||||
\P,Q,R,T,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => table R { r => table T {t => x.s ! p ! q ! r ! t ++ c ++ xs.s1 ! p ! q ! r ! t}}}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
consrTable3 : (P,Q,R : Type) -> Str -> {s : P => Q => R => Str} ->
|
||||
ListTable3 P Q R -> ListTable3 P Q R =
|
||||
\P,Q,R,c,x,xs ->
|
||||
{s1 = table P {p => table Q {q => table R {t => x.s ! p ! q ! t ++ c ++ xs.s1 ! p ! q ! t }}} ;
|
||||
s2 = xs.s2
|
||||
} ;
|
||||
|
||||
|
||||
} ;
|
||||
Reference in New Issue
Block a user