diff --git a/examples/phrasebook/missing.txt b/examples/phrasebook/missing.txt index 908552b37..c1d166b1c 100644 --- a/examples/phrasebook/missing.txt +++ b/examples/phrasebook/missing.txt @@ -4,5 +4,5 @@ PhrasebookFin : PhrasebookFre : AHasRoom AHasTable AReady Cheap Cinema Hotel PSeeYou PSeeYouPlace Park School Shop Suspect Theatre Tomorrow University PhrasebookGer : AHasAge AHasChildren AHasRoom AHasTable AMarried AReady Bar Cheap Chicken Children Cinema Coffee Daughter Dollar Flemish GNiceToMeetYou Hotel Husband Lei Meat Museum PSeeYou PSeeYouPlace Park QWhatAge Romanian School Shop Son Suspect Swedish SwedishCrown Tea Theatre Toilet Tomorrow Wife PhrasebookIta : -PhrasebookRon : AHasAge AHasChildren AHasName AHasRoom AHasTable AHungry AIll AKnow ALive AMarried AReady AScared AThirsty ATired AWantGo Airport Belgian Belgium Cheap Chicken Children Church Cinema Coffee DanishCrown Daughter English Finnish Flemish French Friday GExcusePol GPleaseGivePol GSorryPol Hospital Hotel Husband Italian Meat Monday Museum PSeeYou PSeeYouPlace Park PropClosed PropClosedDate PropClosedDay PropOpen PropOpenDate PropOpenDay QWhatAge QWhatName Romanian Saturday School Shop Son Station Sunday Suspect Swedish SwedishCrown Tea Theatre Thursday Tomorrow Tuesday University Wednesday Wife +PhrasebookRon : AHungry AThirsty Flemish GExcusePol GPleaseGivePol GSorryPol PhrasebookSwe : diff --git a/lib/src/prelude/Coordination.gf b/lib/src/prelude/Coordination.gf index 4c7f55f40..b9fc7a25e 100644 --- a/lib/src/prelude/Coordination.gf +++ b/lib/src/prelude/Coordination.gf @@ -103,6 +103,35 @@ oper {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 = "," ; @@ -124,13 +153,10 @@ oper {s1 = table P {p => table Q {q => x.s ! p ! q ++ c ++ xs.s1 ! p ! q}} ; 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 { - r => x.s ! p ! q ! r ++ c ++ xs.s1 ! p ! q ! r - }}} ; + 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 } ;