MAth

grammars/logic/Logic.gf

@@ -82,7 +82,9 @@ def
   ImplE _ _ (ImplI _ _ b) a = b a ;
   NegE _ (NegI _ b) a = b a ;
   UnivE _ _ (UnivI _ _ b) a = b a ;
----  ExistE _ _ _ (ExistI _ _ a b) d = d a b ; 
+  ExistE A B _ (ExistI A B a b) d = d a b ;
+ 
+---  ExistE _ _ _ (ExistI _ _  a b) d = d a b ; 
 --- does not tc 13/9/2005: {a{-2-}<>a{-0-}}
 --- moreover: no problem with
 --- ConjEr _ _ (ConjI _ _ a _) = a ;

lib/resource/abstract/Lang.gf

@@ -6,7 +6,8 @@ abstract Lang =
   Structural, 
   Basic, 
   Time, 
-  Country 
+  Country,
+  Math
 
   ** {
   fun

lib/resource/abstract/Math.gf

@@ -0,0 +1,52 @@
+
+
+abstract Math = Categories ** {
+
+--3 Noun phrases with symbols
+
+fun
+  SymbPN      : String -> PN ;             -- "x"
+  IntPN       : Int -> PN ;                -- "27"
+  IntNP       : CN -> Int -> NP ;          -- "level 53"
+
+  IndefSymbNumNP : Num -> CN -> SymbList -> NP ;         -- "(2) numbers x and y"
+  DefSymbNumNP   : Num -> CN -> SymbList -> NP ;         -- "the (2) numbers x and y"
+  NDetSymbNP     : NDet -> Num -> CN -> SymbList -> NP ; -- "some (3) points x, y and z"
+
+--3 Symbol lists
+
+-- A symbol list has at least two elements. The last two are separated
+-- by a conjunction ("and" in English), the others by commas.
+-- This produces "x, y and z", in English. 
+
+cat
+  SymbList ;
+
+fun
+  SymbTwo  : String -> String   -> SymbList ;
+  SymbMore : String -> SymbList -> SymbList ;
+
+--3 Special forms of expression
+
+-- These expression forms are typical of mathematical texts.
+
+  LetCN    : String   -> CN -> Imp ;         -- Let x be a number.
+  LetNumCN : SymbList -> Num -> CN -> Imp ;  -- Let x and y be (2) numbers.
+
+-- This rule is slightly overgenerating: "there exists every number x". 
+-- The problem seems to be of semantic nature. By this we avoid having many rules.
+
+  ExistNP : NP -> Cl ;  -- there exist (2) number(s) x and y
+
+--3 Rules moved from $Rules$.
+
+-- This rule is powerful but overgenerating.
+
+  SymbCN      : CN -> String -> CN ;       -- "number x"
+
+-- This rule is simply wrong, and will be deprecated: the correct
+-- value type is $NP$.
+
+  IntCN       : CN -> Int -> CN ;          -- "level 53"
+
+}

lib/resource/abstract/Rules.gf

@@ -17,9 +17,12 @@ fun
   UseN        : N -> CN ;                  -- "car"
   UsePN       : PN -> NP ;                 -- "John"
 
+-- These three rules have been moved to the module $Math$.
+  {-
   SymbPN      : String -> PN ;             -- "x"
   SymbCN      : CN -> String -> CN ;       -- "number x"
   IntCN       : CN -> Int -> CN ;          -- "number 53"
+  -}
 
   IndefOneNP  : CN -> NP ;                 -- "a car", "cars"
   IndefNumNP  : Num -> CN -> NP ;          -- "houses", "86 houses"

lib/resource/danish/MathDan.gf

@@ -0,0 +1,4 @@
+--# -path=.:../scandinavian:../abstract:../../prelude
+
+concrete MathDan of Math = CategoriesDan **
+  MathScand with (SyntaxScand=SyntaxDan) ;

lib/resource/danish/SyntaxDan.gf

@@ -116,4 +116,5 @@ instance SyntaxDan of SyntaxScand = TypesDan **
       {s = verbVara.s ; s1 = "ved" ; isAux = False}
       vp) ;
 
+  conjEt = "og" ;
 }

lib/resource/english/LangEng.gf

@@ -6,7 +6,8 @@ concrete LangEng of Lang =
   StructuralEng,  
   BasicEng,
   TimeEng,
