From c066721dd1b200eb7e22c8c242bf48a83e5fcc69 Mon Sep 17 00:00:00 2001 From: krasimir Date: Wed, 7 Jul 2010 10:12:08 +0000 Subject: fix in example/tutorial/smart/SmartFre.gf to make the dependent types work nicely --- examples/tutorial/smart/SmartEng.gf | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'examples/tutorial/smart/SmartEng.gf') diff --git a/examples/tutorial/smart/SmartEng.gf b/examples/tutorial/smart/SmartEng.gf index eff8a000a..c5d9ac090 100644 --- a/examples/tutorial/smart/SmartEng.gf +++ b/examples/tutorial/smart/SmartEng.gf @@ -18,6 +18,9 @@ lincat Action = {s : VForm => Str ; part : Str} ; Device = {s : Str ; n : Number} ; Location = SS ; + Switchable = SS ; + Dimmable = SS ; + Statelike = SS ; lin UCommand c = c ; @@ -42,10 +45,10 @@ lin light = mkNoun "light" ; fan = mkNoun "fan" ; - switchOn _ _ = mkVerb "switch" "swithced" "on" ; - switchOff _ _ = mkVerb "switch" "swithced" "off" ; + switchOn _ proof = mkVerb proof.s "switch" "switched" "on" ; + switchOff _ proof = mkVerb proof.s "switch" "switched" "off" ; - dim _ _ = mkVerb "dim" "dimmed" [] ; + dim _ proof = mkVerb proof.s "dim" "dimmed" [] ; kitchen = ss "kitchen" ; livingRoom = ss ["living room"] ; @@ -58,10 +61,10 @@ oper } } ; - mkVerb : (_,_,_ : Str) -> {s : VForm => Str ; part : Str} = \go,gone,away -> { + mkVerb : (_,_,_,_ : Str) -> {s : VForm => Str ; part : Str} = \proof,go,gone,away -> { s = table { - VImp => go ; - VPart => gone + VImp => proof++go ; + VPart => proof++gone } ; part = away } ; -- cgit v1.2.3