From 541b578be8999151c20e03b8fe72e2113adc7e16 Mon Sep 17 00:00:00 2001 From: aarne Date: Mon, 12 Apr 2010 10:04:29 +0000 Subject: [PATCH] 4-arg coordination by Shafqat --- examples/phrasebook/missing.txt | 2 +- lib/src/prelude/Coordination.gf | 40 +++++++++++++++++++++++++++------ 2 files changed, 34 insertions(+), 8 deletions(-) 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 } ;