-  CountryEng
+  CountryEng,
+  MathEng
 
    ** open Prelude, ParadigmsEng in {
 

lib/resource/english/MathEng.gf

@@ -0,0 +1,49 @@
+--# -path=.:../abstract:../../prelude
+
+concrete MathEng of Math = CategoriesEng **  open Prelude, SyntaxEng, ParadigmsEng in {
+
+lin
+  SymbPN i = {s = \\c => caseSymb c i.s ; g = Neutr} ;
+  IntPN i  = {s = \\c => caseSymb c i.s ; g = Neutr} ;
+  IntNP cn i = nameNounPhrase {
+    s = \\c => (cn.s ! Sg ! Nom ++ caseSymb c i.s) ; 
+    g = Neutr
+    } ;
+
+  IndefSymbNumNP nu cn xs = 
+    addSymbNounPhrase (indefNounPhraseNum plural nu cn) xs.s ;
+  DefSymbNumNP nu cn xs = 
+    addSymbNounPhrase (defNounPhraseNum plural nu cn) xs.s ;
+  NDetSymbNP det nu cn xs = 
+    addSymbNounPhrase (numDetNounPhrase det nu cn) xs.s ;
+
+lincat 
+  SymbList = SS ;
+
+lin
+  SymbTwo  = infixSS "and" ;
+  SymbMore = infixSS "," ;
+
+
+  LetCN x cn = {
+    s = \\_ => "let" ++ x.s ++ "be" ++ (indefNounPhrase singular cn).s ! NomP
+    } ;
+  LetNumCN x nu cn = {
+    s = \\_ => "let" ++ x.s ++ "be" ++ (indefNounPhraseNum plural nu cn).s ! NomP
+    } ;
+  ExistNP np = predVerbClause
+                 (nameNounPhraseN (fromAgr np.a).n (nameReg "there" Neutr))
+                 (regV "exist")
+                 (complNounPhrase np) ;
+
+-- Moved from $RulesEng$.
+
+  SymbCN cn s =
+    {s = \\n,c => cn.s ! n ! Nom ++ caseSymb c s.s ; 
+     g = cn.g} ;
+  IntCN cn s =
+    {s = \\n,c => cn.s ! n ! Nom ++ caseSymb c s.s ; 
+     g = cn.g} ;
+
+
+}

lib/resource/english/RulesEng.gf

@@ -28,14 +28,6 @@ lin
   UseN  = noun2CommNounPhrase ;
   UsePN = nameNounPhrase ;
 
-  SymbPN i = {s = table {Nom => i.s ; Gen => i.s ++ "'s"} ; g = Neutr} ; ---
-  SymbCN cn s =
-    {s = \\n,c => cn.s ! n ! c ++ s.s ; 
-     g = cn.g} ;
-  IntCN cn s =
-    {s = \\n,c => cn.s ! n ! c ++ s.s ; 
-     g = cn.g} ;
-
   IndefOneNP = indefNounPhrase singular ;
   IndefNumNP = indefNounPhraseNum plural ;
   DefOneNP = defNounPhrase singular ;

lib/resource/english/SyntaxEng.gf

@@ -66,11 +66,17 @@ oper
         APl   p => {n = Pl ; p = p ; g = human}
         } ;
 
-  nameNounPhrase : ProperName -> NounPhrase = \john -> 
-    {s = \\c => john.s ! toCase c ; a = toAgr Sg P3 john.g} ;
+  caseSymb : Case -> Str -> Str = \c,i -> case c of {
+    Nom => i ; 
+    Gen => glue i "'s"
+    } ;
 
-  nameNounPhrasePl : ProperName -> NounPhrase = \john -> 
-    {s = \\c => john.s ! toCase c ; a = toAgr Pl P3 john.g} ;
+  nameNounPhrase : ProperName -> NounPhrase = 
+    nameNounPhraseN Sg ;
+  nameNounPhrasePl : ProperName -> NounPhrase = 
+    nameNounPhraseN Pl ;
+  nameNounPhraseN : Number -> ProperName -> NounPhrase = \n,john -> 
+    {s = \\c => john.s ! toCase c ; a = toAgr n P3 john.g} ;
 
 -- The following construction has to be refined for genitive forms:
 -- "we two", "us two" are OK, but "our two" is not.
@@ -86,6 +92,14 @@ oper
   pronNounPhrase : Pronoun -> NounPhrase = \pro -> 
     {s = pro.s ; a = toAgr pro.n pro.p pro.g} ;
 
+-- To add a symbol, such as a variable or variable list, to the end of
+-- an NP.
+
+  addSymbNounPhrase : NounPhrase -> Str -> NounPhrase = \np,x ->
+    {s = \\c => np.s ! c ++ x ;
+     a = np.a
+    } ;
+
 --2 Determiners
 --
 -- Determiners are inflected according to the nouns they determine.

lib/resource/finnish/LangFin.gf

@@ -4,9 +4,10 @@ concrete LangFin of Lang =
   RulesFin, 
   ClauseFin, 
   StructuralFin,  
-  BasicFin
+  BasicFin,
 ----  TimeEng,
 ----  CountryEng
+  MathFin
 
    ** open Prelude, ParadigmsFin in {
 

lib/resource/finnish/MathFin.gf

@@ -0,0 +1,50 @@
+--# -path=.:../abstract:../../prelude
+
+concrete MathFin of Math = CategoriesFin **  open Prelude, SyntaxFin, ParadigmsFin in {
+
+lin
+  SymbPN i = {s = \\c => i.s} ;  --- case endings often needed
+  IntPN i  = {s = \\c => i.s} ;
+  IntNP cn i = nameNounPhrase {
+    s = \\c => cn.s ! False ! Sg ! c ++ i.s
+    } ;
+
+  IndefSymbNumNP nu cn xs = 
+    addSymbNounPhrase (nounPhraseNum False nu cn) xs.s ;
+  DefSymbNumNP nu cn xs = 
+    addSymbNounPhrase (nounPhraseNum True nu cn) xs.s ;
+  NDetSymbNP det nu cn xs = 
+    addSymbNounPhrase (numDetNounPhrase det nu cn) xs.s ;
+
+lincat 
+  SymbList = SS ;
+
+lin
+  SymbTwo  = infixSS "ja" ;
+  SymbMore = infixSS "," ;
+
+
+  LetCN x cn = {
+    s = \\_ => "olkoon" ++ x.s ++ (indefNounPhrase singular cn).s !
+    NPCase Nom
+    } ;
+  LetNumCN x nu cn = {
+    s = \\_ => "olkoot" ++ x.s ++ (nounPhraseNum False nu cn).s
+    ! NPCase Part
+    } ;
+
+  ExistNP np = 
+    sats2clause (
+      mkSatsCopula impersNounPhrase ("olemassa" ++ np.s ! NPCase Nom)
+      ) ;
+
+-- Moved from $RulesFin$.
+
+  SymbCN cn s =
+    {s = \\f,n,c => cn.s ! f ! n ! c ++ s.s ; 
+     g = cn.g} ;
+  IntCN cn s =
+    {s = \\f,n,c => cn.s ! f ! n ! c ++ s.s ; 
+     g = cn.g} ;
+
+}

lib/resource/finnish/RulesFin.gf

@@ -24,14 +24,6 @@ lin
   UseN  = noun2CommNounPhrase ;
   UsePN = nameNounPhrase ;
 
-  SymbPN i = {s = \\_ => i.s} ;  --- case endings often needed
-  SymbCN cn s =
-    {s = \\f,n,c => cn.s ! f ! n ! c ++ s.s ; 
-     g = cn.g} ;
-  IntCN cn s =
-    {s = \\f,n,c => cn.s ! f ! n ! c ++ s.s ; 
-     g = cn.g} ;
-
   IndefOneNP = indefNounPhrase singular ;
   IndefNumNP = nounPhraseNum False ;
   DefOneNP = defNounPhrase singular ;
@@ -206,6 +198,8 @@ lin
 
 ----  OneNP = nameNounPhrase (nameReg "one" human) ;
 
+--- should be partitive in negative forms: "ei ole olemassa puista autoa"
+
   ExistCN cn = 
     sats2clause (
       mkSatsCopula impersNounPhrase ("olemassa" ++ (singularNounPhrase cn).s ! NPCase Nom)

lib/resource/finnish/SyntaxFin.gf

@@ -157,6 +157,14 @@ oper
 
   noNum : Numeral = {s = \\_ => [] ; isNum = False ; n = Pl} ;
 
+-- To add a symbol, such as a variable or variable list, to the end of
+-- an NP.
+
+  addSymbNounPhrase : NounPhrase -> Str -> NounPhrase = \np,x ->
+    {s = \\c => np.s ! c ++ x ;
+     n = np.n ;
+     p = np.p 
+    } ;
 
 --2 Determiners
 --

lib/resource/french/MathFre.gf

@@ -0,0 +1,4 @@
+--# -path=.:../romance:../abstract:../../prelude
+
+concrete MathFre of Math = CategoriesFre **
+  MathRomance with (SyntaxRomance=SyntaxFre) ;

lib/resource/italian/MathIta.gf

@@ -0,0 +1,4 @@
+--# -path=.:../romance:../abstract:../../prelude
+
+concrete MathIta of Math = CategoriesIta **
+  MathRomance with (SyntaxRomance=SyntaxIta) ;

lib/resource/norwegian/MathNor.gf

@@ -0,0 +1,4 @@
+--# -path=.:../scandinavian:../abstract:../../prelude
+
+concrete MathNor of Math = CategoriesNor **
+  MathScand with (SyntaxScand=SyntaxNor) ;

lib/resource/norwegian/SyntaxNor.gf

@@ -117,4 +117,7 @@ instance SyntaxNor of SyntaxScand = TypesNor **
      (complVerbVerb 
       ({s = verbVara.s ; s1 = "ved" ; isAux = False})
       vp) ;
+
+  conjEt = "og" ;
+
 }

lib/resource/romance/MathRomance.gf

@@ -0,0 +1,51 @@
+--# -path=.:../romance:../abstract:../../prelude
+
+incomplete concrete MathRomance of Math = CategoriesRomance ** 
+  open Prelude, SyntaxRomance in {
+
+lin
+  SymbPN i = {s = i.s ; g = Masc} ; --- cannot know gender
+  IntPN i  = {s = i.s ; g = Masc} ;
+  IntNP cn i = nameNounPhrase {
+    s = cn.s ! Sg ++ i.s ;
+    g = cn.g
+    } ;
+
+  IndefSymbNumNP nu cn xs = 
+    addSymbNounPhrase (indefNounPhraseNum nu cn) xs.s ;
+  DefSymbNumNP nu cn xs = 
+    addSymbNounPhrase (defNounPhraseNum nu cn) xs.s ;
+  NDetSymbNP det nu cn xs = 
+    addSymbNounPhrase (numDetNounPhrase det nu cn) xs.s ;
+
+lincat 
+  SymbList = SS ;
+
+lin
+  SymbTwo  = infixSS etConj.s ;
+  SymbMore = infixSS "," ;
+
+
+  LetCN x cn = {
+    s = \\_,_ => copula.s ! VFin (VPres Con) Sg P3 ++ x.s ++ (indefNounPhrase singular cn).s !
+    unstressed nominative
+    } ;
+  LetNumCN x nu cn = {
+    s = \\_,_ => copula.s ! VFin (VPres Con) Pl P3 ++ x.s ++ (indefNounPhraseNum nu cn).s
+    ! unstressed nominative
+    } ;
+
+--- to be replaced by "il existe", "esiste", etc.
+
+  ExistNP np = existNounPhrase np ;
+
+-- Moved from $RulesRomance$.
+
+  SymbCN cn s =
+    {s = \\n => cn.s ! n ++ s.s ; 
+     g = cn.g} ;
+  IntCN cn i =
+    {s = \\n => cn.s ! n ++ i.s ; 
+     g = cn.g} ;
+
+}

lib/resource/romance/RulesRomance.gf

@@ -7,14 +7,6 @@ lin
   UseN = noun2CommNounPhrase ;
   UsePN = nameNounPhrase ;
 
-  SymbPN i = {s = i.s ; g = Masc} ; --- cannot know gender
-  SymbCN cn s =
-    {s = \\n => cn.s ! n ++ s.s ; 
-     g = cn.g} ;
-  IntCN cn i =
-    {s = \\n => cn.s ! n ++ i.s ; 
-     g = cn.g} ;
-
   IndefOneNP = indefNounPhrase singular ;
   IndefNumNP = indefNounPhraseNum ;
   DefOneNP = defNounPhrase singular ;

lib/resource/romance/SyntaxRomance.gf

@@ -80,6 +80,17 @@ oper
 
   existNounPhrase : NounPhrase -> Clause ;
 
+-- To add a symbol, such as a variable or variable list, to the end of
+-- an NP.
+
+  addSymbNounPhrase : NounPhrase -> Str -> NounPhrase = \np,x ->
+    {s = \\c => np.s ! c ++ x ;
+     g = np.g ;
+     n = np.n ;
+     p = np.p ;
+     c = np.c
+    } ;
+
 
 --2 Determiners
 --

lib/resource/scandinavian/MathScand.gf

@@ -0,0 +1,58 @@
+--# -path=.:../abstract:../../prelude
+
+incomplete concrete MathScand of Math = CategoriesScand ** 
+  open Prelude, SyntaxScand in {
+
+lin
+  SymbPN i = {s = \\_ => i.s ; g = NNeutr} ; --- cannot know gender
+  IntPN i  = {s = \\_ => i.s ; g = NNeutr} ;
+  IntNP cn i = nameNounPhrase {
+    s = \\c => cn.s ! Sg ! DefP Def ! Nom ++ i.s ;
+    g = cn.g
+    } ;
+
+  IndefSymbNumNP nu cn xs = 
+    addSymbNounPhrase (indefNounPhraseNum plural nu cn) xs.s ;
+  DefSymbNumNP nu cn xs = 
+    addSymbNounPhrase (defNounPhraseNum plural nu cn) xs.s ;
+  NDetSymbNP det nu cn xs = 
+    addSymbNounPhrase (numDetNounPhrase det nu cn) xs.s ;
+
+lincat 
+  SymbList = SS ;
+
+lin
+  SymbTwo  = infixSS conjEt ;
+  SymbMore = infixSS "," ;
+
+
+  LetCN x cn = {
+    s = \\_ => letImp ++ x.s ++ verbVara.s ! VI (Inf Act) ++ (indefNounPhrase singular cn).s !
+    PNom
+    } ;
+  LetNumCN x nu cn = {
+    s = \\_ => letImp ++ x.s ++ verbVara.s ! VI (Inf Act) ++
+    (indefNounPhraseNum plural nu cn).s
+    ! PNom
+    } ;
+
+--- to be replaced by "det existerar", etc.
+
+  ExistNP np = predVerbGroupClause npDet 
+                (complTransVerb (mkDirectVerb (deponentVerb verbFinnas)) 
+                   np) ;
+
+-- Moved from $RulesScand$.
+
+  SymbCN cn s =
+    {s = \\a,n,c => cn.s ! a ! n ! c ++ s.s ; 
+     g = cn.g ;
+     p = cn.p
+     } ;
+  IntCN cn s =
+    {s = \\a,n,c => cn.s ! a ! n ! c ++ s.s ; 
+     g = cn.g ;
+     p = cn.p
+     } ;
+
+}

lib/resource/scandinavian/RulesScand.gf

@@ -10,16 +10,13 @@ lin
   UsePN = nameNounPhrase ;
 
   SymbPN i = {s = \\_ => i.s ; g = NNeutr} ;
+
   SymbCN cn s =
-    {s = \\a,n,c => cn.s ! a ! n ! c ++ s.s ; 
-     g = cn.g ;
-     p = cn.p
-     } ;
-  IntCN cn s =
-    {s = \\a,n,c => cn.s ! a ! n ! c ++ s.s ; 
-     g = cn.g ;
-     p = cn.p
-     } ;
+    {s = \\n => cn.s ! n ++ s.s ; 
+     g = cn.g} ;
+  IntCN cn i =
+    {s = \\n => cn.s ! n ++ i.s ; 
+     g = cn.g} ;
 
   IndefOneNP = indefNounPhrase singular ;
   IndefNumNP = indefNounPhraseNum plural ;

lib/resource/scandinavian/SyntaxScand.gf

@@ -122,6 +122,11 @@ oper
 
   npDet : NounPhrase ;
 
+
+  addSymbNounPhrase : NounPhrase -> Str -> NounPhrase = \np,x -> 
+    {s = \\c => np.s ! c ++ x ; g = np.g ; n = np.n ; p = np.p} ;
+
+
 --2 Determiners
 --
 -- Determiners are inflected according to noun in gender and sex. 
@@ -1710,4 +1715,7 @@ oper
 
   pronVars, pronVem, pronVems : Str ;
 
+  conjEt : Str ;
+
+  letImp : Str = "låt" ; ---- check for all scand
 } ;

lib/resource/spanish/MathSpa.gf

@@ -0,0 +1,4 @@
+--# -path=.:../romance:../abstract:../../prelude
+
+concrete MathSpa of Math = CategoriesSpa **
+  MathRomance with (SyntaxRomance=SyntaxSpa) ;

lib/resource/swedish/MathSwe.gf

@@ -0,0 +1,4 @@
+--# -path=.:../scandinavian:../abstract:../../prelude
+
+concrete MathSwe of Math = CategoriesSwe **
+  MathScand with (SyntaxScand=SyntaxSwe) ;

lib/resource/swedish/SyntaxSwe.gf

@@ -132,4 +132,7 @@ instance SyntaxSwe of SyntaxScand = TypesSwe **
     CPpå => "på" ;
     CPtill => "till"
     } ;
+
+  conjEt = "och" ;
+
 }

src/GF/Grammar/TC.hs

@@ -5,9 +5,9 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/04/21 16:22:29 $ 
--- > CVS $Author: bringert $
--- > CVS $Revision: 1.9 $
+-- > CVS $Date: 2005/09/15 16:22:02 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.10 $
 --
 -- Thierry Coquand's type checking algorithm that creates a trace
 -----------------------------------------------------------------------------
@@ -16,6 +16,7 @@ module GF.Grammar.TC (AExp(..),
 	   Theory,
 	   checkExp,
 	   inferExp,
+           checkEqs,
 	   eqVal,
 	   whnf
 	  ) where
@@ -25,6 +26,7 @@ import GF.Grammar.Abstract
 import GF.Grammar.AbsCompute
 
 import Control.Monad
+import Data.List (sortBy)
 
 data AExp =
      AVr   Ident Val 
@@ -36,7 +38,7 @@ data AExp =
    | AApp  AExp AExp Val 
    | AAbs  Ident Val AExp 
    | AProd Ident AExp AExp 
-   | AEqs  [([Exp],AExp)] ---
+   | AEqs  [([Exp],AExp)] --- not used
    | AData Val
   deriving (Eq,Show)
 
@@ -119,11 +121,12 @@ checkExp th tenv@(k,rho,gamma) e ty = do
 	return (AAbs x a' t', cs)
       _ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ
 
+-- {- --- to get deprec when checkEqs works (15/9/2005)
     Eqs es -> do
       bcs <- mapM (\b -> checkBranch th tenv b typ) es
       let (bs,css) = unzip bcs
       return (AEqs bs, concat css) 
-
+-- - }
     Prod x a b -> do
       testErr (typ == vType) "expected Type"
       (a',csa) <- checkType th tenv a
@@ -165,7 +168,42 @@ inferExp th tenv@(k,rho,gamma) e = case e of
      IC "String" -> return $ const $ Q cPredefAbs cString
      _ -> Bad s
 
----- this is an unreliable function which should be rewritten (AR)
+checkEqs :: Theory -> TCEnv -> (Fun,Trm) -> Val -> Err [(Val,Val)]
+checkEqs th tenv@(k,rho,gamma) (fun@(m,f),def) val = case def of
+  Eqs es -> liftM concat $ mapM checkBranch es
+  _      -> liftM snd $ checkExp th tenv def val
+ where
+  checkBranch (ps,df) = 
+   let
+      (ps',_,vars) = foldr p2t ([],0,[]) ps
+      fps        = mkApp (Q m f) ps'
+   in errIn ("branch" +++ prt fps) $ do
+    (aexp, typ, cs1) <- inferExp th tenv fps
+    let
+      bds = binds vars aexp 
+      tenv' = (k, rho, bds ++ gamma) 
+    (_,cs2)  <- errIn (show bds) $ checkExp th tenv' df typ
+    return $ (cs1 ++ cs2)
+  p2t p (ps,i,g) = case p of
+     PW      -> (meta (MetaSymb i) : ps, i+1,        g) 
+     PV IW   -> (meta (MetaSymb i) : ps, i+1,        g) 
+     PV x    -> (meta (MetaSymb i) : ps, i+1,upd x i g)
+     PString s -> (            K s : ps, i,          g)
+     PInt i -> (EInt i : ps, i, g)
+     PP m c xs -> (mkApp (qq (m,c)) xss : ps, i', g') 
+                    where (xss,i',g') = foldr p2t ([],i,g) xs
+     _ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
+  upd x i g = (x,i) : g --- to annotate pattern variables: treat as metas
+  
+  -- notice: in vars, the sequence 0.. is sorted. In subst aexp, all
+  -- this occurs and nothing else.
+  binds vars aexp = [(x,v) | ((x,_),v) <- zip vars metas] where
+    metas = map snd $ sortBy (\ (x,_) (y,_) -> compare x y) $ subst aexp
+  subst aexp = case aexp of
+   AMeta (MetaSymb i) v -> [(i,v)]
+   AApp  c a _ -> subst c ++ subst a
+   _ -> [] -- never matter in patterns
+
 checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
 checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $ 
                                   chB tenv' ps' ty 
@@ -207,6 +245,7 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
 
   upd x k g = (x, VGen k x) : g --- hack to recognize pattern variables
 
+
 checkPatt :: Theory -> TCEnv -> Exp -> Val -> Err (Binds,[(Val,Val)])
 checkPatt th tenv exp val = do
   (aexp,_,cs) <- checkExpP tenv exp val

src/GF/Grammar/TypeCheck.hs

@@ -5,9 +5,9 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/09/13 22:05:32 $ 
+-- > CVS $Date: 2005/09/15 16:22:02 $ 
 -- > CVS $Author: aarne $
--- > CVS $Revision: 1.15 $
+-- > CVS $Revision: 1.16 $
 --
 -- (Description of the module)
 -----------------------------------------------------------------------------
@@ -247,8 +247,8 @@ justTypeCheckSrc gr e v = do
 ----  return $ fst $ splitConstraintsSrc gr constrs0
 ---- this change was to force proper tc of abstract modules. 
 ---- May not be quite right. AR 13/9/2005 
- where 
-   notJustMeta (c,k) = case (c,k) of
+
+notJustMeta (c,k) = case (c,k) of
      (VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
      _ -> True
 
@@ -268,8 +268,9 @@ checkTyp gr typ = err singleton prConstrs $ justTypeCheckSrc gr typ vType
 checkEquation :: Grammar -> Fun -> Trm -> [String]
 checkEquation gr (m,fun) def = err singleton id $ do
   typ  <- lookupFunTypeSrc gr m fun
+----  cs   <- checkEqs (grammar2theorySrc gr) (initTCEnv []) ((m,fun),def) (vClos typ)
   cs   <- justTypeCheckSrc gr def (vClos typ)
-  let cs1 = cs ----- filter (not . possibleConstraint gr) cs ----
+  let cs1 = filter notJustMeta cs ----- filter (not . possibleConstraint gr) cs ----
   return $ ifNull [] (singleton . prConstraints) cs1
 
 checkConstrs :: Grammar -> Cat -> [Ident] -> [String]

src/GF/UseGrammar/GetTree.hs

@@ -5,9 +5,9 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/06/03 21:51:59 $ 
+-- > CVS $Date: 2005/09/15 16:22:02 $ 
 -- > CVS $Author: aarne $
--- > CVS $Revision: 1.8 $
+-- > CVS $Revision: 1.9 $
 --
 -- how to form linearizable trees from strings and from terms of different levels
 --
@@ -24,6 +24,7 @@ import GF.Grammar.MMacros
 import GF.Grammar.Macros
 import GF.Compile.Rename
 import GF.Grammar.TypeCheck
+import GF.Grammar.AbsCompute (beta)
 import GF.Compile.PGrammar
 import GF.Compile.ShellState
 
@@ -42,7 +43,8 @@ string2treeErr :: StateGrammar -> String -> Err Tree
 string2treeErr _ "" = Bad "empty string"
 string2treeErr gr s = do
   t <- pTerm s
-  let t1 = refreshMetas [] t
+  let t0 = beta [] t
+  let t1 = refreshMetas [] t0
   let t2 = qualifTerm abstr t1
   annotate grc t2
  where